{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:53:53Z","timestamp":1762458833328},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540226710"},{"type":"electronic","value":"9783540277750"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27775-0_1","type":"book-chapter","created":{"date-parts":[[2010,9,15]],"date-time":"2010-09-15T20:29:36Z","timestamp":1284582576000},"page":"1-18","source":"Crossref","is-referenced-by-count":6,"title":["Termination by Abstraction"],"prefix":"10.1007","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-60939-3_17","volume-title":"Logic Program Synthesis and Transformation","author":"T. Arts","year":"1996","unstructured":"Arts, T., Zantema, H.: Termination of logic programs using semantic unification. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol.\u00a01048, pp. 219\u2013233. Springer, Heidelberg (1996)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/3-540-16780-3_76","volume-title":"8th International Conference on Automated Deduction","author":"L. Bachmair","year":"1986","unstructured":"Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 5\u201320. Springer, Heidelberg (1986)"},{"issue":"2","key":"1_CR4","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF01810293","volume":"1","author":"F. Bellegarde","year":"1990","unstructured":"Bellegarde, F., Lescanne, P.: Termination by completion. Applied Algebra on Engineering, Communication and Computer Science\u00a01(2), 79\u201396 (1990)","journal-title":"Applied Algebra on Engineering, Communication and Computer Science"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/10721959_27","volume-title":"Automated Deduction - CADE-17","author":"C. Borralleras","year":"2000","unstructured":"Borralleras, C., Ferreira, M., Rubio, A.: Complete monotonic semantic path orderings. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 346\u2013364. Springer, Heidelberg (2000)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/3-540-53904-2_90","volume-title":"Rewriting Techniques and Applications","author":"J. Chabin","year":"1991","unstructured":"Chabin, J., R\u00e9ty, P.: Narrowing directed by a graph of terms. In: Book, R.V. (ed.) RTA 1991. LNCS, vol.\u00a0488, pp. 112\u2013123. Springer, Heidelberg (1991)"},{"key":"1_CR7","unstructured":"Codish, M., Genaim, S., Bruynooghe, M., Gallagher, J., Vanhoof, W.: One loop at a time. In: 6th International Workshop on Termination, WST 2003 (June 2003)"},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0743-1066(99)00006-0","volume":"41","author":"M. Codish","year":"1999","unstructured":"Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. J. Logic Programming\u00a041(1), 103\u2013123 (1999)","journal-title":"J. Logic Programming"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P.M. Cousot","year":"1977","unstructured":"Cousot, P.M., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"1_CR10","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0743-1066(94)90027-2","volume":"19\/20","author":"D. Schreye De","year":"1993","unstructured":"De Schreye, D., Decorte, S.: Termination of logic programs: The neverending story. J. Logic Programming\u00a019\/20, 199\u2013260 (1993)","journal-title":"J. Logic Programming"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1007\/3-540-10843-2_36","volume-title":"Automata, Languages and Programming","author":"N. Dershowitz","year":"1981","unstructured":"Dershowitz, N.: Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol.\u00a0115, pp. 448\u2013458. Springer, Heidelberg (1981)"},{"issue":"3","key":"1_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science\u00a017(3), 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"issue":"1&2","key":"1_CR13","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symbolic Computation\u00a03(1&2), 69\u2013115 (1987)","journal-title":"J. Symbolic Computation"},{"issue":"2","key":"1_CR14","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","volume":"142","author":"N. Dershowitz","year":"1995","unstructured":"Dershowitz, N., Hoot, C.: Natural termination. Theoretical Computer Science\u00a0142(2), 179\u2013207 (1995)","journal-title":"Theoretical Computer Science"},{"key":"1_CR15","series-title":"Formal Methods and Semantics","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, vol.\u00a0B, ch. 6, pp. 243\u2013320. North-Holland, Amsterdam (1990)"},{"issue":"1\/2","key":"1_CR16","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s002000100065","volume":"12","author":"N. Dershowitz","year":"2001","unstructured":"Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing\u00a012(1\/2), 117\u2013156 (2001)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"issue":"8","key":"1_CR17","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM\u00a022(8), 465\u2013476 (1979)","journal-title":"Communications of the ACM"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-19242-5_3","volume-title":"Conditional Term Rewriting Systems","author":"N. Dershowitz","year":"1988","unstructured":"Dershowitz, N., Okada, M., Sivakumar, G.: Confluence of conditional rewrite systems. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol.\u00a0308, pp. 31\u201344. Springer, Heidelberg (1988)"},{"key":"1_CR19","first-page":"21","volume-title":"Machine Intelligence 11: The logic and acquisition of knowledge","author":"N. Dershowitz","year":"1988","unstructured":"Dershowitz, N., Plaisted, D.A.: Equational programming. In: Hayes, J.E., Michie, D., Richards, J. (eds.) Machine Intelligence 11: The logic and acquisition of knowledge, ch.\u00a02, pp. 21\u201356. Oxford Press, Oxford (1988)"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1016\/B978-044450813-3\/50011-4","volume-title":"Handbook of Automated Reasoning","author":"N. Dershowitz","year":"2001","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 9, pp. 535\u2013610. Elsevier Science, Amsterdam (2001)"},{"key":"1_CR21","first-page":"166","volume-title":"Proceedings of the Seventh National Conference on Artificial Intelligence","author":"N. Dershowitz","year":"1988","unstructured":"Dershowitz, N., Sivakumar, G.: Goal-directed equation solving. In: Proceedings of the Seventh National Conference on Artificial Intelligence, St. Paul, MN, August 1988, pp. 166\u2013170. AAAI, Menlo Park (1988)"},{"key":"1_CR22","series-title":"Mathematical Aspects of Computer Science","first-page":"19","volume-title":"Proceedings of Symposia in Applied Mathematics","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics, Providence, RI. Mathematical Aspects of Computer Science, vol.\u00a0XIX, pp. 19\u201332. American Mathematical Society, Providence (1967)"},{"issue":"6","key":"1_CR23","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/BF01293264","volume":"7","author":"A. Geser","year":"1996","unstructured":"Geser, A.: An improved general path order. Applicable Algebra in Engineering, Communication, and Computing\u00a07(6), 469\u2013511 (1996)","journal-title":"Applicable Algebra in Engineering, Communication, and Computing"},{"key":"1_CR24","unstructured":"Geupel, O.: Overlap closures and termination of term rewriting systems. Report MIP-8922, Universit\u00e4t Passau, Passau, West Germany (July 1989)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45127-7_9","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 93\u2013107. Springer, Heidelberg (2001)"},{"issue":"2","key":"1_CR26","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357073.357080","volume":"1","author":"D. Gries","year":"1979","unstructured":"Gries, D.: Is sometime ever better than alway? ACM Transactions on Programming Languages and Systems\u00a01(2), 258\u2013265 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR27","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/0743-1066(94)90034-5","volume":"19&20","author":"M. Hanus","year":"1994","unstructured":"Hanus, M.: The integration of functions into logic programming: From theory to practice. J. Logic Programming\u00a019&20, 583\u2013628 (1994)","journal-title":"J. Logic Programming"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol.\u00a087, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"key":"1_CR29","unstructured":"Kamin, S., L\u00e9vy, J.-J.: Two generalizations of the recursive path ordering, February 1980. Unpublished note, Department of Computer Science, University of Illinois, Urbana, IL. Available at http:\/\/www.ens-lyon.fr \/ LIP \/ REWRITING \/ OLD PUBLICATIONS ON TERMINATION \/ KAMIN LEVY (viewed June 2004)"},{"issue":"4","key":"1_CR30","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00264565","volume":"5","author":"S.M. Katz","year":"1975","unstructured":"Katz, S.M., Manna, Z.: A closer look at termination. Acta Informatica\u00a05(4), 333\u2013352 (1975)","journal-title":"Acta Informatica"},{"key":"1_CR31","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1112\/blms\/14.4.285","volume":"14","author":"L. Kirby","year":"1982","unstructured":"Kirby, L., Paris, J.: Accessible independence results for Peano arithmetic. Bulletin London Mathematical Society\u00a014, 285\u2013293 (1982)","journal-title":"Bulletin London Mathematical Society"},{"key":"1_CR32","unstructured":"Lankford, D.S.: On proving term rewriting systems are Noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech. University, Ruston, LA (May 1979) (revised October 1979)"},{"key":"#cr-split#-1_CR33.1","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Conference Record of the Twenty-Eighth Symposium on Principles of Programming Languages, London, UK, January 2001, vol.\u00a036(3), pp. 81\u201392 (2001);","DOI":"10.1145\/360204.360210"},{"key":"#cr-split#-1_CR33.2","unstructured":"ACM SIGPLAN Notices"},{"key":"1_CR34","volume-title":"Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Manna, Z.: Mathematical Theory of Computation. McGraw-Hill, New York (1974)"},{"key":"1_CR35","unstructured":"Middeldorp, A.: Personal communication (June 2003)"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","first-page":"270","volume-title":"Rewriting Techniques and Applications","author":"E. Ohlebusch","year":"1999","unstructured":"Ohlebusch, E., Claves, C., March\u00e9, C.: TALP: A tool for the termination analysis of logic programs. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 270\u2013273. Springer, Heidelberg (1999)"},{"issue":"2\/3","key":"1_CR37","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D.A. Plaisted","year":"1985","unstructured":"Plaisted, D.A.: Semantic confluence tests and completion methods. Information and Control\u00a065(2\/3), 182\u2013215 (1985)","journal-title":"Information and Control"},{"key":"1_CR38","first-page":"518","volume-title":"Logic Programming: Proceedings of the 1991 International Symposium","author":"Y. Sagiv","year":"1991","unstructured":"Sagiv, Y.: A termination test for logic programs. In: Logic Programming: Proceedings of the 1991 International Symposium, San Diego, CA, October 1991, pp. 518\u2013532. MIT Press, Cambridge (1991)"},{"key":"1_CR39","unstructured":"Serebrenik, A.: Termination Analysis of Logic Programs. PhD thesis, Katholieke Universiteit Leuven, Leuven, Belgium (July 2003)"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Sintzoff, M.: Calculating properties of programs by valuations on specific models. In: Proceedings of the ACM Conference on Proving Assertions About Programs, January 1972, vol.\u00a07(1), pp. 203\u2013207 (1972)","DOI":"10.1145\/800235.807086"},{"issue":"2","key":"1_CR41","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. Journalof Symbolic Logic\u00a032(2), 198\u2013212 (1967)","journal-title":"Journalof Symbolic Logic"},{"key":"1_CR42","unstructured":"Terese. In: Bezem, M., Klop, J.W., de Vrijer, R. (eds.) Term Rewriting Systems, Cambridge University Press, Cambridge (2002)"},{"key":"1_CR43","unstructured":"Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, Cambridge, England, pp. 67\u201369 (1949), University Mathematics Laboratory"},{"key":"1_CR44","first-page":"301","volume-title":"Proceeedings of the Eighth International Conference on Logic Programming","author":"K. Vershaetse","year":"1991","unstructured":"Vershaetse, K., De Schreye, D.: Deriving termination proofs for logic programs, using abstract procedures. In: Furukawa, K. (ed.) Proceeedings of the Eighth International Conference on Logic Programming, Cambridge, MA, pp. 301\u2013315. The MIT Press, Cambridge (1991)"},{"issue":"3","key":"1_CR45","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1109\/TSE.1975.6312852","volume":"SE-1","author":"B. Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Property extraction in well-founded property sets. IEEE Transactions on Software Engineering\u00a0SE-1(3), 270\u2013285 (1975)","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27775-0_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:24:31Z","timestamp":1620012271000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27775-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540226710","9783540277750"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27775-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}