Skip to main content
SpringerLink
Log in

LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11893))

Included in the following conference series:

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.

We thank Ekaterina Komendantskaya, Josef Urban, and anonymous reviewers for APLAS2019 for their valuable comments on an early draft of this paper. This work was supported by the European Regional Development Fund under the project AI & Reasoning (reg. no.CZ.02.1.01/0.0/0.0/15_003/0000466).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Proof methods are the Isar syntactic layer of LCF-style tactics.

  2. 2.

    Recursion induction is also known as functional induction or computation induction.

  3. 3.

    This naive heuristic is not very reliable: there are cases where the induct method takes terms involving constants and apply induction appropriately by automatically introducing induction variables. See Concrete Semantics [25] for more details.

  4. 4.

    For better readability we omit parentheses where the binding of terms is obvious from indentation.

  5. 5.

    Note that in reality the counting starts at 0 internally. Therefore, “the first argument” in this English sentence is processed as the 0th argument within LiFtEr.

References

  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/4593

    Article  MathSciNet  MATH  Google Scholar 

  2. Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, Perspectives in Computing, vol. 23. Academic Press, Boston (1979)

    Google Scholar 

  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. 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_7

    Chapter  MATH  Google Scholar 

  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_2

    Chapter  Google Scholar 

  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.006

    Article  MATH  Google Scholar 

  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/BFb0031814

    Chapter  Google Scholar 

  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_27

    Chapter  MATH  Google Scholar 

  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_6

    Chapter  Google Scholar 

  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.588534

    Article  Google Scholar 

  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.1743574

    Article  Google Scholar 

  12. Klein, G., Nipkow, T., Paulson, L., Thiemann, R.: The Archive of Formal Proofs (2004). https://www.isa-afp.org/

  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_21

    Chapter  Google Scholar 

  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. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). https://doi.org/10.1145/1538788.1538814

    Article  Google Scholar 

  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-2

    Article  MathSciNet  MATH  Google Scholar 

  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. 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_22

    Chapter  Google Scholar 

  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. Nagashima, Y.: data61/PSL. https://github.com/data61/PSL/releases/tag/v0.1.4-alpha

  21. Nagashima, Y.: Towards machine learning mathematical induction. CoRR abs/1812.04088 (2018). http://arxiv.org/abs/1812.04088

  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. 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

    Chapter  Google Scholar 

  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_19

    Chapter  Google Scholar 

  25. Nipkow, T., Klein, G.: Concrete Semantics - With Isabelle/HOL. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10542-0

    Book  MATH  Google Scholar 

  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-9

    Book  MATH  Google Scholar 

  27. The Coq development team: The Coq proof assistant. https://coq.inria.fr

  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_38

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Czech Technical University in Prague, Prague, Czech Republic

    Yutaka Nagashima

  2. University of Innsbruck, Innsbruck, Austria

    Yutaka Nagashima

Authors
  1. Yutaka Nagashima
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yutaka Nagashima .

Editor information

Editors and Affiliations

  1. University of Kaiserslautern, Kaiserslautern, Germany

    Anthony Widjaja Lin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Nagashima, Y. (2019). LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL. In: Lin, A. (eds) Programming Languages and Systems. APLAS 2019. Lecture Notes in Computer Science(), vol 11893. Springer, Cham. https://doi.org/10.1007/978-3-030-34175-6_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34175-6_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34174-9

  • Online ISBN: 978-3-030-34175-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation