Hammering towards QED
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F16%3A00311250" target="_blank" >RIV/68407700:21730/16:00311250 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.6092/issn.1972-5787/4593" target="_blank" >http://dx.doi.org/10.6092/issn.1972-5787/4593</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.6092/issn.1972-5787/4593" target="_blank" >10.6092/issn.1972-5787/4593</a>
Alternative languages
Result language
angličtina
Original language name
Hammering towards QED
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
R - Projekt Ramcoveho programu EK
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
JOURNAL OF FORMALIZED REASONING
ISSN
1972-5787
e-ISSN
1972-5787
Volume of the periodical
9
Issue of the periodical within the volume
1
Country of publishing house
IT - ITALY
Number of pages
48
Pages from-to
101-148
UT code for WoS article
000371983900006
EID of the result in the Scopus database
—