Skip to main content
SpringerLink
Log in

Sharing HOL4 and HOL Light Proof Knowledge

  • Conference paper
  • First Online:
Book cover Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9450))

Included in the following conference series:

Abstract

New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In this paper we propose and evaluate a number of methods, which strengthen proof automation by learning from proof libraries of different provers. Certain conjectures can be proved directly from the dependencies induced by similar proofs in the other library. Even if exact correspondences are not found, learning-reasoning systems can make use of the association between proved theorems and their characteristics to predict the relevant premises. Such external help can be further combined with internal advice. We evaluate the proposed knowledge-sharing methods by reproving the HOL Light and HOL4 standard libraries. The learning-reasoning system HOL(y)Hammer, whose single best strategy could automatically find proofs for 30 % of the HOL Light problems, can prove 40 % with the knowledge from HOL4.

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

References

  1. Adams, M.: The common HOL platform. In: Kaliszyk, C., Paskevich, A., (eds.) Fourth International Workshop on Proof Exchange for Theorem Proving, PxTP 2015, Berlin, Germany, 2–3 August 2015. to appear in EPTCS (2015)

    Google Scholar 

  2. Asperti, A., Ricciotti, W., Coen, C.S.: Matita tutorial. J. Formaliz. Reason. 7(2), 91–199 (2014)

    MathSciNet  Google Scholar 

  3. Autexier, S., Hutter, D.: Structure formation in large theories. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 155–170. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  4. Blanchette, J.C., Haslbeck, M., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 3–17. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  5. Bortin, M., Johnsen, E.B., Lüth, C.: Structured formal development in Isabelle. Nordic J. Comput. 13, 1–20 (2006)

    MathSciNet  Google Scholar 

  6. Gauthier, T., Kaliszyk, C.: Matching concepts across HOL libraries. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 267–281. Springer, Heidelberg (2014)

    Google Scholar 

  7. Gauthier, T., Kaliszyk, C.: Premise selection and external provers for HOL4. In: Leroy, X., Tiu, A., (eds.) Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pp. 49–57 (2015)

    Google Scholar 

  8. Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104. Springer, Heidelberg (1996)

    Google Scholar 

  9. Harrison, J.: HOL Light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Huet, G., Herbelin, H.: 30 years of research and development around Coq. In: Jagannathan, S., Sewell, P., (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 249–250. ACM (2014)

    Google Scholar 

  11. Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Muñoz, C., (eds.) Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical reports, pp. 56–68, September 2003

    Google Scholar 

  12. Hurd, J.: The OpenTheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 177–191. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Kaliszyk, C., Krauss, A.: Scalable LCF-Style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 51–66. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  14. Kaliszyk, C., Rabe, F.: Towards knowledge management for HOL Light. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 357–372. Springer, Heidelberg (2014)

    Google Scholar 

  15. Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173–213 (2014)

    Article  MathSciNet  Google Scholar 

  16. Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5–22 (2015)

    Article  MATH  MathSciNet  Google Scholar 

  17. Kaliszyk, C., Urban, J., Vyskočil, J.: Efficient semantic features for automated reasoning over large theories. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence, IJCAI 2015 (2015). (to appear)

    Google Scholar 

  18. Keller, C., Werner, B.: Importing HOL Light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307–322. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  19. The Mizar Mathematical Library. http://mizar.org/

  20. Obua, S., Skalberg, S.: Importing HOL into isabelle/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 298–302. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In: 8th IWIL (2010). Invited talk

    Google Scholar 

  22. Rabe, F.: The MMT API: a generic MKM system. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 339–343. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  23. Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Acknowledgments

This work has been supported by the Austrian Science Fund (FWF): P26201.

Author information

Authors and Affiliations

  1. University of Innsbruck, Innsbruck, Austria

    Thibault Gauthier & Cezary Kaliszyk

Authors
  1. Thibault Gauthier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cezary Kaliszyk
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Thibault Gauthier .

Editor information

Editors and Affiliations

  1. New York University, New York, New York, USA

    Martin Davis

  2. University of the South Pacific, Suva, Fiji

    Ansgar Fehnker

  3. Macquarie University, Sydney, New South Wales, Australia

    Annabelle McIver

  4. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gauthier, T., Kaliszyk, C. (2015). Sharing HOL4 and HOL Light Proof Knowledge. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015. Lecture Notes in Computer Science(), vol 9450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48899-7_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48898-0

  • Online ISBN: 978-3-662-48899-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation