{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:16:36Z","timestamp":1725560196585},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_10","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T14:56:52Z","timestamp":1279724212000},"page":"131-148","source":"Crossref","is-referenced-by-count":8,"title":["The Decidability of the First-Order Theory of Knuth-Bendix Order"],"prefix":"10.1007","author":[{"given":"Ting","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Henny B.","family":"Sipma","sequence":"additional","affiliation":[]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1999","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)"},{"issue":"1&2","key":"10_CR2","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0743-1066(95)00033-G","volume":"24","author":"R. Backofen","year":"1995","unstructured":"Backofen, R.: A complete axiomatization of a theory with feature and arity constraints. Journal of Logical Programming\u00a024(1&2), 37\u201371 (1995)","journal-title":"Journal of Logical Programming"},{"issue":"4","key":"10_CR3","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1142\/S0129054190000278","volume":"1","author":"H. Comon","year":"1990","unstructured":"Comon, H.: Solving symbolic ordering constraints. International Journal of Foundations of Computer Science\u00a01(4), 387\u2013411 (1990)","journal-title":"International Journal of Foundations of Computer Science"},{"issue":"2","key":"10_CR4","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation\u00a0112(2), 167\u2013216 (1994)","journal-title":"Information and Computation"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation\u00a07, 371\u2013425 (1989)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0017470","volume-title":"Trees in Algebra and Programming - CAAP 1994","author":"H. Comon","year":"1994","unstructured":"Comon, H., Treinen, R.: Ordering constraints on trees. In: Tison, S. (ed.) CAAP 1994. LNCS, vol.\u00a0787, pp. 1\u201314. Springer, Heidelberg (1994)"},{"issue":"1-2","key":"10_CR7","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/S0304-3975(96)00049-7","volume":"176","author":"H. Comon","year":"1997","unstructured":"Comon, H., Treinen, R.: The first-order theory of lexicographic path orderings is undecidable. Theoretical Computer Science\u00a0176(1-2), 67\u201387 (1997)","journal-title":"Theoretical Computer Science"},{"key":"10_CR8","first-page":"91","volume-title":"Machine Intelligence","author":"D.C. Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Machine Intelligence, vol.\u00a07, pp. 91\u201399. American Elsevier, Amsterdam (1972)"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"7","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science\u00a07, 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"key":"10_CR10","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, London (2001)"},{"key":"10_CR11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574","volume-title":"Model Theory","author":"W. Hodges","year":"1993","unstructured":"Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-54233-7_155","volume-title":"Automata, Languages and Programming","author":"J.-P. Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Okada, M.: Satisfiability of systems of ordinal notation with the subterm property is decidable. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 455\u2013468. Springer, Heidelberg (1991)"},{"doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970);","key":"#cr-split#-10_CR13.1","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"doi-asserted-by":"crossref","unstructured":"Siekmann, J., Wrightson, G. (eds.): Reprinted in Automation of Reasoning, vol.\u00a02, pp. 342\u2013376. Springer, Heidelberg (1983)","key":"#cr-split#-10_CR13.2","DOI":"10.1007\/978-3-642-81955-1"},{"key":"10_CR14","first-page":"291","volume-title":"Proceedings of the 15th IEEE Symposium on Logic in Computer Science (LICS 2000)","author":"K. Korovin","year":"2000","unstructured":"Korovin, K., Voronkov, A.: A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering. In: Proceedings of the 15th IEEE Symposium on Logic in Computer Science (LICS 2000), pp. 291\u2013302. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"979","DOI":"10.1007\/3-540-48224-5_79","volume-title":"Automata, Languages and Programming","author":"K. Korovin","year":"2001","unstructured":"Korovin, K., Voronkov, A.: Knuth-bendix constraint solving is NP-complete. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 979\u2013992. Springer, Heidelberg (2001)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-36206-1_21","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"K. Korovin","year":"2002","unstructured":"Korovin, K., Voronkov, A.: The decidability of the first-order theory of the knuth-bendix order in the case of unary signatures. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 230\u2013240. Springer, Heidelberg (2002)"},{"unstructured":"Kuncak, V., Rinard, M.: On the theory of structural subtyping. Technical Report MIT-LCS-TR-879, Massachusetts Institute of Technology (January 2003)","key":"10_CR17"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/LICS.2003.1210049","volume-title":"Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003)","author":"V. Kuncak","year":"2003","unstructured":"Kuncak, V., Rinard, M.: The structural subtyping of non-recursive types is decidable. In: Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 96\u2013107. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"10_CR19","first-page":"348","volume-title":"Proceedings of the 3th IEEE Symposium on Logic in Computer Science (LICS 1988)","author":"M.J. Maher","year":"1988","unstructured":"Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite tree. In: Proceedings of the 3th IEEE Symposium on Logic in Computer Science (LICS 1988), pp. 348\u2013357. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"10_CR20","first-page":"262","volume-title":"The Metamathematics of Algebraic Systems, Collected Papers, ch.\u00a023","author":"A.I. Mal\u2019cev","year":"1971","unstructured":"Mal\u2019cev, A.I.: Axiomatizable classes of locally free algebras of various types. In: The Metamathematics of Algebraic Systems, Collected Papers, ch.\u00a023, pp. 262\u2013281. North Holland, Amsterdam (1971)"},{"key":"10_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/3-540-44957-4_44","volume-title":"Computational Logic - CL 2000","author":"P. Narendran","year":"2000","unstructured":"Narendran, P., Rusinowitch, M.: The theory of total unary RPO is decidable. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 660\u2013672. Springer, Heidelberg (2000)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/10703163_26","volume-title":"Computer Science Logic","author":"P. Narendran","year":"1999","unstructured":"Narendran, P., Rusinowitch, M., Verma, R.M.: RPO constraint solving is in NP. In: Gottlob, G., Grandjean, E., Seyr, K. (eds.) CSL 1998. LNCS, vol.\u00a01584, pp. 385\u2013398. Springer, Heidelberg (1999)"},{"issue":"2","key":"10_CR23","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","volume":"47","author":"R. Nieuwenhuis","year":"1993","unstructured":"Nieuwenhuis, R.: Robert Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters\u00a047(2), 65\u201369 (1993)","journal-title":"Information Processing Letters"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48685-2_1","volume-title":"Rewriting Techniques and Applications","author":"R. Nieuwenhuis","year":"1999","unstructured":"Nieuwenhuis, R., Rivero, J.: Solved forms for path ordering constraints. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 1\u201315. Springer, Heidelberg (1999)"},{"issue":"4","key":"10_CR25","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., Rubio, A.: Robert Nieuwenhuis and Albert Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computation\u00a019(4), 321\u2013351 (1995)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR26","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/800133.804361","volume-title":"Proceedings of the 10th Annual Symposium on Theory of Computing","author":"C.R. Reddy","year":"1978","unstructured":"Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: Proceedings of the 10th Annual Symposium on Theory of Computing, pp. 320\u2013325. ACM Press, New York (1978)"},{"issue":"2","key":"10_CR27","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1145\/371316.371494","volume":"2","author":"T. Rybina","year":"2001","unstructured":"Rybina, T., Voronkov, A.: A decision procedure for term algebras with queues. ACM Transactions on Computational Logic\u00a02(2), 155\u2013181 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/0747-7171(92)90016-W","volume":"14","author":"R. Treinen","year":"1992","unstructured":"Treinen, R.: A new method for undecidability proofs of first order theories. Journal of Symbolic Computation\u00a014, 437\u2013457 (1992)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-25984-8_9","volume-title":"Automated Reasoning","author":"T. Zhang","year":"2004","unstructured":"Zhang, T., Sipma, H., Manna, Z.: Decision procedures for recursive data structures with integer constraints. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 152\u2013167. Springer, Heidelberg (2004)"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-30142-4_23","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Zhang","year":"2004","unstructured":"Zhang, T., Sipma, H., Manna, Z.: Term algebras with length function and bounded quantifier alternation. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 321\u2013336. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:09:05Z","timestamp":1605625745000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11532231_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}