{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:40:12Z","timestamp":1737063612815,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_44","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T05:24:41Z","timestamp":1180675481000},"page":"660-672","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["The Theory of Total Unary RPO Is Decidable"],"prefix":"10.1007","author":[{"given":"Paliath","family":"Narendran","sequence":"first","affiliation":[]},{"given":"Michael","family":"Rusinowitch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"unstructured":"R. Caferra and N. Peltier. Disinference rules, model building and abduction. Logic at work: Essays dedicated to the memory of Helena Rasiowa(Part 5: Logic in Computer Science, Chap. 20). Physica-Verlag, 1998.","key":"44_CR1"},{"key":"44_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/3-540-56868-9_25","volume-title":"Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada)","author":"A.-C. Caron","year":"1993","unstructured":"A-C. Caron, J-L. Coquide, and M. Dauchet. Encompassment properties and automata with constraints. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada),volume 690 of Lecture Notes in Computer Science, pages 328\u2013342. Springer-Verlag, 1993."},{"unstructured":"H. Comon. Solving inequations in term algebras. In Proc. 5th IEEE Symposium on Logic in Computer Science (LICS), Philadelphia, June1990.","key":"44_CR3"},{"unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi. Tree Automata Techniques and Applications. http:\/\/www.grappa.univ-lille3.fr\/tata\/","key":"44_CR4"},{"doi-asserted-by":"crossref","unstructured":"H. Comon, P. Narendran, R. Nieuwenhuis, and M. Rusinowitch. Decision problems in ordered rewriting. In Proc. 13th IEEE Symp. Logic in Computer Science (LICS\u201998), Indianapolis, IN, USA, June 1998, pages 276\u2013286, 1998.","key":"44_CR5","DOI":"10.1109\/LICS.1998.705664"},{"doi-asserted-by":"crossref","unstructured":"H. Comon and R. Treinen. The first-order theory of lexicographic path orderings is undecidable. Theoretical Computer Science 176, April 1997.","key":"44_CR6","DOI":"10.1016\/S0304-3975(96)00049-7"},{"issue":"3","key":"44_CR7","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(3): 279\u2013301. 1982.","journal-title":"Theoretical Computer Science"},{"key":"44_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-54233-7_155","volume-title":"18th International Colloquium on Automata, Languages and Programming (ICALP)","author":"J.-P. Jouannaud","year":"1991","unstructured":"J.-P. Jouannaud and M. Okada. Satisfiability of systems of ordinal notations with the subterm ordering is decidable. In 18th International Colloquium on Automata, Languages and Programming (ICALP), volume 510 of Lecture Notes in Computer Science, pages 455\u2013468, Madrid, Spain, July 1991. Springer-Verlag."},{"key":"44_CR9","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF01893885","volume":"28","author":"D. Kapur","year":"1991","unstructured":"D. Kapur, P. Narendran, D. Rosenkrantz and H. Zhang. Sufficient Completeness, Ground-Reducibility and Their Complexity. Acta Informatica 28 (1991) 311\u2013350.","journal-title":"Acta Informatica"},{"key":"44_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/3-540-15198-2_11","volume-title":"10th CAAP","author":"D. Kapur","year":"1985","unstructured":"D. Kapur, P. Narendran and G. Sivakumar. A path ordering for proving termination of term rewriting systems. In H. Ehrig (ed.), 10th CAAP, volume 185 of Lecture Notes in Computer Science, pages 173\u2013187, Berlin, March 1985."},{"issue":"2","key":"44_CR11","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D. Kapur","year":"1995","unstructured":"D. Kapur and H. Zhang. An Overview of Rewrite Rule Laboratory (RRL), J. of Computer and Mathematics with Applications, 29,2, 1995, 91\u2013114.","journal-title":"J. of Computer and Mathematics with Applications"},{"issue":"3","key":"44_CR12","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue Franaise d\u2019Intelligence Artificielle, 4(3):9\u201352, 1990. Special issue on automatic deduction.","journal-title":"Revue Franaise d\u2019Intelligence Artificielle"},{"issue":"4","key":"44_CR13","first-page":"331","volume":"16","author":"P. Lescanne","year":"1982","unstructured":"P. Lescanne. Some properties of the Decomposition Ordering, a simplification ordering to prove termination of rewriting systems. RAIRO, 16(4):331\u2013347, 1982.","journal-title":"RAIRO"},{"key":"44_CR14","doi-asserted-by":"publisher","first-page":"624","DOI":"10.2307\/2275551","volume":"62","author":"U. Martin","year":"1997","unstructured":"U. Martin and E. Scott. The order types of termination orderings on monadic terms, strings and multisets. J. Symbolic Logic 62 (1997) 624\u2013635.","journal-title":"J. Symbolic Logic"},{"key":"44_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Computer Science Logic (CSL 98)","author":"P. Narendran","year":"1998","unstructured":"P. Narendran, M. Rusinowitch and R. Verma. RPO constraint solving is in NP. In: Computer Science Logic (CSL 98), Brno, Czech Republic. August 1998. 12p. LNCS 1584, Springer-Verlag, 1999."},{"key":"44_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61398-6","volume-title":"Automated Deduction in Equational Logic and Cubic Curves","author":"W. McCune","year":"1996","unstructured":"W. McCune and R. Padmanabhan. Automated Deduction in Equational Logic and Cubic Curves, Springer-Verlag LNCS 1095 (1996)"},{"doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis. Simple LPO constraint solving methods. Inf. Process. Lett. 47(2):65\u201369, Aug. 1993.","key":"44_CR17","DOI":"10.1016\/0020-0190(93)90226-Y"},{"key":"44_CR18","series-title":"Lecture Notes in Artificial Intelligence","first-page":"477","volume-title":"Proceedings of 11th Conf. on Automated Deduction","author":"R. Nieuwenhuis","year":"1992","unstructured":"R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In D. Kapur, editor, Proceedings of 11th Conf. on Automated Deduction, Saratoga Springs, NY, 1992, volume 607 of Lecture Notes in Artificial Intelligence, pages 477\u2013491, June 1992, Springer-Verlag."},{"key":"44_CR19","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"D. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182\u2013215, 1985.","journal-title":"Information and Control"},{"key":"44_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/3-540-51081-8_124","volume-title":"Proceedings of 3rd RTA","author":"J. Steinbach","year":"1989","unstructured":"J. Steinbach. Extensions and comparison of simplification orderings. Proceedings of 3rd RTA, Chapel Hill, NC, volume 355 of Lecture Notes in Computer Science, pages 434\u2013448, 1989, Springer-Verlag."},{"unstructured":"C. Weidenbach. SPASS: Combining Superposition, Sorts and Splitting in A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, Elsevier, 1999. To appear.","key":"44_CR21"}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:04:41Z","timestamp":1737061481000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_44","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"15 December 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}