Abstract
Automating proofs by induction can be challenging, not least because proofs might need auxiliary lemmas, which themselves need to be proved by induction. In this paper we survey various techniques for automating the discovery of such lemmas, including both top-down techniques attempting to generate a lemma from an ongoing proof attempt, as well as bottom-up theory exploration techniques trying to construct interesting lemmas about available functions and datatypes, thus constructing a richer background theory.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A small program executing one or several proof steps automatically.
References
Aderhold, M.: Improvements in formula generalization. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 231–246. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_16
Aubin, R.: Mechanizing structural induction. Ph.D. thesis, University of Edinburgh (1976)
Boyer, R.S., Moore, J.S.: A Computational Logic. ACM Monographs in Computer Science (1979)
Buchberger, B.: Theory exploration with Theorema. Analele Universitatii Din Timisoara ser. Mat.-Informatica 38(2), 9–32 (2000)
Buchberger, B., et al.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Log. 4(4), 470–504 (2006). Towards Computer Aided Mathematics
Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988). https://doi.org/10.1007/BFb0012826
Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge (2005)
Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The OYSTER-CLAM system. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 647–648. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52885-7_123
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of ICFP, pp. 268–279 (2000)
Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392–406. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_27
Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: TIP: tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 333–337. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_23
Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 6–21. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13977-2_3
Constable, R.L., Allen, S.F., Bromley, H.M.: Implementing Mathematics with the nuPRL Development System. Prentice Hall, Upper Saddle River (1986)
Cruanes, S.: Superposition with structural induction. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 172–188. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_10
Dixon, L., Fleuriot, J.: Higher order rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 83–98. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30142-4_7
Dixon, L., Johansson, M.: IsaPlanner 2: a proof planner in Isabelle. DReaM Technical report (System description) (2007)
Einarsdóttir, S.H., Johansson, M., Åman Pohjola, J.: Into the infinite - theory exploration for coinduction. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) AISC 2018. LNCS (LNAI), vol. 11110, pp. 70–86. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99957-9_5
Gauthier, T., Kaliszyk, C., Urban, J.: Initial experiments with statistical conjecturing over large formal corpora. In: Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 (CICM-WiP 2016). CEUR, vol. 1785, pp. 219–228. CEUR-WS.org (2016)
Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-pattern recognition and lemma discovery in ACL2. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 389–406. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_27
Hesketh, J.: Using middle out reasoning to guide inductive theorem proving. Ph.D. thesis, University of Edinburgh (1992)
Hummel, B.: An investigation of formula generalization heuristics for inductive proofs. Interner Bericht Nr, 6/87, Universität Karlsruhe (1987)
Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J. Autom. Reasoning 16, 79–111 (1996)
Johansson, M.: Automated theory exploration for interactive theorem proving: an introduction to the hipster system. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 1–11. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_1
Johansson, M., Dixon, L., Bundy, A.: Dynamic rippling, middle-out reasoning and lemma discovery. In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis. LNCS (LNAI), vol. 6463, pp. 102–116. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17172-7_6
Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J. Autom. Reasoning 47(3), 251–289 (2011)
Johansson, M., Rosén, D., Smallbone, N., Claessen, K.: Hipster: integrating theory exploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 108–122. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_9
Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with flyspeck. J. Autom. Reasoning 53(2), 173–213 (2014)
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). https://doi.org/10.1007/3-540-61511-3_112
Kaufmann, M., Panagiotis, M., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)
Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315–331. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_21
Maclean, E.: Generalisation as a critic. Master’s thesis, University of Edinburgh (1999)
McCasland, R., Bundy, A., Autexier, S.: Automated discovery of inductive theorems. In: Matuszewski, R., Rudnicki, P. (eds.) From Insight to Proof: Festschrift in Honor of A. Trybulec (2007)
McCasland, R., Bundy, A., Smith, P.: MATHsAiD: automated mathematical theory exploration. Appl. Intell. 47(3), 585–606 (2017)
Montano-Rivas, O., McCasland, R., Dixon, L., Bundy, A.: Scheme-based theorem discovery and concept invention. Expert Syst. Appl. 39(2), 1637–1646 (2012)
Moore, J.S., Wirth, C.-P.: Automation of mathematical induction as part of the history of logic. IfCoLog J. Log. Their Appl. 4(5), 1505–1634 (2014). SEKI-Report SR-2013-02
Nagashima, Y., Parsert, J.: Goal-oriented conjecturing for Isabelle/HOL. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 225–231. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96812-4_19
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
Papapanagiotou, P., Fleuriot, J.: The Boyer-Moore waterfall model revisited (2011). https://arxiv.org/pdf/1808.03810.pdf
Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL-2010 (2010)
Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80–98. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46081-8_5
Smallbone, N., Johansson, M., Claessen, K., Algehed, M.: Quick specifications for the busy programmer. J. Funct. Program. 27, e18 (2017)
Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: an automated prover for properties of recursive data structures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407–421. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_28
Sonnex, W.: Fixed point promotion: taking the induction out of automated induction. Technical report UCAM-CL-TR-905, University of Cambridge, Computer Laboratory, March 2017
Wand, D.: Superposition: types and induction. Ph.D. thesis, Saarland University (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Johansson, M. (2019). Lemma Discovery for Induction. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds) Intelligent Computer Mathematics. CICM 2019. Lecture Notes in Computer Science(), vol 11617. Springer, Cham. https://doi.org/10.1007/978-3-030-23250-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-23250-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-23249-8
Online ISBN: 978-3-030-23250-4
eBook Packages: Computer ScienceComputer Science (R0)