Advertisement

LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL

  • Yutaka NagashimaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11893)

Abstract

Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, there is a little tool support for transferring this expert knowledge to a wider user audience. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr’s interpreter mechanically checks if a given application of induction tool matches the heuristics, thus automating the knowledge transfer loop.

Keywords

Induction Isabelle/HOL Domain-specific language 

References

  1. 1.
    Blanchette, J., Kaliszyk, C., Paulson, L., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101–148 (2016).  https://doi.org/10.6092/issn.1972-5787/4593MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, Perspectives in Computing, vol. 23. Academic Press, Boston (1979)Google Scholar
  3. 3.
    Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 845–911. Elsevier and MIT Press (2001)Google Scholar
  4. 4.
    Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNAI, vol. 1955, pp. 85–95. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44404-1_7CrossRefzbMATHGoogle Scholar
  5. 5.
    Torra, V., Karlsson, A., Steinhauer, H.J., Berglund, S.: Artificial intelligence. In: Said, A., Torra, V. (eds.) Data Science in Practice. SBD, vol. 46, pp. 9–26. Springer, Cham (2019).  https://doi.org/10.1007/978-3-319-97556-6_2CrossRefGoogle Scholar
  6. 6.
    Gramlich, B.: Strategic issues, problems and challenges in inductive theorem proving. Electr. Notes Theor. Comput. Sci. 125(2), 5–43 (2005).  https://doi.org/10.1016/j.entcs.2005.01.006CrossRefzbMATHGoogle Scholar
  7. 7.
    Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996).  https://doi.org/10.1007/BFb0031814CrossRefGoogle Scholar
  8. 8.
    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_27CrossRefzbMATHGoogle Scholar
  9. 9.
    Jiang, Y., Papapanagiotou, P., Fleuriot, J.: Machine learning for inductive theorem proving. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) AISC 2018. LNCS (LNAI), vol. 11110, pp. 87–103. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-99957-9_6CrossRefGoogle Scholar
  10. 10.
    Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on Common Lisp. IEEE Trans. Software Eng. 23(4), 203–213 (1997).  https://doi.org/10.1109/32.588534CrossRefGoogle Scholar
  11. 11.
    Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010).  https://doi.org/10.1145/1743546.1743574CrossRefGoogle Scholar
  12. 12.
    Klein, G., Nipkow, T., Paulson, L., Thiemann, R.: The Archive of Formal Proofs (2004). https://www.isa-afp.org/
  13. 13.
    Komendantskaya, E., Heras, J.: Proof mining with dependent types. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 303–318. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-62075-6_21CrossRefGoogle Scholar
  14. 14.
    Lammich, P., Wimmer, S.: IMP2 - simple program verification in Isabelle/HOL. Arch. Formal Proofs 2019 (2019). https://www.isa-afp.org/entries/IMP2.html
  15. 15.
    Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009).  https://doi.org/10.1145/1538788.1538814CrossRefGoogle Scholar
  16. 16.
    Matichuk, D., Murray, T.C., Wenzel, M.: Eisbach: a proof method language for Isabelle. J. Autom. Reasoning 56(3), 261–282 (2016).  https://doi.org/10.1007/s10817-015-9360-2MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Moore, J.S.: Computational logic: structure sharing and proof of program properties. Ph.D. thesis, University of Edinburgh, UK (1973). http://hdl.handle.net/1842/2245
  18. 18.
    Moore, J.S.: Symbolic simulation: an ACL2 approach. In: Formal Methods in Computer-Aided Design, Second International Conference, FMCAD 1998, Palo Alto, California, USA, 4–6 November 1998, Proceedings, pp. 334–350 (1998).  https://doi.org/10.1007/3-540-49519-3_22CrossRefGoogle Scholar
  19. 19.
    Moore, J.S., Wirth, C.: Automation of mathematical induction as part of the history of logic. CoRR abs/1309.6226 (2013). http://arxiv.org/abs/1309.6226
  20. 20.
  21. 21.
    Nagashima, Y.: Towards machine learning mathematical induction. CoRR abs/1812.04088 (2018). http://arxiv.org/abs/1812.04088
  22. 22.
    Nagashima, Y., He, Y.: PaMpeR: proof method recommendation system for Isabelle/HOL. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, 3–7 September 2018, pp. 362–372 (2018).  https://doi.org/10.1145/3238147.3238210
  23. 23.
    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_32CrossRefGoogle Scholar
  24. 24.
    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_19CrossRefGoogle Scholar
  25. 25.
    Nipkow, T., Klein, G.: Concrete Semantics - With Isabelle/HOL. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10542-0CrossRefzbMATHGoogle Scholar
  26. 26.
    Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45949-9CrossRefzbMATHGoogle Scholar
  27. 27.
    The Coq development team: The Coq proof assistant. https://coq.inria.fr
  28. 28.
    Wenzel, M.: Isabelle/jEdit – a prover IDE within the PIDE framework. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 468–471. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31374-5_38CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Czech Technical University in PraguePragueCzech Republic
  2. 2.University of InnsbruckInnsbruckAustria

Personalised recommendations