{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:06:53Z","timestamp":1768000013823,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_21","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"291-306","source":"Crossref","is-referenced-by-count":20,"title":["Case-Analysis for Rippling and Inductive Proof"],"prefix":"10.1007","author":[{"given":"Moa","family":"Johansson","sequence":"first","affiliation":[]},{"given":"Lucas","family":"Dixon","sequence":"additional","affiliation":[]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-73595-3_16","volume-title":"Automated Deduction \u2013 CADE-21","author":"M. Aderhold","year":"2007","unstructured":"Aderhold, M.: Improvements in formula generalization. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 231\u2013246. Springer, Heidelberg (2007)"},{"issue":"4","key":"21_CR2","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1023\/A:1008763422061","volume":"6","author":"A. Armando","year":"1999","unstructured":"Armando, A., Smaill, A., Green, I.: Automatic synthesis of recursive programs: The proof-planning paradigm. Automated Software Engineering\u00a06(4), 329\u2013356 (1999)","journal-title":"Automated Software Engineering"},{"key":"21_CR3","series-title":"ACM monograph series","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. ACM monograph series. Academic Press, London (1979)"},{"key":"21_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50015-1","volume-title":"Handbook of Automated Reasoning","author":"A. Bundy","year":"2001","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Handbook of Automated Reasoning, vol.\u00a01. Elsevier, Amsterdam (2001)"},{"key":"21_CR5","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling: Meta-level Guidance for Mathematical Reasoning","author":"A. Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge Tracts in Theoretical Computer Science, vol.\u00a056. Cambridge University Press, Cambridge (2005)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Bundy, A., Dixon, L., Gow, J., Fleuriot, J.: Constructing induction rules for deductive synthesis proofs. In: CLASE at ETAPS-8. ENTCS, vol.\u00a0153, pp. 3\u201321 (2006)","DOI":"10.1016\/j.entcs.2005.08.003"},{"issue":"2","key":"21_CR7","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence\u00a062(2), 185\u2013253 (1993)","journal-title":"Artificial Intelligence"},{"key":"21_CR8","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol.\u00a0449, pp. 647\u2013648. Springer, Heidelberg (1990)"},{"key":"21_CR9","unstructured":"Dixon, L.: A Proof Planning Framework for Isabelle. PhD thesis, University of Edinburgh (2006)"},{"key":"21_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L. Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.D.: IsaPlanner: A prototype proof planner in Isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 279\u2013283. Springer, Heidelberg (2003)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-540-30142-4_7","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Dixon","year":"2004","unstructured":"Dixon, L., Fleuriot, J.D.: Higher order rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 83\u201398. Springer, Heidelberg (2004)"},{"issue":"5","key":"21_CR12","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"G. Huet","year":"1997","unstructured":"Huet, G.: The zipper. Journal of Functional Programming\u00a07(5), 549\u2013554 (1997)","journal-title":"Journal of Functional Programming"},{"issue":"1-2","key":"21_CR13","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"Ireland, A., Bundy, A.: Productive use of failure in inductive proof. JAR\u00a016(1-2), 79\u2013111 (1996)","journal-title":"JAR"},{"issue":"4","key":"21_CR14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common Lisp. IEEE Transactions on Software Engineering\u00a023(4), 203\u2013213 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"21_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A generic theorem prover. Springer, Heidelberg (1994)"},{"key":"21_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BFb0054254","volume-title":"Automated Deduction - CADE-15","author":"J.D.C. Richardson","year":"1998","unstructured":"Richardson, J.D.C., Smaill, A., Green, I.: System description: proof planning in higher-order logic with Lambda-Clam. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 129\u2013133. Springer, Heidelberg (1998)"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BFb0105418","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Smaill","year":"1996","unstructured":"Smaill, A., Green, I.: Higher-order annotated terms for proof search. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 399\u2013413. Springer, Heidelberg (1996)"},{"key":"21_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","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)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Wilson, S., Fleuriot, J., Smaill, A.: Automation for dependently typed functional programming. Special Issue on Dependently Typed Programming of Fundamental Informaticae (2009)","DOI":"10.3233\/FI-2010-305"}],"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-14052-5_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:01Z","timestamp":1606186021000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}