Hammering towards QED

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Hammering towards QED

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Hammering towards QED

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

JOURNAL OF FORMALIZED REASONING

ISSN

1972-5787

e-ISSN

1972-5787

Svazek periodika

9

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

IT - Italská republika

Počet stran výsledku

48

Strana od-do

101-148

Kód UT WoS článku

000371983900006

EID výsledku v databázi Scopus

—