{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:32:49Z","timestamp":1725535969372},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642029585"},{"type":"electronic","value":"9783642029592"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_25","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T05:02:22Z","timestamp":1248498142000},"page":"322-338","source":"Crossref","is-referenced-by-count":2,"title":["Termination Analysis by Dependency Pairs and Inductive Theorem Proving"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Swiderski","sequence":"first","affiliation":[]},{"given":"Michael","family":"Parting","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"AProVE website, http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Induction\/"},{"key":"25_CR2","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":"25_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/3-540-60043-4_79","volume-title":"Algebraic Methodology and Software Technology","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A., Rusinowitch, M.: SPIKE: A system for automatic inductive proofs. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol.\u00a0936, pp. 576\u2013577. Springer, Heidelberg (1995)"},{"key":"25_CR5","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)"},{"key":"25_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/BFb0054264","volume-title":"Automated Deduction - CADE-15","author":"J. Brauburger","year":"1998","unstructured":"Brauburger, J., Giesl, J.: Termination analysis by inductive evaluation. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 254\u2013269. Springer, Heidelberg (1998)"},{"key":"25_CR7","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 & MIT (2001)","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"25_CR8","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 & MIT (2001)","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"key":"25_CR9","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)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-60360-3_38","volume-title":"Static Analysis","author":"J. Giesl","year":"1995","unstructured":"Giesl, J.: Termination analysis for functional programs using term orderings. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983, pp. 154\u2013171. Springer, Heidelberg (1995)"},{"key":"25_CR11","series-title":"LNAI","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 DP 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":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/11805618_23","volume-title":"Term Rewriting and Applications","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Swiderski, S., Schneider-Kamp, P., Thiemann, R.: Automated termination analysis for Haskell: From term rewriting to programming languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 297\u2013312. Springer, Heidelberg (2006)"},{"key":"25_CR13","series-title":"LNAI","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)"},{"issue":"3","key":"25_CR14","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"},{"key":"25_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-73595-3_33","volume-title":"Automated Deduction \u2013 CADE-21","author":"J. Giesl","year":"2007","unstructured":"Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 443\u2013459. Springer, Heidelberg (2007)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Gnaedig, I., Kirchner, H.: Termination of rewriting under strategies. ACM Transactions on Computational Logic\u00a010(3) (2008)","DOI":"10.1145\/1462179.1462182"},{"issue":"1-2","key":"25_CR17","first-page":"2","volume":"24","author":"B. Gramlich","year":"1995","unstructured":"Gramlich, B.: Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae\u00a024(1-2), 2\u201323 (1995)","journal-title":"Fundamenta Informaticae"},{"issue":"1-2","key":"25_CR18","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":"4","key":"25_CR19","doi-asserted-by":"publisher","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. Information and Computation\u00a0205(4), 474\u2013511 (2007)","journal-title":"Information and Computation"},{"issue":"2","key":"25_CR20","doi-asserted-by":"publisher","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. Int.\u00a031(2), 125\u2013157 (1987)","journal-title":"Artif. Int."},{"key":"25_CR21","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)"},{"key":"25_CR22","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-540-73595-3_34","volume-title":"Automated Deduction \u2013 CADE-21","author":"A. Krauss","year":"2007","unstructured":"Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 460\u2013475. Springer, Heidelberg (2007)"},{"key":"25_CR23","unstructured":"Lankford, D.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA (1979)"},{"key":"25_CR24","first-page":"108","volume-title":"Proc. PPDP 2008","author":"S. Lucas","year":"2008","unstructured":"Lucas, S., Meseguer, J.: Order-sorted dependency pairs. In: Proc. PPDP 2008, pp. 108\u2013119. ACM Press, New York (2008)"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11817963_36","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 401\u2013414. Springer, Heidelberg (2006)"},{"key":"25_CR26","unstructured":"Middeldorp, A., Zantema, H.: Personal communication (2008)"},{"key":"25_CR27","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 approaches revisited. Appl. Algebra in Engineering, Comm. and Computing\u00a012, 73\u2013116 (2001)","journal-title":"Appl. Algebra in Engineering, Comm. and Computing"},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/BFb0032752","volume-title":"Static Analysis","author":"S.E. Panitz","year":"1997","unstructured":"Panitz, S.E., Schmidt-Schau\u00df, M.: TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.\u00a01302, pp. 345\u2013360. Springer, Heidelberg (1997)"},{"key":"25_CR29","doi-asserted-by":"crossref","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, Oxford, vol.\u00a01, pp. 273\u2013364 (1993)","DOI":"10.1093\/oso\/9780198537458.003.0005"},{"key":"25_CR30","unstructured":"van de Pol, J.: Modularity in many-sorted term rewriting. Master\u2019s Thesis, Utrecht University (1992), http:\/\/homepages.cwi.nl\/~vdpol\/papers\/"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic (to appear, 2009)","DOI":"10.1145\/1614431.1614433"},{"issue":"1","key":"25_CR32","doi-asserted-by":"publisher","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. Artificial Intelligence\u00a071(1), 101\u2013157 (1994)","journal-title":"Artificial Intelligence"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Walther, C.: Mathematical induction. In: Gabbay, D., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in AI and Logic Programming, Oxford, vol.\u00a02, pp. 127\u2013228 (1994)","DOI":"10.1093\/oso\/9780198537465.003.0003"},{"key":"25_CR34","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45085-6_28","volume-title":"Automated Deduction \u2013 CADE-19","author":"C. Walther","year":"2003","unstructured":"Walther, C., Schweitzer, S.: About VeriFun. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 322\u2013327. Springer, Heidelberg (2003)"},{"issue":"1","key":"25_CR35","doi-asserted-by":"publisher","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. Journal of Symbolic Computation\u00a017(1), 23\u201350 (1994)","journal-title":"Journal of Symbolic Computation"},{"key":"25_CR36","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/BFb0012831","volume-title":"9th International Conference on Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifications. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS (LNAI), vol.\u00a0310, pp. 162\u2013181. Springer, Heidelberg (1988)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T13:08:31Z","timestamp":1710508111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}