{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:29:14Z","timestamp":1778300954842,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540563938","type":"print"},{"value":"9783540475491","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56393-8_12","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:07:27Z","timestamp":1330254447000},"page":"155-167","source":"Crossref","is-referenced-by-count":12,"title":["Termination of term rewriting by interpretation"],"prefix":"10.1007","author":[{"given":"H.","family":"Zantema","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"issue":"4","key":"12_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., and L\u00e9vy, J.-J. Explicit substitutions. Journal of Functional Programming 1, 4 (1991), 375\u2013416.","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"12_CR2","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. Ben-Cherifa","year":"1987","unstructured":"Ben-Cherifa, A., and Lescanne, P. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computing Programming 9, 2 (1987), 137\u2013159.","journal-title":"Science of Computing Programming"},{"key":"12_CR3","unstructured":"Curien, P.-L., Hardin, T., and R\u00edos, A. Normalisation forte du calcul des substitutions. Tech. rep., LIENS Ecole Normale Sup\u00e9rieure, 1991."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Dauchet, M. Simulation of Turing machines by a left-linear rewrite rule. In Proceedings of the 3rd Conference on Rewriting Techniques an Applications (1989), N. Dershowitz, Ed., vol. 355 of Lecture Notes in Computer Science, Springer, pp. 109\u2013120.","DOI":"10.1007\/3-540-51081-8_103"},{"issue":"1","key":"12_CR5","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N. Termination of rewriting. Journal of Symbolic Computation 3, 1 and 2 (1987), 69\u2013116.","journal-title":"Journal of Symbolic Computation"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., and Jouannaud, J.-P. Rewrite systems. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed., vol. B. Elsevier, 1990, ch. 6, pp. 243\u2013320.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"8","key":"12_CR7","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., and Manna, Z. Proving termination with multiset orderings. Communications ACM 22, 8 (1979), 465\u2013176.","journal-title":"Communications ACM"},{"key":"12_CR8","unstructured":"Ferreira, M. C. F., and Zantema, H. Total termination of term rewriting. In preparation."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Gnaedig, I., and Lescanne, P. Proving termination of associative commutative rewriting systems by rewriting. In Proceedings of the 8th Conference on Automated Deduction (1986), J. H. Sickmann, Ed., vol. 230 of Lecture Notes in Computer Science, Springer, pp. 52\u201361.","DOI":"10.1007\/3-540-16780-3_79"},{"key":"12_CR10","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0304-3975(86)90035-6","volume":"46","author":"T. Hardin","year":"1986","unstructured":"Hardin, T., and Laville, A. Proof of termination of the rewriting system SUBST on CCL. Theoretical Computer Science 46 (1986), 305\u2013312.","journal-title":"Theoretical Computer Science"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Hofbauer, D. Termination proofs by multiset path orderings imply primitive recursive derivation lengths. In Algebraic and Logic Programming (1990), H. Kirchner and W. Wechler, Eds., vol. 463 of Lecture Notes in Computer Science, Springer, pp. 347\u2013358.","DOI":"10.1007\/3-540-53162-9_50"},{"key":"12_CR12","unstructured":"Huet, G., and Lankford, D. S. On the uniform halting problem for term rewriting systems. Rapport Laboria 283, INRIA, 1978."},{"key":"12_CR13","first-page":"210","volume":"95","author":"J. Kruskal","year":"1960","unstructured":"Kruskal, J. Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture. Trans. American Mathematical Society 95 (1960), 210\u2013225.","journal-title":"Trans. American Mathematical Society"},{"key":"12_CR14","unstructured":"Kuratowski, K., and MosTOWSKi, A. Set Theory. North-Holland Publishing Company, 1968."},{"key":"12_CR15","volume-title":"Tech. Rep. MTP-3","author":"D. S. Lankford","year":"1979","unstructured":"Lankford, D. S. On proving term rewriting systems ar noetherian. Tech. Rep. MTP-3, Louisiana Technical University, Ruston, 1979."},{"key":"12_CR16","unstructured":"Lescanne, P. Termination of rewrite systems by elementary interpretations. Tech. Rep. 91-R-168, CRIN, 1991."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Steinbach, J. Extensions and comparison of simplification orderings. In Proceedings of the 3rd Conference on Rewriting Techniques an Applications (1989), N. Dershowitz, Ed., vol. 355 of Lecture Notes in Computer Science, Springer, pp. 434\u2013448.","DOI":"10.1007\/3-540-51081-8_124"},{"key":"12_CR18","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Toyama, Y. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters 25 (1987), 141\u2013143.","journal-title":"Information Processing Letters"},{"key":"12_CR19","unstructured":"Zantema, H. Termination of term rewriting by interpretation. Tech. Rep. RUU-CS-92-14, Utrecht University, April 1992."}],"container-title":["Lecture Notes in Computer Science","Conditional Term Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56393-8_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T00:50:17Z","timestamp":1619571017000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56393-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540563938","9783540475491"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-56393-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}