{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:20Z","timestamp":1725490100170},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_5","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"38-53","source":"Crossref","is-referenced-by-count":16,"title":["Finding Lexicographic Orders for Termination Proofs in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Lukas","family":"Bulwahn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Krauss","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Archive of Formal Proofs, http:\/\/afp.sourceforge.net\/","key":"5_CR1"},{"unstructured":"Abel, A.: foetus \u2013 termination checker for simple functional programs. Programming Lab. Report (1998)","key":"5_CR2"},{"issue":"1","key":"5_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796801004191","volume":"12","author":"A. Abel","year":"2002","unstructured":"Abel, A., Altenkirch, T.: A predicative analysis of structural recursion. J. Functional Programming\u00a012(1), 1\u201341 (2002)","journal-title":"J. Functional Programming"},{"issue":"1-2","key":"5_CR4","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. Theor. Comput. Sci.\u00a0236(1-2), 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Wadler, P. (eds.) FLOPS 2006. LNCS, vol.\u00a03945, Springer, Heidelberg (2006)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48256-3_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"1999","unstructured":"Berghofer, S., Wenzel, M.: Inductive datatypes in HOL - lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 19\u201336. Springer, Heidelberg (1999)"},{"volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","year":"1993","unstructured":"Gordon, M., Melham, T. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)","key":"5_CR7"},{"unstructured":"Harrison, J.: The HOL Light theorem prover, http:\/\/www.cl.cam.ac.uk\/users\/jrh\/hol-light","key":"5_CR8"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BFb0055137","volume-title":"Theorem Proving in Higher Order Logics","author":"P.V. Homeier","year":"1998","unstructured":"Homeier, P.V., Martin, D.F.: Mechanical verification of total correctness through diversion verification conditions. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol.\u00a01479, pp. 189\u2013206. Springer, Heidelberg (1998)"},{"key":"5_CR10","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, June 2000. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"5_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11814771_48","volume-title":"Automated Reasoning","author":"A. Krauss","year":"2006","unstructured":"Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 589\u2013603. Springer, Heidelberg (2006)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/978-3-540-73595-3_34","volume-title":"CADE-21","author":"A. Krauss","year":"2007","unstructured":"Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) CADE-21. LNCS, vol.\u00a04603, pp. 460\u2013476. Springer, Heidelberg (to appear, 2007)"},{"key":"5_CR13","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/360204.360210","volume-title":"ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"C.S. Lee","year":"2001","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 81\u201392. ACM Press, New York (2001)"},{"key":"5_CR14","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":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"issue":"6","key":"5_CR17","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1093\/comjnl\/29.6.531","volume":"29","author":"P. Pandya","year":"1986","unstructured":"Pandya, P., Joseph, M.: A Structure-directed Total Correctness Proof Rule for Recursive Procedure Calls. The Computer Journal\u00a029(6), 531\u2013537 (1986)","journal-title":"The Computer Journal"},{"key":"5_CR18","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, New York (1994)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BFb0105417","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"1996","unstructured":"Slind, K.: Function definition in Higher-Order Logic. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 381\u2013397. Springer, Heidelberg (1996)"},{"unstructured":"Slind, K.: Reasoning About Terminating Functional Programs. PhD thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen (1999)","key":"5_CR21"},{"issue":"1","key":"5_CR22","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. Artif. Intell.\u00a071(1), 101\u2013157 (1994)","journal-title":"Artif. Intell."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,22]],"date-time":"2021-08-22T05:08:16Z","timestamp":1629608896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}