{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:21:08Z","timestamp":1743038468881,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_13","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T09:47:55Z","timestamp":1312796875000},"page":"152-167","source":"Crossref","is-referenced-by-count":6,"title":["Termination of Isabelle Functions via Termination of Rewriting"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Krauss","sequence":"first","affiliation":[]},{"given":"Christian","family":"Sternagel","sequence":"additional","affiliation":[]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1999","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11737414_9","volume-title":"Functional and Logic Programming","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: A practical tool for the coq proof assistant. In: Hagiya, M. (ed.) FLOPS 2006. LNCS, vol.\u00a03945, pp. 114\u2013129. Springer, Heidelberg (2006)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comp. Science (2011) (to appear)","DOI":"10.1017\/S0960129511000120"},{"key":"13_CR4","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":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-540-74591-4_5","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Bulwahn","year":"2007","unstructured":"Bulwahn, L., Krauss, A., Nipkow, T.: Finding lexicographic orders for termination proofs in Isabelle\/HOL. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 38\u201353. Springer, Heidelberg (2007)"},{"key":"13_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-74621-8_10","volume-title":"Frontiers of Combining Systems","author":"E. Contejean","year":"2007","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of automated termination proofs. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 148\u2013162. Springer, Heidelberg (2007)"},{"issue":"2-3","key":"13_CR7","doi-asserted-by":"publisher","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. Reasoning\u00a040(2-3), 195\u2013220 (2008)","journal-title":"J. Autom. Reasoning"},{"issue":"1,2","key":"13_CR8","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s002000100063","volume":"12","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebr. Eng. Comm\u00a012(1,2), 39\u201372 (2001)","journal-title":"Appl. Algebr. Eng. Comm"},{"key":"13_CR9","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)"},{"key":"13_CR10","doi-asserted-by":"crossref","first-page":"169","DOI":"10.7551\/mitpress\/5641.003.0012","volume-title":"Proof, Language, and Interaction","author":"M. Gordon","year":"2000","unstructured":"Gordon, M.: From LCF to HOL: A short history. In: Proof, Language, and Interaction, pp. 169\u2013185. MIT Press, Cambridge (2000)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-02348-4_21","volume-title":"Rewriting Techniques and Applications","author":"M. Korp","year":"2009","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol.\u00a05595, pp. 295\u2013304. Springer, Heidelberg (2009)"},{"key":"13_CR12","series-title":"Lecture Notes in Artificial Intelligence","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)"},{"issue":"4","key":"13_CR13","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A. Krauss","year":"2010","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reasoning\u00a044(4), 303\u2013336 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"1-2","key":"13_CR16","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. Algebr. Eng. Comm.\u00a012(1-2), 73\u2013116 (2001)","journal-title":"Appl. Algebr. Eng. Comm."},{"key":"13_CR17","unstructured":"Sternagel, C.: Automatic Certification of Termination Proofs. PhD thesis, Institut f\u00fcr Informatik, Universit\u00e4t Innsbruck, Austria (2010)"},{"key":"13_CR18","unstructured":"Sternagel, C., Thiemann, R.: Certified subterm criterion and certified usable rules. In: Proc. RTA 2010, LIPIcs, vol.\u00a06, pp. 325\u2013340 (2010)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 452\u2013468. Springer, Heidelberg (2009)"},{"key":"13_CR20","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H. Zantema","year":"1995","unstructured":"Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae\u00a024, 89\u2013105 (1995)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,9]],"date-time":"2024-04-09T19:18:30Z","timestamp":1712690310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}