Document Open Access Logo

Sledgehammering Without ATPs (Short Paper)

Authors Martin Desharnais , Jasmin Blanchette

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.38.pdf
  • Filesize: 0.61 MB
  • 8 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.38.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
  • Computing methodologies → Theorem proving algorithms
Keywords
  • Interactive theorem proving
  • proof assistants
  • proof automation

Metrics

Abstract

We describe an alternative architecture for "hammers," inspired by Magnushammer, in which proofs are found by the proof assistant’s built-in automation instead of by external automatic theorem provers (ATPs). We implemented this approach in Isabelle’s Sledgehammer and evaluated it. The new ATP-free approach nicely complements the traditional Sledgehammer. The two approaches in combination solve more goals than the traditional ATP-based approach alone.

Cite As Get BibTex

Martin Desharnais and Jasmin Blanchette. Sledgehammering Without ATPs (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.38

Author Details

Martin Desharnais
  • Ludwig-Maximilians-Universität München, Germany
Jasmin Blanchette
  • Ludwig-Maximilians-Universität München, Germany

Funding

Co-funded by the European Union (ERC, Nekoka, 101083038). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

Acknowledgements

We thank Benedikt Pilger, whose preliminary experiments motivated us to investigate an ATP-free hammer further. We also thank Mark Summerfield and the anonymous reviewers for suggesting textual improvements.

Supplementary Materials

References

  1. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, TACAS 2022, Part I, volume 13243 of LNCS, pages 415-442. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  2. Ahmed Bhayat and Martin Suda. A higher-order Vampire (short paper). In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, IJCAR 2024, Part I, volume 14739 of LNCS, pages 75-85. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_5.
  3. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning, 51(1):109-128, 2013. URL: https://doi.org/10.1007/s10817-013-9278-5.
  4. Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. Automatic proof and disproof in Isabelle/HOL. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, FroCoS 2011, volume 6989 of LNCS, pages 12-27. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24364-6_2.
  5. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. Journal of Automated Reasoning, 57(3):219-244, 2016. URL: https://doi.org/10.1007/s10817-016-9362-8.
  6. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1):101-148, 2016. URL: https://doi.org/10.6092/issn.1972-5787/4593.
  7. Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach. More SPASS with Isabelle: Superposition with hard sorts and configurable simplification. In Lennart Beringer and Amy Felty, editors, ITP 2012, volume 7406 of LNCS, pages 345-360. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_24.
  8. Thomas Bouton, Diego Caminha Barbosa de Oliveira, David Déharbe, and Pascal Fontaine. veriT: An open, trustable and efficient SMT-solver. In Renate A. Schmidt, editor, CADE-22, volume 5663 of LNCS, pages 151-156. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02959-2_12.
  9. Łukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for dependent type theory. Journal of Automated Reasoning, 61(1-4):423-453, 2018. URL: https://doi.org/10.1007/s10817-018-9458-4.
  10. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, TACAS 2008, volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  11. Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen provers under the hammer. In June Andronick and Leonardo de Moura, editors, ITP 2022, volume 237 of LIPIcs, pages 8:1-8:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.8.
  12. Cezary Kaliszyk and Josef Urban. HOL(y)Hammer: Online ATP service for HOL Light. Mathematics in Computer Science, 9(1):5-22, 2015. URL: https://doi.org/10.1007/s11786-014-0182-0.
  13. Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson. Khovanskii’s theorem. Archive of Formal Proofs, 2022. URL: https://isa-afp.org/entries/Khovanskii_Theorem.html.
  14. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning, 40(1):35-60, 2008. URL: https://doi.org/10.1007/s10817-007-9085-y.
  15. Jia Meng and Lawrence C. Paulson. Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 7(1):41-57, 2009. URL: https://doi.org/10.1016/j.jal.2007.07.004.
  16. Maciej Mikula, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kucinski, Piotr Milos, and Yuhuai Wu. Magnushammer: A transformer-based approach to premise selection. In ICLR 2024. OpenReview.net, 2024. URL: https://openreview.net/forum?id=oYjPk8mqAV.
  17. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  18. Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, IWIL-2010, volume 2 of EPiC, pages 1-11. EasyChair, 2012. URL: https://doi.org/10.29007/36dt.
  19. Alexander Steen and Christoph Benzmüller. The higher-order prover Leo-III. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, IJCAR 2018, volume 10900 of LNCS, pages 108-116. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_8.
  20. Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. In André Platzer and Geoff Sutcliffe, editors, CADE-28, volume 12699 of LNCS, pages 415-432. Springer, 2021. URL: https://doi.org/10.1007/s10817-021-09613-z.
  21. Petar Vukmirović, Jasmin Blanchette, and Stephan Schulz. Extending a high-performance prover to higher-order logic. In Sriram Sankaranarayanan and Natasha Sharygina, editors, TACAS 2023, Part II, volume 13994 of LNCS, pages 111-129. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_10.
  22. Makarius Wenzel. Isabelle/Isar - a generic framework for human-readable proof documents. In Roman Matuszewski and Anna Zalewska, editors, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar, and Rhetoric. University of Białystok, 2007. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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