{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:10:22Z","timestamp":1737436222922,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540002253"},{"type":"electronic","value":"9783540362067"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36206-1_21","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T07:23:08Z","timestamp":1187248988000},"page":"230-240","source":"Crossref","is-referenced-by-count":1,"title":["The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures"],"prefix":"10.1007","author":[{"given":"Konstantin","family":"Korovin","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"21_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":"21_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":"21_CR3","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tom-masi. Tree automata techniques and applications. Available on: http:\/\/www.grappa.univ-lille3.fr\/tata , 1997."},{"issue":"1\u20132","key":"21_CR4","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/S0304-3975(96)00049-7","volume":"176","author":"H. Comon","year":"1997","unstructured":"H. Comon and R. Treinen. The first-order theory of lexicographic path orderings is undecid-able. Theoretical Computer Science, 176(1\u20132):67\u201387, 1997.","journal-title":"Theoretical Computer Science"},{"key":"21_CR5","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"},{"key":"21_CR6","unstructured":"Yuri Ershov. Problems of decidability and constructive models. Nauka, 1980. (in Russian)."},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"W. Hodges. Model theory. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511551574"},{"key":"21_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-54233-7_155","volume-title":"Satisfiability of systems of ordinal notations with the sub-term property is decidable","author":"J.-P. Jouannaud","year":"1991","unstructured":"J.-P. Jouannaud and M. Okada. Satisfiability of systems of ordinal notations with the sub-term property is decidable. In Automata, Languages and Programming, 18th International Colloquium (ICALP), volume 510 of Lecture Notes in Computer Science, pages 455\u2013468, 1991."},{"key":"21_CR9","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":"21_CR10","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":"21_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"979","DOI":"10.1007\/3-540-48224-5_79","volume-title":"Knuth-bendix ordering constraint solving is NP-complete","author":"K. Korovin","year":"2001","unstructured":"K. Korovin and A. Voronkov. Knuth-bendix ordering constraint solving is NP-complete. In F. Orejas, P.G. Spirakis, and J. van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, volume 2076 of Lecture Notes in Computer Science, pages 979\u2013992. Springer Verlag, 2001."},{"key":"21_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-45127-7_12","volume-title":"Verifying orientability of rewrite rules using the Knuth-Bendix order","author":"K. Korovin","year":"2001","unstructured":"K. Korovin and A. Voronkov. Verifying orientability of rewrite rules using the Knuth-Bendix order. In A. Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, volume 2051 of Lecture Notes in Computer Science, pages 137\u2013153. Springer Verlag, 2001."},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"M. Maher. Complete axiomatizations of the algebras of finite, rational and infi nite trees. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 348\u2013357, 1988.","DOI":"10.1109\/LICS.1988.5132"},{"key":"21_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1007\/3-540-44957-4_44","volume-title":"The theory of total unary rpo is decidable","author":"Narendran","year":"2000","unstructured":"Narendran and Rusinowitch. The theory of total unary rpo is decidable. In First International Conference on Computational Logic, volume 1861 of Lecture Notes in Computer Science, pages 660\u2013672, 2000."},{"key":"21_CR15","series-title":"Lect Notes Comput Sci","first-page":"385","volume-title":"RPO constraint solving is in NP","author":"Narendran","year":"1998","unstructured":"Narendran, Rusinowitch, and Verma. RPO constraint solving is in NP. In CSL: 12thWorkshop on Computer Science Logic, volume 1584, pages 385\u2013398. LNCS, Springer-Verlag, 1998."},{"key":"21_CR16","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":"21_CR17","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Solved forms for path ordering constraints","author":"R. Nieuwenhuis","year":"1999","unstructured":"R. Nieuwenhuis and J.M. Rivero. Solved forms for path ordering constraints. In In Proc. 10th International Conference on Rewriting Techniques and Applications (RTA), volume 1631 of Lecture Notes in Computer Science, pages 1\u201315, Trento, Italy, 1999."},{"key":"21_CR18","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1016\/S0049-237X(08)71116-9","volume-title":"Handbook of Mathematical Logic","author":"M. O. Rabin","year":"1977","unstructured":"Michael O. Rabin. Decidable theories. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter C.3, pages 595\u2013629. North-Holland, Amsterdam, 1977."},{"issue":"1","key":"21_CR19","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J. W. Thatcher","year":"1968","unstructured":"James W. Thatcher and Jesse B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2( 1): 57\u201381,1968.","journal-title":"Mathematical Systems Theory"},{"key":"21_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/3-540-53487-3_34","volume-title":"A new method for undecidability proofs of first order theories","author":"R. Treinen","year":"1990","unstructured":"Ralf Treinen. A new method for undecidability proofs of first order theories. In Foundations of Software Technology and Theoretical Computer Science,(FSTTCS), 10th conference, volume 472 of Lecture Notes in Computer Science, pages 48\u201362, 1990. (journal version [21])."},{"issue":"5","key":"21_CR21","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/0747-7171(92)90016-W","volume":"14","author":"R. Treinen","year":"1992","unstructured":"Ralf Treinen. A new method for undecidablity proofs of first order theories. Journal of Symbolic Computations, 14(5):437\u2013458, 1992.","journal-title":"Journal of Symbolic Computations"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36206-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T11:23:07Z","timestamp":1737372187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36206-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540002253","9783540362067"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-36206-1_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}