{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:10:23Z","timestamp":1725466223200},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054264","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T03:28:51Z","timestamp":1149650931000},"page":"254-269","source":"Crossref","is-referenced-by-count":5,"title":["Termination analysis by inductive evaluation"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Brauburger","sequence":"first","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"T. Arts and J. Giesl. Proving innermost normalisation automatically. In Proc. RTA-97, Sitges, Spain, LNCS 1232, 1997.","DOI":"10.1007\/3-540-62950-5_68"},{"key":"25_CR2","unstructured":"R. S. Boyer and J S. Moore. A computational logic. Academic Press, 1979."},{"key":"25_CR3","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF00881856","volume":"14","author":"A. Bouhoula","year":"1995","unstructured":"A. Bouhoula and M. Rusinowitch. Implicit induction in conditional theories. Journal of Automated Reasoning, 14:189\u2013235, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR4","series-title":"Report IBN-96-33","volume-title":"LNCS 1145","author":"J. Brauburger","year":"1996","unstructured":"J. Brauburger and J. Giesl. Termination analysis for partial functions. In Proc. 3rd Int. Static Analysis Symp., Aachen, Germany, LNCS 1145, 1996. Extended version appeared as Report IBN-96-33, TU Darmstadt, 1996."},{"key":"25_CR5","volume-title":"Technical Report IBN-98-47","author":"J. Brauburger","year":"1998","unstructured":"J. Brauburger and J. Giesl. Termination analysis with inductive evaluation. Technical Report IBN-98-47, TU Darmstadt, Germany, 1998."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"J. Brauburger. Automatic termination analysis for partial functions using polynomial orderings. In Proc. 4th SAS, Paris, France, LNCS 1302, 1997.","DOI":"10.1007\/BFb0032751"},{"key":"25_CR7","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, and A. Stevens. A rational reconstruction and extension of recursion analysis. In Proc. IJCAI '89, Detroit, USA, 1989."},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. J. Symb. Comp., 3:69\u2013115, 1987.","journal-title":"J. Symb. Comp."},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"J. Giesl. Generating polynomial orderings for termination proofs. In Proc. RTA-95, Kaiserslautern, Germany, LNCS 914, 1995.","DOI":"10.1007\/3-540-59200-8_77"},{"key":"25_CR10","volume-title":"PhD thesis","author":"J. Giesl","year":"1995","unstructured":"J. Giesl. Automatisierung von Terminierungsbeweisen f\u00fcr rekursiv definierte Algorithmen. PhD thesis, Infix-Verlag, St. Augustin, Germany, 1995."},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"J. Giesl. Termination analysis for functional programs using term orderings. In Proc. 2nd Int. Static Analysis Symp., Glasgow, UK, LNCS 983, 1995.","DOI":"10.1007\/3-540-60360-3_38"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1005797629953","volume":"19","author":"J. Giesl","year":"1997","unstructured":"J. Giesl. Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning, 19:1\u201329, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"J. Giesl, C. Walther, and J. Brauburger. Termination analysis for functional programs. In W. Bibel and P. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications, vol. 3. Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-0437-3_6"},{"key":"25_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The science of programming","author":"D. Gries","year":"1981","unstructured":"D. Gries. The science of programming. Springer-Verlag, New York, 1981."},{"key":"25_CR15","volume-title":"Functional programming","author":"P. Henderson","year":"1980","unstructured":"P. Henderson. Functional programming. Prentice-Hall, London, 1980."},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"D. Hutter and C. Sengler. INKA: The next generation. In Proc. CADE-13, New Brunswick, USA, LNAI 1104, 1996.","DOI":"10.1007\/3-540-61511-3_92"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D. Kapur","year":"1995","unstructured":"D. Kapur and H. Zhang. An overview of Rewrite Rule Laboratory (RRL). J. Computer Math. Appl., 29:91\u2013114, 1995.","journal-title":"J. Computer Math. Appl."},{"key":"25_CR18","volume-title":"Memo MTP-3","author":"D.S. Lankford","year":"1979","unstructured":"D.S. Lankford. On proving term rewriting systems are noetherian. Memo MTP-3, Math. Dept., Louisiana Tech. Univ., Ruston, USA, 1979."},{"issue":"2","key":"25_CR19","first-page":"144","volume":"3","author":"F. Nielson","year":"1996","unstructured":"F. Nielson and H. R. Nielson. Operational semantics of termination types. Nordic Journal of Computing, 3(2):144\u2013187, 1996.","journal-title":"Nordic Journal of Computing"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"S. E. Panitz and M. Schmidt-Schau\\. TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In Proc. 4th Int. Static Analysis Symp., Paris, France, LNCS 1302, 1997.","DOI":"10.1007\/BFb0032752"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"L. Pl\u00fcmer. Termination proofs for logic programs. LNAI 446, 1990.","DOI":"10.1007\/3-540-52837-7"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"M. Protzen. Patching faulty conjectures. In Proc. CADE-13, LNAI 1104, New Brunswick, USA, 1996.","DOI":"10.1007\/3-540-61511-3_70"},{"key":"25_CR23","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":"D. De Schreye and S. Decorte. Termination of logic programs: The never-ending story. Journal of Logic Programming, 19\/20:199\u2013260, 1994.","journal-title":"Journal of Logic Programming"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"C. Sengler. Termination of algorithms over non-freely generated data types. In Proc. CADE-13, New Brunswick, USA, LNAI 1104, 1996.","DOI":"10.1007\/3-540-61511-3_73"},{"key":"25_CR25","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0020-0190(94)90032-9","volume":"49","author":"J. Steinbach","year":"1994","unstructured":"J. Steinbach. Generating polynomial orderings. IPL, 49:85\u201393, 1994.","journal-title":"IPL"},{"key":"25_CR26","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/FI-1995-24123","volume":"24","author":"J. Steinbach","year":"1995","unstructured":"J. Steinbach. Simplification orderings: History of results. Fundamenta Informaticae, 24:47\u201387, 1995.","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"25_CR27","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/42282.42285","volume":"35","author":"J. D. Ullman","year":"1988","unstructured":"J. D. Ullman and A. van Gelder. Efficient tests for top-down termination of logical rules. Journal of the ACM, 35(2):345\u2013373, 1988.","journal-title":"Journal of the ACM"},{"key":"25_CR28","unstructured":"C. Walther. Mathematical induction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2. Oxford University Press, 1994."},{"issue":"1","key":"25_CR29","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"C. Walther. On proving the termination of algorithms by machine. Artificial Intelligence, 71(1):101\u2013157, 1994.","journal-title":"Artificial Intelligence"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"H. Zhang, D. Kapur, and M. S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In Proc. CADE-9, Argonne, USA, LNCS 310, 1988.","DOI":"10.1007\/BFb0012831"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054264","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T05:22:32Z","timestamp":1586928152000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054264"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/bfb0054264","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}