{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:01:57Z","timestamp":1725487317963},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421177"},{"type":"electronic","value":"9783540451273"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45127-7_12","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:25:25Z","timestamp":1184588725000},"page":"137-153","source":"Crossref","is-referenced-by-count":7,"title":["Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order"],"prefix":"10.1007","author":[{"given":"Konstantin","family":"Korovin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,5,8]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University press, Cambridge, 1998."},{"issue":"4","key":"12_CR2","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1142\/S0129054190000278","volume":"1","author":"H. Comon","year":"1990","unstructured":"H. Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387\u2013411, 1990.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"12_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0017470","volume-title":"Trees in Algebra and Programming: CAAP\u201994","author":"H. Comon","year":"1994","unstructured":"H. Comon and R. Treinen. Ordering constraints on trees. In S. Tison, editor, Trees in Algebra and Programming: CAAP\u201994, volume 787 of Lecture Notes in Computer Science, pages 1\u201314. Springer Verlag, 1994."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and D.A. Plaisted. Rewriting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 9, pages 533\u2013608. Elsevier Science, 2001.","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/3-540-15976-2_12","volume-title":"Rewriting Techniques and Applications, First International Conference, RTA-85","author":"D. Detlefs","year":"1985","unstructured":"D. Detlefs and R. Forgaard. A procedure for automatically proving the termination of a set of rewrite rules. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, First International Conference, RTA-85, volume 202 of Lecture Notes in Computer Science, pages 255\u2013270, Dijon, France, 1985. Springer Verlag."},{"issue":"2","key":"12_CR6","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF01237233","volume":"28","author":"J. Dick","year":"1990","unstructured":"J. Dick, J. Kalmus, and U. Martin. Automating the Knuth-Bendix ordering. Acta Informatica, 28(2):95\u2013119, 1990.","journal-title":"Acta Informatica"},{"key":"12_CR7","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, 1970."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"K. Korovin and A. Voronkov. A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering. In Proc. 15th Annual IEEE Symp. on Logic in Computer Science, pages 291\u2013302, Santa Barbara, California, June 2000.","DOI":"10.1109\/LICS.2000.855777"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"K. Korovin and A. Voronkov. Knuth-Bendix constraint solving is NP-complete. Preprint CSPP-8, Department of Computer Science, University of Manchester, November 2000.","DOI":"10.1007\/3-540-48224-5_79"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"K. Korovin and A. Voronkov. Verifying orientability of rewrite rules using the knuth-bendix order. Preprint CSPP-11, Department of Computer Science, University of Manchester, March 2001.","DOI":"10.1007\/3-540-45127-7_12"},{"key":"12_CR11","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","volume":"40","author":"M.S. Krishnamoorthy","year":"1985","unstructured":"M.S. Krishnamoorthy and P. Narendran. On recursive path ordering. Theoretical Computer Science, 40:323\u2013328, 1985.","journal-title":"Theoretical Computer Science"},{"key":"12_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/BFb0047120","volume-title":"7th International Conference on Automated Deduction, CADE-7","author":"P. Lescanne","year":"1984","unstructured":"P. Lescanne. Term rewriting systems and algebra. In R.E. Shostak, editor, 7th International Conference on Automated Deduction, CADE-7, volume 170 of Lecture Notes in Computer Science, pages 166\u2013174, 1984."},{"key":"12_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-17220-3_4","volume-title":"Rewriting Techniques and Applications","author":"U. Martin","year":"1987","unstructured":"U. Martin. How to choose weights in the Knuth-Bendix ordering. In Rewriting Techniques and Applications, volume 256 of Lecture Notes in Computer Science, pages 42\u201353, 1987."},{"key":"12_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/10703163_26","volume-title":"Computer Science Logic, 12th International Workshop, CSL\u201998","author":"P. Narendran","year":"1999","unstructured":"P. Narendran, M. Rusinowitch, and R. Verma. RPO constraint solving is in NP. In G. Gottlob, E. Grandjean, and K. Seyr, editors, Computer Science Logic, 12th International Workshop, CSL\u201998, volume 1584 of Lecture Notes in Computer Science, pages 385\u2013398. Springer Verlag, 1999."},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","volume":"47","author":"R. Nieuwenhuis","year":"1993","unstructured":"R. Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters, 47:65\u201369, 1993.","journal-title":"Information Processing Letters"},{"key":"12_CR16","unstructured":"A. Schrijver. Theory of Linear and Integer Programming. John Wiley and Sons, 1998."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45127-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:35:43Z","timestamp":1556667343000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45127-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421177","9783540451273"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45127-7_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}