{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:03:10Z","timestamp":1771059790602,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642171710","type":"print"},{"value":"9783642171727","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17172-7_6","type":"book-chapter","created":{"date-parts":[[2010,11,2]],"date-time":"2010-11-02T13:17:15Z","timestamp":1288703835000},"page":"102-116","source":"Crossref","is-referenced-by-count":6,"title":["Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery"],"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":"6_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)"},{"key":"6_CR2","first-page":"2","volume-title":"ASE 1997","author":"A. Armando","year":"1997","unstructured":"Armando, A., Smaill, A., Green, I.: Automatic synthesis of recursive programs: the proof-planning paradigm. In: ASE 1997, pp. 2\u20139. IEEE Computer Society Press, Los Alamitos (1997)"},{"issue":"1-2","key":"6_CR3","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D. Basin","year":"1996","unstructured":"Basin, D., Walsh, T.: A calculus for and termination of rippling. Journal of Automated Reasoning\u00a016(1-2), 147\u2013180 (1996)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"6_CR4","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B. Buchberger","year":"2006","unstructured":"Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkrantz, M., Windsteiger, W.: Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic\u00a04(4), 470\u2013504 (2006)","journal-title":"Journal of Applied Logic"},{"key":"6_CR5","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, ch. 13. MIT Press, Cambridge (2001)"},{"key":"6_CR6","doi-asserted-by":"publisher","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 University Press, Cambridge (2005)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Bundy, A., Dixon, L., Gow, J., Fleuriot, J.: Constructing induction rules for deductive synthesis proofs. In: CLASE 2005. ENTCS, vol.\u00a0153, pp. 3\u201321 (2006)","DOI":"10.1016\/j.entcs.2005.08.003"},{"key":"6_CR8","unstructured":"Bundy, A., Smaill, A., Hesketh, J.: Turning Eureka steps into calculations in automatic program synthesis. In: UK IT 1990, pp. 221\u2013226 (1990)"},{"issue":"3","key":"6_CR9","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1992","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. Journal of Automated Reasoning\u00a07(3), 303\u2013324 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Cook, A., Ireland, A., Michaelson, G.: Higher order function synthesis through proof planning. In: ASE-16, pp. 307\u2013310 (2001)","DOI":"10.1109\/ASE.2001.989817"},{"key":"6_CR11","unstructured":"Dixon, L.: A Proof Planning Framework for Isabelle. PhD thesis, University of Edinburgh (2005)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: 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)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/3-540-55602-8_174","volume-title":"Automated Deduction - CADE-11","author":"J. Hesketh","year":"1992","unstructured":"Hesketh, J., Bundy, A., Smaill, A.: Using middle-out reasoning to control the synthesis of tail-recursive programs. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 310\u2013324. Springer, Heidelberg (1992)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Hodorog, M., Craciun, A.: Scheme-based systematic exploration of natural numbers. In: Synasc-8, pp. 26\u201334 (2006)","DOI":"10.1109\/SYNASC.2006.67"},{"issue":"1-2","key":"6_CR15","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. Journal of Automated Reasoning\u00a016(1-2), 79\u2013111 (1996)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"6_CR16","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/s001650050052","volume":"11","author":"A. Ireland","year":"1999","unstructured":"Ireland, A., Jackson, M., Reid, G.: Interactive proof critics. Formal Aspects of Computing\u00a011(3), 302\u2013325 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. Journal of Automated Reasoning (to appear, 2010)","DOI":"10.1007\/s10817-010-9193-y"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/3-540-61511-3_112","volume-title":"Automated Deduction - Cade-13","author":"D. Kapur","year":"1996","unstructured":"Kapur, D., Subramaniam, M.: Lemma discovery in automating induction. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 538\u2013552. Springer, Heidelberg (1996)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Kraan, I., Basin, D., Bundy, A.: Middle-out reasoning for synthesis and induction. Journal of Automated Reasoning\u00a016(1-2), 113\u2013145 (1996)","DOI":"10.1007\/BF00244461"},{"issue":"23","key":"6_CR20","first-page":"135","volume":"10","author":"R. McCasland","year":"2007","unstructured":"McCasland, R., Bundy, A., Autexier, S.: Automated discovery of inductive theorems. Special Issue of Studies in Logic, Grammar and Rhetoric: Festschrift in Honor of A. Trybulec\u00a010(23), 135\u2013149 (2007)","journal-title":"Special Issue of Studies in Logic, Grammar and Rhetoric: Festschrift in Honor of A. Trybulec"},{"key":"6_CR21","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.T.: Isabelle\/HOL - A proof assistant for higher-order logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"6_CR22","first-page":"507","volume-title":"LICS-9","author":"C. Prehofer","year":"1994","unstructured":"Prehofer, C.: Higher-order narrowing. In: LICS-9, pp. 507\u2013516. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 399\u2013413. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Verification, Induction, Termination Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17172-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T00:56:15Z","timestamp":1559782575000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17172-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171710","9783642171727"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17172-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}