Document Open Access Logo

Automated Theorem Proving for Metamath

Authors Mario Carneiro , Chad E. Brown, Josef Urban

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.9.pdf
  • Filesize: 0.75 MB
  • 19 pages

Document Identifiers

Author Details

Mario Carneiro
  • Carnegie Mellon University, Pittsburgh, PA, USA
Chad E. Brown
  • Czech Technical University in Prague, Czech Republic
Josef Urban
  • Czech Technical University in Prague, Czech Republic

Funding

This work was partially supported by the European Regional Development Fund under the Czech project AI&Reasoning no. CZ.02.1.01/0.0/0.0/15_003/0000466 (CB, JU), Amazon Research Awards (CB, JU), the Czech MEYS under the ERC CZ project POSTMAN no. LL1902 (CB), and the EU ICT-48 2020 project TAILOR no. 952215 (JU).
  • Carneiro, Mario: Supported by the Hoskinson Center for Formal Mathematics at CMU.

Cite AsGet BibTex

Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.9

Abstract

Metamath is a proof assistant that keeps surprising outsiders by its combination of a very minimalist design with a large library of advanced results, ranking high on the Freek Wiedijk’s 100 list. In this work, we develop several translations of the Metamath logic and its large set-theoretical library into higher-order and first-order TPTP formats for automated theorem provers (ATPs). We show that state-of-the-art ATPs can prove 68% of the Metamath problems automatically when using the premises that were used in the human-written Metamath proofs. Finally, we add proof reconstruction and premise selection methods and combine the components into the first hammer system for Metamath.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Higher order logic
  • Theory of computation → Logic and verification
Keywords
  • Metamath
  • Automated theorem proving
  • Interactive theorem proving
  • Formal proof assistants
  • proof discovery

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52(2):191-213, 2014. URL: https://doi.org/10.1007/s10817-013-9286-5.
  2. Ahmed Bhayat and Giles Reger. A combinator-based superposition calculus for higher-order logic. In IJCAR (1), volume 12166 of Lecture Notes in Computer Science, pages 278-296. Springer, 2020. Google Scholar
  3. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, CADE, volume 6803 of LNCS, pages 116-130. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_11.
  4. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101-148, 2016. URL: https://doi.org/10.6092/issn.1972-5787/4593.
  5. Mario Carneiro. Metamath zero: Designing a theorem prover prover. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings, pages 71-88, Berlin, Heidelberg, 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-53518-6_5.
  6. Simon Cruanes. Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. Theses, École polytechnique, September 2015. URL: https://hal.archives-ouvertes.fr/tel-01223502.
  7. Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. J. Autom. Reason., 61(1-4):423-453, 2018. Google Scholar
  8. Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen provers under the hammer, 2022. URL: https://matryoshka-project.github.io/pubs/seventeen.pdf.
  9. Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. Smtcoq: A plug-in for integrating SMT solvers into coq. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 126-133. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_7.
  10. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Certified Programs and Proofs (CPP'15), LNCS. Springer, 2015. URL: https://doi.org/10.1145/2676724.2693173.
  11. Allen Van Gelder and Geoff Sutcliffe. Extending the TPTP language to higher-order logic with automated parser generation. In Ulrich Furbach and Natarajan Shankar, editors, IJCAR, volume 4130 of LNCS, pages 156-161. Springer, 2006. URL: https://doi.org/10.1007/11814771_15.
  12. Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller. A revision of the proof of the Kepler conjecture. Discrete & Computational Geometry, 44(1):1-34, 2010. URL: https://doi.org/10.1007/s00454-009-9148-4.
  13. Jan Jakubův and Josef Urban. BliStrTune: hierarchical invention of theorem proving strategies. In Yves Bertot and Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 43-52. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018619.
  14. Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. Mizar 60 for mizar 50. CoRR, abs/2303.06686, 2023. URL: https://doi.org/10.48550/arXiv.2303.06686.
  15. Cezary Kaliszyk and Josef Urban. HOL(y)Hammer: Online ATP service for HOL Light. Mathematics in Computer Science, 9(1):5-22, 2015. Google Scholar
  16. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. Journal of Automated Reasoning, 55(3):245-256, 2015. URL: https://doi.org/10.1007/s10817-015-9330-8.
  17. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, CAV, volume 8044 of LNCS, pages 1-35. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_1.
  18. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: Machine learning for Sledgehammer. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP 2013, volume 7998 of LNCS, pages 35-50. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_6.
  19. William McCune. Prover9 and Mace4, 2005-2010. URL: http://www.cs.unm.edu/~mccune/prover9/.
  20. Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf. Google Scholar
  21. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reasoning, 40(1):35-60, 2008. URL: https://doi.org/10.1007/s10817-007-9085-y.
  22. Lawrence C. Paulson and Jasmin C. Blanchette. Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, Workshop on the Implementation of Logics (IWIL), volume 2 of EPiC, pages 1-11. EasyChair, 2010. Invited talk. URL: http://www.easychair.org/publications/paper/62805.
  23. John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001. URL: https://www.sciencedirect.com/book/9780444508133/handbook-of-automated-reasoning.
  24. Stephan Schulz. System description: E 1.8. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, LPAR, volume 8312 of Lecture Notes in Computer Science, pages 735-743. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_49.
  25. Stephan Schulz, Simon Cruanes, and Petar Vukmirovic. Faster, higher, stronger: E 2.3. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science, pages 495-507. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29436-6_29.
  26. Josef Urban. BliStr: The Blind Strategymaker. In Georg Gottlob, Geoff Sutcliffe, and Andrei Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, volume 36 of EPiC Series in Computing, pages 312-319. EasyChair, 2015. URL: http://www.easychair.org/publications/paper/BliStr_The_Blind_Strategymaker, URL: https://doi.org/10.29007/8n7m.
  27. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50:229-241, 2013. URL: https://doi.org/10.1007/s10817-012-9269-y.
  28. Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. In CADE, volume 12699 of Lecture Notes in Computer Science, pages 415-432. Springer, 2021. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact