{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T18:09:22Z","timestamp":1768586962115,"version":"3.49.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,1,15]],"date-time":"2011-01-15T00:00:00Z","timestamp":1295049600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2011,8]]},"DOI":"10.1007\/s10817-010-9215-9","type":"journal-article","created":{"date-parts":[[2011,1,14]],"date-time":"2011-01-14T16:11:43Z","timestamp":1295021503000},"page":"133-160","source":"Crossref","is-referenced-by-count":11,"title":["Proving Termination by Dependency Pairs and Inductive Theorem Proving"],"prefix":"10.1007","volume":"47","author":[{"given":"Carsten","family":"Fuhs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Parting","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Swiderski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,1,15]]},"reference":[{"key":"9215_CR1","unstructured":"AProVE web site: http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Induction\/ (2010). Accessed December 2010"},{"key":"9215_CR2","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 236, 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"9215_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"issue":"2","key":"9215_CR4","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., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program. 9(2), 137\u2013159 (1987)","journal-title":"Sci. Comput. Program."},{"key":"9215_CR5","doi-asserted-by":"crossref","unstructured":"Bouhoula, A., Rusinowitch, M.: SPIKE: a system for automatic inductive proofs. In: Proc.\u00a0AMAST\u201995. LNCS, vol. 936, pp. 576\u2013577 (1995)","DOI":"10.1007\/3-540-60043-4_79"},{"key":"9215_CR6","volume-title":"A Computational Logic","author":"RS Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, JS.: A Computational Logic. Academic Press, New York (1979)"},{"key":"9215_CR7","doi-asserted-by":"crossref","unstructured":"Brauburger, J., Giesl, J.: Termination analysis by inductive evaluation. In: Proc. CADE\u201998. LNAI, vol. 1421, pp. 254\u2013269 (1998)","DOI":"10.1007\/BFb0054264"},{"key":"9215_CR8","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, pp. 845\u2013911. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"9215_CR9","doi-asserted-by":"crossref","unstructured":"Comon, H.: Inductionless induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, pp. 913\u2013962. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"key":"9215_CR10","first-page":"63","volume-title":"Proc. PEPM\u201910","author":"E Contejean","year":"2010","unstructured":"Contejean, E., Paskevich, A., Urbain, X., Courtieu, P., Pons, O., Forest, J.: A3PAT, an approach for certified automated termination proofs. In: Proc. PEPM\u201910, pp. 63\u201372. ACM Press, New York (2010)"},{"issue":"2,3","key":"9215_CR11","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2,3), 195\u2013220 (2008)","journal-title":"J. Autom. Reason."},{"key":"9215_CR12","doi-asserted-by":"crossref","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Proc.\u00a0SAT\u201907. LNCS, vol. 4501, pp. 340\u2013354 (2007)","DOI":"10.1007\/978-3-540-72788-0_33"},{"key":"9215_CR13","doi-asserted-by":"crossref","unstructured":"Giesl, J.: Termination analysis for functional programs using term orderings. In: Proc.\u00a0SAS\u201995. LNCS, vol. 983, pp. 154\u2013171 (1995)","DOI":"10.1007\/3-540-60360-3_38"},{"key":"9215_CR14","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proc.\u00a0LPAR\u201904. LNAI, vol. 3452, pp. 301\u2013331 (2005)","DOI":"10.1007\/978-3-540-32275-7_21"},{"key":"9215_CR15","doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Proc.\u00a0IJCAR\u201906. LNAI, vol. 4130, pp. 281\u2013286 (2006)","DOI":"10.1007\/11814771_24"},{"issue":"3","key":"9215_CR16","doi-asserted-by":"crossref","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. J. Autom. Reason. 37(3), 155\u2013203 (2006)","journal-title":"J. Autom. Reason."},{"key":"9215_CR17","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. In: Proc.\u00a0CADE\u201907. LNAI, vol. 4603, pp. 443\u2013459 (2007)","DOI":"10.1007\/978-3-540-73595-3_33"},{"key":"9215_CR18","doi-asserted-by":"crossref","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2) (2011, to appear). Preliminary version appeared in Proc.\u00a0RTA\u201906. LNCS, vol. 4098, pp. 297\u2013312 (2006)","DOI":"10.1145\/1890028.1890030"},{"issue":"2","key":"9215_CR19","first-page":"10:1","volume":"10","author":"I Gnaedig","year":"2008","unstructured":"Gnaedig, I., Kirchner, H.: Termination of rewriting under strategies. ACM Trans. Comput. Log. 10(2), 10:1\u201310:52 (2008)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1,2","key":"9215_CR20","doi-asserted-by":"crossref","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. Inf. Comput. 199(1,2), 172\u2013199 (2005)","journal-title":"Inf. Comput."},{"issue":"4","key":"9215_CR21","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1016\/j.ic.2006.08.010","volume":"205","author":"N Hirokawa","year":"2007","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool: techniques and features. Inf. Comput. 205(4), 474\u2013511 (2007)","journal-title":"Inf. Comput."},{"issue":"2","key":"9215_CR22","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D Kapur","year":"1987","unstructured":"Kapur, D., Musser, D.R.: Proof by consistency. Artif. Intell. 31(2), 125\u2013157 (1987)","journal-title":"Artif. Intell."},{"key":"9215_CR23","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P., Zhang, H.: On sufficient completeness and related properties of term rewriting systems. Acta Inf. 24, 395\u2013415 (1987)","journal-title":"Acta Inf."},{"key":"9215_CR24","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, JS.: Computer-Aided Reasoning: An Approach. Kluwer, Norwell (2000)"},{"key":"9215_CR25","unstructured":"Korp, M., Middeldorp, A.: Beyond dependency graphs. In: Proc.\u00a0CADE\u201909. LNAI, vol. 5663, pp. 339\u2013354 (2009)"},{"key":"9215_CR26","unstructured":"Krauss, A.: Certified size-change termination. In: Proc.\u00a0CADE\u201907. LNAI, vol. 4603, pp. 460\u2013475 (2007)"},{"key":"9215_CR27","unstructured":"Lankford, D.: On Proving Term Rewriting Systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)"},{"key":"9215_CR28","first-page":"108","volume-title":"Proc.\u00a0PPDP\u201908","author":"S Lucas","year":"2008","unstructured":"Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Proc.\u00a0PPDP\u201908, pp. 108\u2013119. ACM Press, New York (2008)"},{"key":"9215_CR29","doi-asserted-by":"crossref","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Proc.\u00a0CAV\u201906. LNCS, vol. 4144, pp. 401\u2013414 (2006)","DOI":"10.1007\/11817963_36"},{"issue":"1,2","key":"9215_CR30","doi-asserted-by":"crossref","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 Eng. Commun. Comput. 12(1,2), 73\u2013116 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9215_CR31","doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proc. RTA\u201910. LIPIcs, vol. 6, pp. 259\u2013276 (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"9215_CR32","doi-asserted-by":"crossref","unstructured":"Panitz, S.E., Schmidt-Schau\u00df, M.: TEA: automatically proving termination of programs in a non-strict higher-order functional language. In: Proc.\u00a0SAS\u201997. LNCS, vol. 1302, pp. 345\u2013360 (1997)","DOI":"10.1007\/BFb0032752"},{"key":"9215_CR33","first-page":"273","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a01","author":"DA Plaisted","year":"1993","unstructured":"Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a01, pp. 273\u2013364. Oxford University Press, London (1993)"},{"key":"9215_CR34","unstructured":"van de Pol, J.: Modularity in Many-Sorted Term Rewriting. Master\u2019s thesis, Utrecht University (1992). Available from http:\/\/homepages.cwi.nl\/~vdpol\/papers\/"},{"key":"9215_CR35","doi-asserted-by":"crossref","unstructured":"Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and SAT solving. In: Proc.\u00a0FroCoS\u201907. LNAI, vol. 4720, pp. 267\u2013282 (2007)","DOI":"10.1007\/978-3-540-74621-8_18"},{"issue":"1","key":"9215_CR36","doi-asserted-by":"crossref","first-page":"2:1","DOI":"10.1145\/1614431.1614433","volume":"11","author":"P Schneider-Kamp","year":"2009","unstructured":"Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination proofs for logic programs by term rewriting. ACM Trans. Comput. Log. 11(1), 2:1\u20132:52 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"9215_CR37","doi-asserted-by":"crossref","unstructured":"Swiderski, S., Parting, M., Giesl, J., Fuhs, C., Schneider-Kamp, P.: Termination analysis by dependency pairs and inductive theorem proving. In: Proc.\u00a0CADE\u201909. LNAI, vol. 5663, pp. 322\u2013338 (2009)","DOI":"10.1007\/978-3-642-02959-2_25"},{"key":"9215_CR38","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Proc. TPHOLs\u201909. LNCS, vol. 5674, pp. 452\u2013468 (2009)","DOI":"10.1007\/978-3-642-03359-9_31"},{"issue":"3","key":"9215_CR39","doi-asserted-by":"crossref","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. Inf. Process. Lett. 25(3), 141\u2013143 (1987)","journal-title":"Inf. Process. Lett."},{"key":"9215_CR40","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1093\/oso\/9780198537465.003.0003","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a02","author":"C Walther","year":"1994","unstructured":"Walther, C.: Mathematical induction. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a02, pp. 127\u2013228. Oxford University Press, London (1994)"},{"issue":"1","key":"9215_CR41","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C Walther","year":"1994","unstructured":"Walther, C.: On proving the termination of algorithms by machine. Artif. Intell. 71(1), 101\u2013157 (1994)","journal-title":"Artif. Intell."},{"key":"9215_CR42","unstructured":"Walther, C., Schweitzer, S.: About VeriFun. In: Proc.\u00a0CADE\u201903. LNAI, vol. 2741, pp. 322\u2013327 (2003)"},{"issue":"2","key":"9215_CR43","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-009-9131-z","volume":"43","author":"H Zankl","year":"2009","unstructured":"Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. J. Autom. Reason. 43(2), 173\u2013201 (2009)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9215_CR44","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H Zantema","year":"1994","unstructured":"Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17(1), 23\u201350 (1994)","journal-title":"J. Symb. Comput."},{"key":"9215_CR45","doi-asserted-by":"crossref","unstructured":"Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifications. In: Proc.\u00a0CADE\u201988. LNAI, vol. 310, pp. 162\u2013181 (1988)","DOI":"10.1007\/BFb0012831"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9215-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9215-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9215-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T04:01:58Z","timestamp":1712116918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9215-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,15]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["9215"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9215-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1,15]]}}}