{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:57:04Z","timestamp":1781927824984,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540422877","type":"print"},{"value":"9783540482246","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-48224-5_79","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T02:29:04Z","timestamp":1193538544000},"page":"979-992","source":"Crossref","is-referenced-by-count":14,"title":["Knuth-Bendix Constraint Solving Is NP-Complete"],"prefix":"10.1007","author":[{"given":"Konstantin","family":"Korovin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"79_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and and All That","author":"F. Baader","year":"1998","unstructured":"F. Baader and T. Nipkow. Term Rewriting and and All That. Cambridge University press, Cambridge, 1998."},{"issue":"4","key":"79_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":"79_CR3","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17:279\u2013301, 1982.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"79_CR4","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"Th. Hillenbrand","year":"1997","unstructured":"Th. Hillenbrand, A. Buch, R. Vogt, and B. L\u00f6chner. Waldmeister: High-performance equational deduction. Journal of Automated Reasoning, 18(2):265\u2013270, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"79_CR5","doi-asserted-by":"crossref","unstructured":"W. Hodges. Model theory. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511551574"},{"key":"79_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-54233-7_155","volume-title":"Automata, Languages and Programming, 18th International Colloquium, ICALP\u201991","author":"J.-P. Jouannaud","year":"1991","unstructured":"J.-P. Jouannaud and M. Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In J.L. Albert, B. Monien, and M. Rodr\u00f3guez-Artalejo, editors, Automata, Languages and Programming, 18th International Colloquium, ICALP\u201991, volume 510 of Lecture Notes in Computer Science, pages 455\u2013468, Madrid, Spain, 1991. Springer Verlag."},{"key":"79_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/3-540-59155-9_8","volume-title":"Constraint Programming: Basics and Tools","author":"H. Kirchner","year":"1995","unstructured":"H. Kirchner. On the use of constraints in automated deduction. In A. Podelski, editor, Constraint Programming: Basics and Tools, volume 910 of Lecture Notes in Computer Science, pages 128\u2013146. Springer Verlag, 1995."},{"key":"79_CR8","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":"79_CR9","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":"79_CR10","series-title":"Preprint CSPP-8","volume-title":"Knuth-Bendix constraint solving is NP-complete","author":"K. Korovin","year":"2000","unstructured":"K. Korovin and A. Voronkov. Knuth-Bendix constraint solving is NP-complete. Preprint CSPP-8, Department of Computer Science, University of Manchester, February 2000."},{"key":"79_CR11","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":"79_CR12","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":"79_CR13","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis. Rewrite-based deduction and symbolic constraints. In H. Ganzinger, editor, Automated Deduction\u2014CADE-16. 16th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 302\u2013313, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48660-7_28"},{"key":"79_CR14","doi-asserted-by":"crossref","unstructured":"A. Riazanov and A. Voronkov. Vampire. In H. Ganzinger, editor, Automated Deduction\u2014CADE-16. 16th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 292\u2013296, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48660-7_26"},{"key":"79_CR15","doi-asserted-by":"crossref","unstructured":"S. Schulz. System abstract: E 0.3. In H. Ganzinger, editor, Automated Deduction\u2014 CADE-16. 16th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 297\u2013301, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48660-7_27"},{"key":"79_CR16","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, and D. Topic. System description: Spass version 1.0.0. In H. Ganzinger, editor, Automated Deduction\u2014CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 378\u2013382, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48660-7_34"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48224-5_79","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:28:23Z","timestamp":1556922503000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48224-5_79"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422877","9783540482246"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48224-5_79","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}