Translating Between Implicit and Explicit Versions of Proof

Roberto Blanco 1 Zakaria Chihani 2 Dale Miller 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
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : The Foundational Proof Certificate (FPC) framework can be used to define the semantics of a wide range of proof evidence. For example , such definitions exist for a number of textbook proof systems as well as for the proof evidence output from some existing theorem proving systems. An important decision in designing a proof certificate format is the choice of how many details are to be placed within certificates. Formats with fewer details are smaller and easier for theorem provers to output but they require more sophistication from checkers since checking will involve some proof reconstruction. Conversely, certificate formats containing many details are larger but are checkable by less sophisticated checkers. Since the FPC framework is based on well-established proof theory principles, proof certificates can be manipulated in meaningful ways. In this paper, we illustrate how it is possible to automate moving from implicit to explicit (elaboration) and from explicit to implicit (distillation) proof evidence via the proof checking of a pair of proof certificates. Performing elaboration makes it possible to transform a proof certificate with details missing into a certificate packed with enough details so that a simple kernel (without support for proof reconstruction) can check the elaborated certificate. We illustrate how trust in only a single, simple checker of explicitly described proofs can be used to provide trust in a range of theorem provers employing a range of proof structures.
Type de document :
Communication dans un congrès
CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01645016
Contributeur : Dale Miller <>
Soumis le : mercredi 22 novembre 2017 - 17:46:57
Dernière modification le : jeudi 10 mai 2018 - 02:06:32

Fichier

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

Identifiants

  • HAL Id : hal-01645016, version 1

Citation

Roberto Blanco, Zakaria Chihani, Dale Miller. Translating Between Implicit and Explicit Versions of Proof. CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. 〈hal-01645016〉

Partager

Métriques

Consultations de la notice

206

Téléchargements de fichiers

31