{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T22:29:32Z","timestamp":1729636172653,"version":"3.28.0"},"reference-count":16,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/lics.2003.1210047","type":"proceedings-article","created":{"date-parts":[[2003,12,22]],"date-time":"2003-12-22T17:34:10Z","timestamp":1072114450000},"page":"75-84","source":"Crossref","is-referenced-by-count":2,"title":["Orienting equalities with the Knuth-Bendix order"],"prefix":"10.1109","author":[{"given":"K.","family":"Korovin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"15","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90226-Y"},{"journal-title":"Theory of Linear and Integer Programming","year":"1998","author":"schrijver","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17220-3_4"},{"key":"14","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/10703163_26","article-title":"RPO constraint solving is in NP","volume":"1584","author":"narendran","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90175-6"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0047120"},{"journal-title":"Introduction to Algorithms","year":"1991","author":"cormen","key":"3"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017470"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054190000278"},{"key":"10","first-page":"1","article-title":"Verifying orientability of rewrite rules using the Knuth-Bendix order","author":"korovin","year":"2003","journal-title":"Information and Computation"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1016\/0041-5553(80)90061-0"},{"key":"6","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-54233-7_155","article-title":"Satisfiability of systems of ordinal notations with the subterm property is decidable","volume":"510","author":"jouannaud","year":"1991","journal-title":"Lecture Notes in Computer Science"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/BF01237233"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15976-2_12"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45127-7_12"},{"key":"8","doi-asserted-by":"crossref","first-page":"979","DOI":"10.1007\/3-540-48224-5_79","article-title":"Knuth-Bendix ordering constraint solving is NP-complete","volume":"2076","author":"korovin","year":"2001","journal-title":"Lecture Notes in Computer Science"}],"event":{"name":"18th Annual IEEE Symposium on Logic in Computer Science","acronym":"LICS-03","location":"Ottawa, Ont., Canada"},"container-title":["18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8592\/27231\/01210047.pdf?arnumber=1210047","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T02:58:18Z","timestamp":1497581898000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1210047\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":16,"URL":"https:\/\/doi.org\/10.1109\/lics.2003.1210047","relation":{},"subject":[]}}