{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T00:47:11Z","timestamp":1768438031647,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540787686","type":"print"},{"value":"9783540787693","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-78769-3_2","type":"book-chapter","created":{"date-parts":[[2008,11,26]],"date-time":"2008-11-26T12:05:56Z","timestamp":1227701156000},"page":"8-22","source":"Crossref","is-referenced-by-count":19,"title":["Termination Analysis of Logic Programs Based on Dependency Graphs"],"prefix":"10.1007","author":[{"given":"Manh Thang","family":"Nguyen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Danny","family":"De Schreye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1-2","key":"2_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(1-2), 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"2_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(91)90004-L","volume":"86","author":"R.N. Bol","year":"1991","unstructured":"Bol, R.N., Apt, K.R., Klop, J.W.: An analysis of loop checking mechanisms for logic programs. Theoretical Computer Science\u00a086(1), 35\u201379 (1991)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(92)00019-N","volume":"124","author":"A. Bossi","year":"1994","unstructured":"Bossi, A., Cocco, N., Fabris, M.: Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science\u00a0124(2), 297\u2013328 (1994)","journal-title":"Theoretical Computer Science"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Bruynooghe, M., Codish, M., Gallagher, J.P., Genaim, S., Vanhoof, W.: Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems\u00a029(2) (2007)","DOI":"10.1145\/1216374.1216378"},{"issue":"1","key":"2_CR5","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. Journal of Logic Programming\u00a041(1), 103\u2013123 (1999)","journal-title":"Journal of Logic Programming"},{"key":"2_CR6","unstructured":"Codish, M., Genaim, S.: Proving termination one loop at a time. In: Proc. WLPE 2003 (2003)"},{"issue":"4","key":"2_CR7","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10817-005-9022-x","volume":"34","author":"E. Contejean","year":"2005","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning\u00a034(4), 325\u2013363 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"De Schreye, D., Verschaetse, K., Bruynooghe, M.: A framework for analyzing the termination of definite logic programs with respect to call patterns. In: Proc. FGCS 1992, pp. 481\u2013488 (1992)","DOI":"10.1007\/3-540-56282-6_5"},{"key":"2_CR9","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)"},{"issue":"6","key":"2_CR10","doi-asserted-by":"publisher","first-page":"1137","DOI":"10.1145\/330643.330645","volume":"21","author":"S. Decorte","year":"1999","unstructured":"Decorte, S., De Schreye, D., Vandecasteele, H.: Constraint-based automatic termination analysis of logic programs. ACM Transactions on Programming Languages and Systems\u00a021(6), 1137\u20131195 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1-2","key":"2_CR11","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. Journal of Symbolic Computation\u00a03(1-2), 69\u2013116 (1987)","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. In: Applicable Algebra in Engineering, Communication and Computing, 12(1,2), pp. 117\u2013156 (2001)","DOI":"10.1007\/s002000100065"},{"key":"2_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/11814771_47","volume-title":"Automated Reasoning","author":"J. Waldmann","year":"2006","unstructured":"Waldmann, J., Zantema, H., Endrullis, J.: Matrix Interpretations for Proving Termination of Term Rewriting. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 574\u2013588. Springer, Heidelberg (2006)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT Solving for Termination Analysis with Polynomial Interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"34","author":"J. Giesl","year":"2002","unstructured":"Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation\u00a034(1), 21\u201358 (2002)","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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":"2_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 dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"3","key":"2_CR18","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning\u00a037(3), 155\u2013203 (2006)","journal-title":"Journal of Automated Reasoning"},{"issue":"1-2","key":"2_CR19","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/j.ic.2004.10.004","volume":"199","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation\u00a0199(1-2), 172\u2013199 (2005)","journal-title":"Information and Computation"},{"issue":"1","key":"2_CR20","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1005983105493","volume":"21","author":"H. Hong","year":"1998","unstructured":"Hong, H., Jaku\u0161, D.: Testing positiveness of polynomials. Journal of Automated Reasoning\u00a021(1), 23\u201338 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/10704567_3","volume-title":"Principles and Practice of Declarative Programming","author":"K. Kusakari","year":"1999","unstructured":"Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol.\u00a01702, pp. 48\u201362. Springer, Heidelberg (1999)"},{"key":"2_CR22","unstructured":"Lankford, D.S.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. POPL 2001, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-540-73449-9_23","volume-title":"Term Rewriting and Applications","author":"C. March\u00e9","year":"2007","unstructured":"March\u00e9, C., Zantema, H.: The Termination Competition. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 303\u2013313. Springer, Heidelberg (2007)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Mesnard, F., Bagnara, R.: cTI: A constraint-based termination inference tool for ISO-Prolog. In: Theory and Practice of Logic Programming, vol.\u00a05(1, 2), pp. 243\u2013257 (2005)","DOI":"10.1017\/S1471068404002017"},{"key":"2_CR26","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":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-71410-1_15","volume-title":"Logic-Based Program Synthesis and Transformation","author":"D. Schreye De","year":"2007","unstructured":"De Schreye, D., Nguyen, M.T.: Polytool: Proving Termination Automatically Based on Polynomial Interpretations. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol.\u00a04407, pp. 210\u2013218. Springer, Heidelberg (2007)"},{"key":"2_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52837-7","volume-title":"Termination Proofs for Logic Programs","author":"L. Pl\u00fcmer","year":"1990","unstructured":"Pl\u00fcmer, L.: Termination Proofs for Logic Programs. Springer, Heidelberg (1990)"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proc. LICS 2004, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"2_CR30","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"30","author":"F.P. Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Society\u00a030, 264\u2013286 (1930)","journal-title":"Proc. London Math. Society"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-71410-1_13","volume-title":"Logic-Based Program Synthesis and Transformation","author":"P. Schneider-Kamp","year":"2007","unstructured":"Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated Termination Analysis for Logic Programs by Term Rewriting. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol.\u00a04407, pp. 177\u2013193. Springer, Heidelberg (2007)"},{"key":"2_CR32","unstructured":"The termination problem data base, http:\/\/www.lri.fr\/~marche\/tpdb ."},{"issue":"4","key":"2_CR33","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s00200-005-0179-7","volume":"16","author":"R. Thiemann","year":"2005","unstructured":"Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing\u00a016(4), 229\u2013270 (2005)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78769-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,21]],"date-time":"2023-05-21T13:54:31Z","timestamp":1684677271000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78769-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540787686","9783540787693"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78769-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}