Proof Outlines as Proof Certificates: A System Description

Roberto Blanco 1, 2, 3 Dale Miller 1, 2, 3
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We apply the foundational proof certificate (FPC) framework to the problem of designing high-level outlines of proofs. The FPC framework provides a means to formally define and check a wide range of proof evidence. A focused proof system is central to this framework and such a proof system provides an interesting approach to proof reconstruction during the process of proof checking (relying on an underlying logic programming implementation). Here, we illustrate how the FPC framework can be used to design proof outlines and then to exploit proof checkers as a means for expanding outlines into fully detailed proofs. In order to validate this approach to proof outlines, we have built the ACheck system that allows us to take a sequence of theorems and apply the proof outline " do the obvious induction and close the proof using previously proved lemmas " .
Type de document :
Communication dans un congrès
First International Workshop on Focusing, Nov 2015, Suva, Fiji. 〈http://www.qatar.cmu.edu/iliano/svc/conf/wof15/〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01238436
Contributeur : Roberto Blanco <>
Soumis le : vendredi 4 décembre 2015 - 20:51:17
Dernière modification le : jeudi 10 mai 2018 - 02:06:51
Document(s) archivé(s) le : samedi 29 avril 2017 - 04:44:18

Fichier

wof.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01238436, version 1

Citation

Roberto Blanco, Dale Miller. Proof Outlines as Proof Certificates: A System Description. First International Workshop on Focusing, Nov 2015, Suva, Fiji. 〈http://www.qatar.cmu.edu/iliano/svc/conf/wof15/〉. 〈hal-01238436〉

Partager

Métriques

Consultations de la notice

322

Téléchargements de fichiers

51