Hammering towards QED
Paper · 2016 · Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson et al.
Summary
This survey covers "hammers," tools that let users of proof assistants prove hard lemmas automatically. The user does not have to script the proof search by hand. The tools draw on very large formal libraries, and the name comes from Sledgehammer for Isabelle and HOLyHammer for HOL Light.
The authors break a typical hammer into three stages:
- Premise selection picks the library facts likely to help with the current goal, using syntactic, semantic or learned heuristics.
- Translation recasts the proof assistant's rich logic into the simpler, usually first-order logic of automatic theorem provers (ATPs).
- Proof reconstruction replays the external proof so the proof assistant can certify it.
The paper also traces the history of ATP/ITP integration and reviews published benchmark results. It links the technology to the 1993 QED Manifesto. The authors argue that strong automated reasoning and AI are likely essential for QED-style projects, and that formal libraries are valuable material for building such AI. Good translations into an efficiently automated logic matter in practice whichever foundational framework is chosen.
Key points
- Hammers prove roughly 40% of top-level lemmas in the Mizar and Flyspeck libraries and about 70% of goals in the Isabelle Judgment Day benchmark. Some of these libraries hold more than 100,000 top-level facts.
- Hales credits automated procedures with 40% of Mizar theorems and 47% of HOL Light/Flyspeck, with similar rates in Isabelle.
- The pipeline has three modules: premise selector, translation module and proof reconstruction module. Not every system includes all three.
- Related systems include MaLARea, the Mizar Proof Advisor and Why3. Further ATP/SMT links exist for HOL Light, HOL4, Coq, ACL2 and PVS.
- Since 2008 the Large Theory Batch category of CASC has benchmarked ATPs on large problems taken from Mizar, Isabelle, HOL Light, SUMO and Cyc.
Institutions
United Kingdom243 works · 121,396 citations🎓Universität InnsbruckInnsbruck · 
Austria8 works · 737 citations🏢Cambridge University PressCambridge · United Kingdom5 works · 355 citations🎓Czech Technical University in PraguePrague · 
Czechia3 works · 402 citationsFields, topics and concepts
📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksComputational Theory and Mathematics · 252 works
🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,426 works
💡 Concepts 1Key ideas and methods explained on our concept pages.Lemma · 24 works
Cite
Cite as Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson and Josef Urban. 2016. Hammering towards QED. Journal of Formalized Reasoning 9(1).
@article{blanchette2016hammering,
title = {{Hammering towards QED}},
author = {Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson and Josef Urban},
journal = {Journal of Formalized Reasoning 9(1)},
year = {2016},
doi = {10.6092/issn.1972-5787/4593},
url = {https://doi.org/10.6092/issn.1972-5787/4593}
}References
- The QED Manifesto. In Bundy [36], pages 238251. find
- Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, and Peter H. Schmitt. Integrating automated Automated DeductionA Basis for Applications and interactive theorem proving. In Wolfgang Bibel and Peter H. Schmitt, editors, , volume II: Systems and Im… find
- Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. find
Updated
This page in Markdown → https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/