{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:10Z","timestamp":1749124090783},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:40:57Z","timestamp":1330274457000},"page":"63-77","source":"Crossref","is-referenced-by-count":4,"title":["Termination of constructor systems"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Arts","sequence":"first","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"T. Arts. Termination by absence of infinite chains of dependency pairs. In Proc. Coll. Trees in Algebra and Programming, Link\u00f6ping, Sweden, 1996.","DOI":"10.1007\/3-540-61064-2_38"},{"key":"6_CR2","volume-title":"Technical Report UU-CS-1996-07","author":"T. Arts","year":"1996","unstructured":"T. Arts & J. Giesl. Termination of constructor systems. Technical Report UU-CS-1996-07, Utrecht University, The Netherlands, 1996. Available from http:\/\/www.cs.ruu.nl."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"L. Bachmair & N. Dershowitz. Commutation, transformation and termination. In Proc. 8th CADE, LNCS 230, Oxford, England, 1986.","DOI":"10.1007\/3-540-16780-3_76"},{"key":"6_CR4","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF01810293","volume":"1","author":"F. Bellegarde","year":"1990","unstructured":"F. Bellegarde & P. Lescanne. Termination by completion. Applicable Algebra in Engineering, Communication and Computing, 1:79\u201396, 1990.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/BF01209624","volume":"30","author":"E. Bevers","year":"1993","unstructured":"E. Bevers & J. Lewi. Proving termination of (conditional) rewrite systems. Acta Informatica, 30:537\u2013568, 1993.","journal-title":"Acta Informatica"},{"issue":"2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. B. Cherifa","year":"1987","unstructured":"A. Ben Cherifa & P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137\u2013159, 1987.","journal-title":"Science of Computer Programming"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"S. Biundo, B. Hummel, D. Hutter & C. Walther. The Karlsruhe induction theorem proving system. 8th CADE, LNCS 230, Oxford, England, 1986.","DOI":"10.1007\/3-540-16780-3_132"},{"key":"6_CR8","unstructured":"A. Bouhoula, E. Kounalis & M. Rusinowitch. spike: an automatic theorem prover. In Proceedings of the Conference on Logic Programming and Automated Reasoning, LNAI 624, St. Petersburg, Russia, 1992."},{"key":"6_CR9","unstructured":"R. S. Boyer & J S. Moore. A computational logic. Academic Press, 1979."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn & A. Smaill. The oyster-clam system. In Proc. 10th CADE, LNAI 449, Kaiserslautern, Germany, 1990.","DOI":"10.1007\/3-540-52885-7_123"},{"issue":"5","key":"6_CR11","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/0020-0190(79)90071-1","volume":"9","author":"N. Dershowitz","year":"1979","unstructured":"N. Dershowitz. A note on simplification orderings. Information Processing Letters, 9(5):212\u2013215, 1979.","journal-title":"Information Processing Letters"},{"key":"6_CR12","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":"1","key":"6_CR13","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1, 2):69\u2013115, 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"N. Dershowitz & J.-P. Jouannaud. Rewrite systems. Handbook of Theoret. Comp. Sc., J. van Leeuwen, ed., vol. B, ch. 6, pp. 243\u2013320, Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"2","key":"6_CR15","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","volume":"142","author":"N. Dershowitz","year":"1995","unstructured":"N. Dershowitz & C. Hoot. Natural Termination. Theoretical Computer Science, 142(2):179\u2013207, 1995.","journal-title":"Theoretical Computer Science"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"M. C. F. Ferreira & H. Zantema. Dummy elimination: making termination easier. In Proceedings of the 10th International Conference on Fundamentals of Computation Theory, LNCS 965, Dresden, Germany, 1995","DOI":"10.1007\/3-540-60249-6_56"},{"key":"6_CR17","unstructured":"A. Geser. An improved general path order. Technical Report MIP-9407, Universit\u00e4t Passau, Germany. To appear in Applicable Algebra in Engineering, Communication, and Computation."},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"J. Giesl. Generating polynomial orderings for termination proofs. In Proc. 6th RTA, LNCS 914, Kaiserslautern, Germany, 1995.","DOI":"10.1007\/3-540-59200-8_77"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"J. Giesl. Automated termination proofs with measure functions. In Proc. 19th Annual German Conf. on AI, LNAI 981, Bielefeld, Germany, 1995.","DOI":"10.1007\/3-540-60343-3_33"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"J. Giesl. Termination analysis for functional programs using term orderings. In Proceedings of the Second International Static Analysis Symposium, LNCS 983, Glasgow, Scotland, 1995.","DOI":"10.1007\/3-540-60360-3_38"},{"key":"6_CR21","volume-title":"Rapport Laboria 283","author":"G. Huet","year":"1978","unstructured":"G. Huet & D. S. Lankford. On the uniform halting problem for term rewriting systems. Rapport Laboria 283, Institut de Recherche d'Informatique et d'Automatique, Le Chesnay, France, 1978."},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"D. Kapur & H. Zhang. An overview of Rewrite Rule Laboratory (rrl). In Proc. 3rd RTA, LNCS 355, Chapel Hill, NC, 1989.","DOI":"10.1007\/3-540-51081-8_138"},{"key":"6_CR23","unstructured":"R. Kennaway. Complete term rewrite systems for decimal arithmetic and other total recursive functions. Presented at the Second International Workshop on Termination, La Bresse, France, 1995."},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"D. E. Knuth & P. B. Bendix. Simple word problems in universal algebras. Computational Problems in Abstract Algebra, J. Leech, ed., Pergamon Press, pp. 263\u2013297, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"6_CR25","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/0304-3975(95)00075-8","volume":"151","author":"M. R. K. K. Rao","year":"1995","unstructured":"M. R. K. Krishna Rao. Modular proofs for completeness of hierarchical term rewriting systems. Theoretical Computer Science, 151:487\u2013512, 1995.","journal-title":"Theoretical Computer Science"},{"key":"6_CR26","volume-title":"Tech. Report Memo MTP-3","author":"D. S. Lankford","year":"1979","unstructured":"D. S. Lankford. On proving term rewriting systems are noetherian. Tech. Report Memo MTP-3, Louisiana Tech. University, Ruston, LA, 1979."},{"key":"6_CR27","unstructured":"Z. Manna & S. Ness. On the termination of Markov algorithms. In Proc. of the 3rd Hawaii Int. Conf. on System Science, Honolulu, HI, 1970."},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"U. Martin. How to choose weights in the Knuth-Bendix ordering. In Proc. 2nd RTA, LNCS 256, Bordeaux, France, 1987.","DOI":"10.1007\/3-540-17220-3_4"},{"key":"6_CR29","volume-title":"Report R-78-943","author":"D. A. Plaisted","year":"1978","unstructured":"D. A. Plaisted. A recursively defined ordering for proving termination of term rewriting systems. Report R-78-943, Dept. of Computer Science, University of Illinois, Urbana, IL, 1978."},{"issue":"2\/3","key":"6_CR30","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. A. Plaisted","year":"1985","unstructured":"D. A. Plaisted. Semantic confluence tests and completion methods. Inform. and Control, 65(2\/3):182\u2013215, 1985.","journal-title":"Inform. and Control"},{"key":"6_CR31","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0020-0190(94)90032-9","volume":"49","author":"J. Steinbach","year":"1994","unstructured":"J. Steinbach. Generating polynomial orderings. Information Processing Letters, 49:85\u201393, 1994.","journal-title":"Information Processing Letters"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"J. Steinbach. Automatic termination proofs with transformation orderings. In Proc. 6th RTA, LNCS 914, Kaiserslautern, Germany, 1995.","DOI":"10.1007\/3-540-59200-8_44"},{"key":"6_CR33","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/FI-1995-24123","volume":"24","author":"J. Steinbach","year":"1995","unstructured":"J. Steinbach. Simplification orderings: history of results. Fundamenta Informaticae, 24:47\u201387, 1995.","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"6_CR34","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"C. Walther. On proving the termination of algorithms by machine. Artificial Intelligence, 71(1):101\u2013157, 1994.","journal-title":"Artificial Intelligence"},{"key":"6_CR35","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H. Zantema","year":"1994","unstructured":"H. Zantema. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation 17:23\u201350, 1994.","journal-title":"Journal of Symbolic Computation"},{"key":"6_CR36","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H. Zantema","year":"1995","unstructured":"H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89\u2013105, 1995.","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:32:08Z","timestamp":1619559128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}