Hammering towards QED

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.
Type de document :
Article dans une revue
Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (1), pp.101-148
Liste complète des métadonnées

Littérature citée [135 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01386988
Contributeur : Jasmin Christian Blanchette <>
Soumis le : lundi 24 octobre 2016 - 23:51:47
Dernière modification le : mercredi 30 novembre 2016 - 17:51:09

Fichier

h4qed-clean.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01386988, version 1

Collections

Citation

Jasmin Blanchette, Cezary Kaliszyk, Lawrence Paulson, Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (1), pp.101-148. 〈hal-01386988〉

Partager

Métriques

Consultations de
la notice

79

Téléchargements du document

103