Abstract
We present a succinct account of dynamic rippling, a technique used to guide the automation of inductive proofs. This simplifies termination proofs for rippling and hence facilitates extending the technique in ways that preserve termination. We illustrate this by extending rippling with a terminating version of middle-out reasoning for lemma speculation. This supports automatic speculation of schematic lemmas which are incrementally instantiated by unification as the rippling proof progresses. Middle-out reasoning and lemma speculation have been implemented in higher-order logic and evaluated on typical libraries of formalised mathematics. This reveals that, when applied, the technique often finds the needed lemmas to complete the proof, but it is not as frequently applicable as initially expected. In comparison, we show that theory formation methods, combined with simpler proof methods, offer an effective alternative.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aderhold, M.: Improvements in formula generalization. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 231–246. Springer, Heidelberg (2007)
Armando, A., Smaill, A., Green, I.: Automatic synthesis of recursive programs: the proof-planning paradigm. In: ASE 1997, pp. 2–9. IEEE Computer Society Press, Los Alamitos (1997)
Basin, D., Walsh, T.: A calculus for and termination of rippling. Journal of Automated Reasoning 16(1-2), 147–180 (1996)
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 4(4), 470–504 (2006)
Bundy, A.: The automation of proof by mathematical induction. In: Handbook of Automated Reasoning, ch. 13. MIT Press, Cambridge (2001)
Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge (2005)
Bundy, A., Dixon, L., Gow, J., Fleuriot, J.: Constructing induction rules for deductive synthesis proofs. In: CLASE 2005. ENTCS, vol. 153, pp. 3–21 (2006)
Bundy, A., Smaill, A., Hesketh, J.: Turning Eureka steps into calculations in automatic program synthesis. In: UK IT 1990, pp. 221–226 (1990)
Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A.: Experiments with proof plans for induction. Journal of Automated Reasoning 7(3), 303–324 (1992)
Cook, A., Ireland, A., Michaelson, G.: Higher order function synthesis through proof planning. In: ASE-16, pp. 307–310 (2001)
Dixon, L.: A Proof Planning Framework for Isabelle. PhD thesis, University of Edinburgh (2005)
Dixon, L., Fleuriot, J.: Higher-order rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 83–98. Springer, Heidelberg (2004)
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. 607, pp. 310–324. Springer, Heidelberg (1992)
Hodorog, M., Craciun, A.: Scheme-based systematic exploration of natural numbers. In: Synasc-8, pp. 26–34 (2006)
Ireland, A., Bundy, A.: Productive use of failure in inductive proof. Journal of Automated Reasoning 16(1-2), 79–111 (1996)
Ireland, A., Jackson, M., Reid, G.: Interactive proof critics. Formal Aspects of Computing 11(3), 302–325 (1999)
Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. Journal of Automated Reasoning (to appear, 2010)
Kapur, D., Subramaniam, M.: Lemma discovery in automating induction. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 538–552. Springer, Heidelberg (1996)
Kraan, I., Basin, D., Bundy, A.: Middle-out reasoning for synthesis and induction. Journal of Automated Reasoning 16(1-2), 113–145 (1996)
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 10(23), 135–149 (2007)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL - A proof assistant for higher-order logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Prehofer, C.: Higher-order narrowing. In: LICS-9, pp. 507–516. IEEE Computer Society Press, Los Alamitos (1994)
Smaill, A., Green, I.: Higher-order annotated terms for proof search. In: von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 399–413. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Johansson, M., Dixon, L., Bundy, A. (2010). Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery. In: Siegler, S., Wasser, N. (eds) Verification, Induction, Termination Analysis. Lecture Notes in Computer Science(), vol 6463. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17172-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-17172-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17171-0
Online ISBN: 978-3-642-17172-7
eBook Packages: Computer ScienceComputer Science (R0)