Abstract
Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluation shows that our working prototype, TBC, achieved 50% point improvement of success rates for problems at intermediate difficulty level.
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
Similar content being viewed by others
Notes
- 1.
Answer: Sledgehammer used the simp tactic with an auxiliary lemma about identity. Furthermore, IsSolved resulted in the done command in the script.
References
Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_11
Bulwahn, L.: The new quickcheck for isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92–108. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35308-6_10
Bundy, A., Basin, D.A., Hutter, D., Ireland, A.: Rippling - meta-level guidance for mathematical reasoning, Cambridge tracts in theoretical computer science, vol. 56. 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., Johansson, M., Rosén, D., Smallbone, N.: HipSpec: automating inductive proofs of program properties. In: Fleuriot, J.D., Höfner, P., McIver, A., Smaill, A. (eds.) ATx 2012/WInG’12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation, Manchester, UK, June 2012. EPiC Series in Computing, vol. 17, pp. 16–25. EasyChair (2012). https://doi.org/10.29007/3qwr
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
Einarsdóttir, S.H., Smallbone, N., Johansson, M.: Template-based theory exploration: discovering properties of functional programs by testing. In: Chitil, O. (ed.) IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages, Virtual Event/Canterbury, UK, 2-4 September 2020, pp. 67–78. ACM (2020). https://doi.org/10.1145/3462172.3462192
Einarsdóttir, S.H., Johansson, M., Smallbone, N.: LOL: A library of lemma templates for data-driven conjecturing. In: Buzzard, K., Kutsia, T. (eds.) Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics (CICM 2022) Informal Proceedings (2022). http://www3.risc.jku.at/publications/download/risc_6584/proceedings-CICM2022-informal.pdf#page=28
Hajdú, M., Hozzová, P., Kovács, L., Voronkov, A.: Induction with recursive definitions in superposition. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021, pp. 1–10. IEEE (2021). https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_34
Johansson, M.: Automated theory exploration for interactive theorem proving. 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.: Lemma discovery for induction. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 125–139. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-23250-4_9
Kaufmann, M., Panagiotis Manolios, J.S.M. (ed.): Computer-Aided Reasoning ACL2 Case Studies. Advances in Formal Methods, Springer, New York, NY (2000). https://doi.org/10.1007/978-1-4757-3188-0
Nagashima, Y.: LiFtEr: language to encode induction heuristics for Isabelle/HOL. In: Lin, A.W. (ed.) APLAS 2019. LNCS, vol. 11893, pp. 266–287. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-34175-6_14
Nagashima, Y.: Smart induction for Isabelle/HOL (tool paper). In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21-24 September 2020, pp. 245–254. IEEE (2020). https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_32
Nagashima, Y.: Faster smarter proof by induction in Isabelle/HOL. In: Zhou, Z. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pp. 1981–1988. ijcai.org (2021). https://doi.org/10.24963/ijcai.2021/273
Nagashima, Y.: Definitional quantifiers realise semantic reasoning for proof by induction. In: Kovács, L., Meinke, K. (eds.) Tests and Proofs - 16th International Conference, TAP 2022, Held as Part of STAF 2022, Nantes, France, July 5, 2022, Proceedings, LNCS, vol. 13361, pp. 48–66. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-09827-7_4
Nagashima, Y., Kumar, R.: A proof strategy language and proof script generation for Isabelle/HOL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 528–545. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_32
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., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
Passmore, G., et al.: The Imandra automated reasoning system (System description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 464–471. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_30
Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011. EPiC Series in Computing, vol. 2, pp. 1–11. EasyChair (2010). https://doi.org/10.29007/36dt
Reger, G., Voronkov, A.: Induction in saturation-based proof search. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 477–494. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29436-6_28
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendix
Appendix
Program 4 shows the output of TBC for our running example. The original goal is proved using commutativity_5382730, which is in turn proved using identity_5382590. 8 out of 10 proved conjectures are not used to prove the final goal; however, TBC outputs them, so that users may exploit them in future.
Rights and permissions
Copyright information
© 2023 IFIP International Federation for Information Processing
About this paper
Cite this paper
Nagashima, Y., Xu, Z., Wang, N., Goc, D.S., Bang, J. (2023). Template-Based Conjecturing for Automated Induction in Isabelle/HOL. In: Hojjat, H., Ábrahám, E. (eds) Fundamentals of Software Engineering. FSEN 2023. Lecture Notes in Computer Science, vol 14155 . Springer, Cham. https://doi.org/10.1007/978-3-031-42441-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-031-42441-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-42440-3
Online ISBN: 978-3-031-42441-0
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
