{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:43:45Z","timestamp":1750308225904,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,4,1]],"date-time":"2005-04-01T00:00:00Z","timestamp":1112313600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2005,4]]},"abstract":"<jats:p>We show the NP-completeness of the existential theory of term algebras with the Knuth--Bendix order by giving a nondeterministic polynomial-time algorithm for solving Knuth--Bendix ordering constraints.<\/jats:p>","DOI":"10.1145\/1055686.1055692","type":"journal-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:30:55Z","timestamp":1123057855000},"page":"361-388","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Knuth--bendix constraint solving is NP-complete"],"prefix":"10.1145","volume":"6","author":[{"given":"Konstantin","family":"Korovin","sequence":"first","affiliation":[{"name":"Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[{"name":"The University of Manchester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press Cambridge mass.]]   Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press Cambridge mass.]]","DOI":"10.1017\/CBO9781139172752"},{"volume-title":"Model Theory and its Applications. Trudy Instituta Matematiki","author":"Belegradek O.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054190000278"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80017-3"},{"volume":"787","volume-title":"Trees in Algebra and Programming: CAAP'94","author":"Comon H.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00049-7"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90026-3"},{"volume":"202","volume-title":"First International Conference, RTA-85","author":"Detlefs D.","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2697758.2698069"},{"volume":"2002","volume-title":"Eds. Lecture Notes in Computer Science","author":"Ganzinger H.","key":"e_1_2_1_10_1"},{"volume-title":"Model theory","author":"Hodges W.","key":"e_1_2_1_11_1"},{"volume":"510","volume-title":"18th International Colloquium, ICALP'91","author":"Jouannaud J.-P.","key":"e_1_2_1_12_1"},{"volume-title":"-J","year":"1980","author":"Kamin S.","key":"e_1_2_1_13_1"},{"volume-title":"Constraint Programming: Basics and Tools","author":"Kirchner H.","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Knuth D. and Bendix P. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra J. Leech Ed. Pergamon Press Oxford 263--297.]]  Knuth D. and Bendix P. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra J. Leech Ed. Pergamon Press Oxford 263--297.]]","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"volume-title":"Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, (LICS'00)","author":"Korovin K.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","volume-title":"12th International Conference, RTA 2001, A. Middeldorp, Ed. Lecture Notes in Computer Science","volume":"2051","author":"Korovin K.","year":"2003"},{"volume":"2556","volume-title":"Proceedings of the 22th Conference on Foundations of Software Technology and Theoretical Computer Science, (FSTTCS'02)","author":"Korovin K.","key":"e_1_2_1_18_1"},{"volume-title":"Proceedings of the 18th IEEE Symposium on Logic in Computer Science, (LICS'03)","author":"Korovin K.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00021-X"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/6400.6416"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(87)90007-0"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00015-9"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 7th International Conference on Automated Deduction, CADE-7, R. Shostak, Ed. Lecture Notes in Computer Science","volume":"170","author":"Lescanne P.","year":"1984"},{"key":"e_1_2_1_25_1","first-page":"2","article-title":"A phytography of WALDMEISTER","volume":"15","author":"L\u00f6chner B.","year":"2002","journal-title":"AI Commun."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5132"},{"key":"e_1_2_1_27_1","first-page":"768","article-title":"On the elementary theories of locally free universal algebras","volume":"2","author":"Ma\u013acev A.","year":"1961","journal-title":"Soviet Math. Dokl."},{"volume-title":"Rewriting Technics and Applications","series-title":"Lecture Notes in Computer Science","author":"Martin U.","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647482.728450"},{"volume":"1584","volume-title":"12th International Workshop, CSL'98, G. Gottlob, E. Grandjean, and K. Seyr, Eds. Lecture Notes in Computer Science","author":"Narendran P.","key":"e_1_2_1_30_1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90226-Y"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753620"},{"volume":"1631","volume-title":"Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA)","author":"Nieuwenhuis R.","key":"e_1_2_1_33_1"},{"key":"e_1_2_1_34_1","first-page":"371","article-title":"Paramodulation--based theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier Science, Amsterdam, The Netherlands","volume":"7","author":"Nieuwenhuis R.","year":"2001","journal-title":"Chap."},{"key":"e_1_2_1_35_1","first-page":"2","article-title":"The design and implementation of Vampire","volume":"15","author":"Riazanov A.","year":"2002","journal-title":"AI Commun."},{"key":"e_1_2_1_36_1","first-page":"2","article-title":"E---A brainiac theorem prover","volume":"15","author":"Schulz S.","year":"2002","journal-title":"AI Commun."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/23005.24037"},{"volume":"1632","volume-title":"16th International Conference on Automated Deduction","author":"Weidenbach C.","key":"e_1_2_1_38_1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1055686.1055692","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1055686.1055692","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:28Z","timestamp":1750264288000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1055686.1055692"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,4]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["10.1145\/1055686.1055692"],"URL":"https:\/\/doi.org\/10.1145\/1055686.1055692","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2005,4]]},"assertion":[{"value":"2005-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}