{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:05Z","timestamp":1763467745687},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643012"},{"type":"electronic","value":"9783540697213"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0052376","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T01:31:11Z","timestamp":1149643871000},"page":"271-285","source":"Crossref","is-referenced-by-count":6,"title":["Towards automated termination proofs through \u201cfreezing\u201d"],"prefix":"10.1007","author":[{"given":"Hongwei","family":"Xi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"T. Arts and J. Giesl. Termination of constructor systems. In Proceedings of the Seventh Conference on Rewriting Techniques and Applications, vol. 1103 of Lecture Notes in Computer Science, pp. 63\u201377, New Brunswick, USA, 1996.","DOI":"10.1007\/3-540-61464-8_43"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"T. Arts and J. Giesl. Automatically Proving Termination Where Simplification Orderings Fail. In Proc. Colloquium on Trees in Algebra and Programming, vol. 1214 of Lecture Notes in Computer Science, pp. 261\u2013272, Lille, France, 1997.","DOI":"10.1007\/BFb0030602"},{"key":"21_CR3","unstructured":"L. Bachmair and N. Dershowitz. Communication, transformation and termination. In Proceedings of the Eighth CADE, vol. 230 of Lecture Notes in Computer Science, pp. 52\u201360, Oxford, July 1986."},{"key":"21_CR4","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF01810293","volume":"1","author":"F. Bellegarde","year":"1990","unstructured":"F. Bellegarde and P. Lescanne. Termination by completion. Applicable Algebra in Engineering, Communication and Computing, vol. 1, pp. 79\u201396, 1990.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"issue":"3","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. TCS, 17(3), pp. 279\u2013301, 1982.","journal-title":"TCS"},{"key":"21_CR6","doi-asserted-by":"publisher","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, vol. 3, pp.69\u2013116, 1987.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"21_CR7","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 and C. Hoot. Natural Termination, TCS, 142(2), pp. 179\u2013207, 1995.","journal-title":"TCS"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems. In I. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"21_CR9","first-page":"162","volume":"43","author":"N. Dershowitz","year":"1991","unstructured":"N. Dershowitz and Jean-Pierre Jouannaud. Notations for rewriting. EATCS, vol. 43, pp. 162\u2013172, 1991.","journal-title":"EATCS"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"M. Ferreira. Dummy Elimination in Equational Rewriting. In Proceedings of the Seventh Conference on Rewriting Techniques and Applications, vol. 1103 of Lecture Notes in Computer Science, pp. 78\u201392, New Brunswick, USA, 1996.","DOI":"10.1007\/3-540-61464-8_44"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"M. Ferreira and H. Zantema. Dummy Elimination: making termination easier. In Proceedings of the 10th International Conference on Fundamentals of Computation Theory, LNCS 965, Dresden, 1995.","DOI":"10.1007\/3-540-60249-6_56"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"J. Giesl. Automated termination proofs with measure function. In Proceedings of 19th Annual German Conference on AI, LNAI 981, Bielefeld, 1995.","DOI":"10.1007\/3-540-60343-3_33"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"M. Hanus. The integration of functions into logic programming: From theory to practice. In JLOGP, vol. 19\u201320, pp. 583\u2013628.","DOI":"10.1016\/0743-1066(94)90034-5"},{"key":"21_CR14","volume-title":"Technical Report 283","author":"G. Hu\u00e9t","year":"1978","unstructured":"G. Hu\u00e9t and D. Lankford. On the uniform halting problem for term rewriting systems. Technical Report 283, INRIA, Le Chesnay, France, 1978."},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebras. Computational Problems in Abstract Algebra, edited by J. Leech, Pergamon Press, pp. 263\u2013297, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"21_CR16","unstructured":"R. Kennaway. Complete term rewrite systems for decimal arithmetic and other total recursive functions. Presented at the 2nd International Workshop on termination, La Bresse, 1995"},{"key":"21_CR17","unstructured":"D. Lankford. On proving term rewriting systems are noetherian. Tech. Report Memo MTP-3, Louisiana Tech. University, 1979."},{"key":"21_CR18","volume-title":"Tech. report UIUC DCS-R-78-943","author":"D. Plaisted","year":"1978","unstructured":"D. Plaisted. A recursively defined ordering for proving termination of term rewriting systems. Tech. report UIUC DCS-R-78-943, Univ. of Illinois, Urbana, 1978."},{"key":"21_CR19","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, vol. 24, pp. 47\u201387, 1995.","journal-title":"Fundamenta Informaticae"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"J. Steinbach. Automatic termination proofs with transformation orderings. In Proceedings of the Sixth RTA, vol. 914 of Lecture Notes in Computer Science, pp. 11\u201325, 1995.","DOI":"10.1007\/3-540-59200-8_44"},{"key":"21_CR21","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, vol. 17, pp. 23\u201350, 1994.","journal-title":"Journal of Symbolic Computation"},{"key":"21_CR22","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, vol. 24, pp 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\/BFb0052376","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T05:13:35Z","timestamp":1586927615000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0052376","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}