{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:01Z","timestamp":1762458541416},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540714095"},{"type":"electronic","value":"9783540714101"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-71410-1_13","type":"book-chapter","created":{"date-parts":[[2007,5,21]],"date-time":"2007-05-21T06:57:52Z","timestamp":1179730672000},"page":"177-193","source":"Crossref","is-referenced-by-count":10,"title":["Automated Termination Analysis for Logic Programs by Term Rewriting"],"prefix":"10.1007","author":[{"given":"Peter","family":"Schneider-Kamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Serebrenik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-57529-4_47","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"G. Aguzzi","year":"1993","unstructured":"G.\u00a0Aguzzi and U.\u00a0Modigliani. Proving termination of logic programs by transforming them into equivalent term rewriting systems. In Proc. 13th FST & TCS, LNCS 761, pages 114\u2013124, 1993."},{"key":"13_CR2","volume-title":"From Logic Programming to Prolog","author":"K.R. Apt","year":"1997","unstructured":"Apt, K.R.: From Logic Programming to Prolog. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Mathematical Foundations of Computer Science 1993","author":"K.R. Apt","year":"1993","unstructured":"Apt, K.R., Etalle, S.: On the unification free Prolog programs. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol.\u00a0711, pp. 1\u201319. Springer, Heidelberg (1993)"},{"key":"13_CR4","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":"13_CR5","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":"13_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"13_CR7","volume-title":"ACM Transactions on Programming Languages and Systems","author":"M. Bruynooghe","year":"2006","unstructured":"Bruynooghe, M., Codish, M., Gallagher, J., Genaim, S., Vanhoof, W.: Termination analysis of logic programs through combination of type-based norms. In: ACM Transactions on Programming Languages and Systems, ACM Press, New York (To appear, 2006)"},{"key":"13_CR8","unstructured":"Chtourou, M., Rusinowitch, M.: M\u00e9thode transformationelle pour la preuve de terminaison des programmes logiques. Unpublished manuscript (1993)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/11562931_25","volume-title":"Logic Programming","author":"M. Codish","year":"2005","unstructured":"Codish, M., Lagoon, V., Stuckey, P.: Testing for termination with monotonicity constraints. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 326\u2013340. Springer, Heidelberg (2005)"},{"issue":"1","key":"13_CR10","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 termination analysis of logic programs. Journal of Logic Programming\u00a041(1), 103\u2013123 (1999)","journal-title":"Journal of Logic Programming"},{"key":"13_CR11","volume-title":"Logic Programming","author":"A. Colmerauer","year":"1982","unstructured":"Colmerauer, A.: Prolog and infinite trees. In: Clark, K.L., T\u00e4rnlund, S. (eds.) Logic Programming, Academic Press, London (1982)"},{"key":"13_CR12","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0743-1066(94)90027-2","volume":"19\/20","author":"D. Schreye De","year":"1994","unstructured":"De Schreye, D., Decorte, S.: Termination of logic programs: The never-ending story. Journal of Logic Programming\u00a019\/20, 199\u2013260 (1994)","journal-title":"Journal of Logic Programming"},{"key":"13_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-45628-7_9","volume-title":"Computational Logic: Logic Programming and Beyond","author":"D. Schreye De","year":"2002","unstructured":"De Schreye, D., Serebrenik, A.: Acceptability with general orderings. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol.\u00a02407, pp. 187\u2013210. Springer, Heidelberg (2002)"},{"key":"13_CR14","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. Symb. Comp.\u00a03, 69\u2013116 (1987)","journal-title":"J. Symb. Comp."},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","first-page":"216","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1993","unstructured":"Ganzinger, H., Waldmann, U.: Termination proofs of well-moded logic programs via conditional rewrite systems. In: Rusinowitch, M., Remy, J.-L. (eds.) Conditional Term Rewriting Systems. LNCS, vol.\u00a0656, pp. 216\u2013222. Springer, Heidelberg (1993)"},{"key":"13_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"key":"13_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the DP framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"13_CR18","unstructured":"Huet, G.: R\u00e9solution d\u2019\u00e9quations dans les langages d\u2019ordre 1, 2, ...\u03c9. PhD (1976)"},{"issue":"1","key":"13_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0743-1066(97)00028-9","volume":"34","author":"M. Krishna Rao","year":"1998","unstructured":"Krishna Rao, M., Kapur, D., Shyamasundar, R.: Transformational methodology for proving termination of logic programs. J. Log. Prog.\u00a034(1), 1\u201342 (1998)","journal-title":"J. Log. Prog."},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/978-3-540-24599-5_18","volume-title":"Logic Programming","author":"V. Lagoon","year":"2003","unstructured":"Lagoon, V., Mesnard, F., Stuckey, P.J.: Termination analysis with types is more accurate. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol.\u00a02916, pp. 254\u2013268. Springer, Heidelberg (2003)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/3-540-62718-9_6","volume-title":"Logic Program Synthesis and Transformation","author":"M. Leuschel","year":"1997","unstructured":"Leuschel, M., S\u00f8rensen, M.H.: Redundant argument filtering of logic programs. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol.\u00a01207, pp. 83\u2013103. Springer, Heidelberg (1997)"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1007\/3-540-63166-6_44","volume-title":"Computer Aided Verification","author":"N. Lindenstrauss","year":"1997","unstructured":"Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: TermiLog: A system for checking ter- mination of queries to logic programs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 444\u2013447. Springer, Heidelberg (1997)"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-58431-5_16","volume-title":"Algebraic and Logic Programming","author":"M. Marchiori","year":"1994","unstructured":"Marchiori, M.: Logic programs as term rewriting systems. In: Rodr\u00edguez-Artalejo, M., Levi, G. (eds.) ALP 1994. LNCS, vol.\u00a0850, pp. 223\u2013241. Springer, Heidelberg (1994)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/BFb0014328","volume-title":"Algebraic Methodology and Software Technology","author":"M. Marchiori","year":"1996","unstructured":"Marchiori, M.: Proving existential termination of normal logic programs. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol.\u00a01101, pp. 375\u2013390. Springer, Heidelberg (1996)"},{"issue":"1-2","key":"13_CR25","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1017\/S1471068404002017","volume":"5","author":"F. Mesnard","year":"2005","unstructured":"Mesnard, F., Bagnara, R.: cTI: A constraint-based termination inference tool for ISO-Prolog. Theory and Practice of Logic Programming\u00a05(1-2), 243\u2013257 (2005)","journal-title":"Theory and Practice of Logic Programming"},{"issue":"2","key":"13_CR26","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/635499.635503","volume":"4","author":"F. Mesnard","year":"2003","unstructured":"Mesnard, F., Ruggieri, S.: On proving left termination of constraint logic programs. ACM Transaction on Computational Logic\u00a04(2), 207\u2013259 (2003)","journal-title":"ACM Transaction on Computational Logic"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/11562931_24","volume-title":"Logic Programming","author":"M.T. Nguyen","year":"2005","unstructured":"Nguyen, M.T., De Schreye, D.: Polynomial interpretations as a basis for termination analysis of logic programs. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 311\u2013325. Springer, Heidelberg (2005)"},{"key":"13_CR28","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s002000100064","volume":"12","author":"E. Ohlebusch","year":"2001","unstructured":"Ohlebusch, E.: Termination of logic programs: Transformational methods revisited. Appl. Algebra in Engineering, Communication and Computing\u00a012, 73\u2013116 (2001)","journal-title":"Appl. Algebra in Engineering, Communication and Computing"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10721975_20","volume-title":"Rewriting Techniques and Applications","author":"E. Ohlebusch","year":"2000","unstructured":"Ohlebusch, E., Claves, C., March\u00e9, C.: TALP: A tool for the termination analysis of logic programs. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 270\u2013273. Springer, Heidelberg (2000)"},{"key":"13_CR30","first-page":"168","volume-title":"Proc. 14th ICLP","author":"F. Raamsdonk van","year":"1997","unstructured":"van Raamsdonk, F.: Translating logic programs into conditional rewriting systems. In: Proc. 14th ICLP, pp. 168\u2013182. MIT Press, Cambridge (1997)"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-540-25938-1_10","volume-title":"Logic Based Program Synthesis and Transformation","author":"A. Serebrenik","year":"2004","unstructured":"Serebrenik, A., De Schreye, D.: Proving termination with adornments. In: Bruynooghe, M. (ed.) Logic Based Program Synthesis and Transformation. LNCS, vol.\u00a03018, pp. 108\u2013109. Springer, Heidelberg (2004)"},{"key":"13_CR32","doi-asserted-by":"publisher","first-page":"719","DOI":"10.1017\/S1471068404002042","volume":"4","author":"A. Serebrenik","year":"2004","unstructured":"Serebrenik, A., De Schreye, D.: Inference of termination conditions for numerical loops in Prolog. Theory and Practice of Logic Programming\u00a04, 719\u2013751 (2004)","journal-title":"Theory and Practice of Logic Programming"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-3-540-27775-0_4","volume-title":"Logic Programming","author":"J.-G. Smaus","year":"2004","unstructured":"Smaus, J.-G.: Termination of logic programs using various dynamic selection rules. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol.\u00a03132, pp. 43\u201357. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71410-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:31:21Z","timestamp":1558258281000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71410-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540714095","9783540714101"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71410-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}