Hammering towards QED
View / Open Files
Publication Date
2016-02-03Journal Title
Journal of Formalized Reasoning
Publisher
Alma Mater Studiorum - University of Bologna
Volume
9
Pages
101-148
Language
English
Type
Article
Metadata
Show full item recordCitation
Blanchette, J. C., Kaliszyk, C., Paulson, L., & Urban, J. (2016). Hammering towards QED. Journal of Formalized Reasoning, 9 101-148. http://jfr.unibo.it/article/view/4593
Abstract
This paper surveys the emerging methods to automate reasoning over large libraries developed with formal proof assistants. We call these methods hammers. They give the authors of formal proofs a strong “one-stroke” tool for discharging difficult lemmas without the need for careful and detailed manual programming of proof search. The main ingredients underlying this approach are efficient automatic theorem provers that can cope with hundreds of axioms, suitable translations of the proof assistant’s logic to the logic of the automatic provers, heuristic and learning methods that select relevant facts from large libraries, and methods that reconstruct the automatically found proofs inside the proof assistants. We outline the history of these methods, explain the main issues and techniques, and show their strength on several large benchmarks. We also discuss the relation of this technology to the QED Manifesto and consider its implications for QED-like efforts.
Sponsorship
Blanchette’s Sledgehammer research was supported by the Deutsche Forschungs-
gemeinschaft projects Quis Custodiet (grants NI 491/11-1 and NI 491/11-2) and
Hardening the Hammer (grant NI 491/14-1). Kaliszyk is supported by the Austrian
Science Fund (FWF) grant P26201. Sledgehammer was originally supported by the
UK’s Engineering and Physical Sciences Research Council (grant GR/S57198/01).
Urban’s work was supported by the Marie-Curie Outgoing International Fellowship
project AUTOKNOMATH (grant MOIF-CT-2005-21875) and by the Netherlands
Organisation for Scientific Research (NWO) project Knowledge-based Automated
Reasoning (grant 612.001.208).
Embargo Lift Date
2050-01-01
Identifiers
External link: http://jfr.unibo.it/article/view/4593
This record's URL: https://www.repository.cam.ac.uk/handle/1810/248884
Rights
Attribution 2.0 UK: England & Wales
Licence URL: http://creativecommons.org/licenses/by/2.0/uk/
Recommended or similar items
The following licence files are associated with this item: