Designing Proof Formats: A User's Perspective --- Experience Report

Abstract : Automatic provers that can produce proof certificates do not need to be trusted. The certificate can be checked by an independent tool, for example an LCF-style proof assistant such as IsabelleHOL or HOL. Currently, the design of proof formats is mostly dictated by internal constraints of automatic provers and less guided by applications such as checking of certificates. In the worst case, checking can be as involved as the actual proof search simply because important information is missing in the proof certificate. To address this and other issues, we describe design choices for proof formats that we consider both feasible for implementors of automatic provers as well as effective to simplify checking of certificates.
Type de document :
Communication dans un congrès
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00677244
Contributeur : Pascal Fontaine <>
Soumis le : mercredi 7 mars 2012 - 16:02:47
Dernière modification le : mercredi 7 mars 2012 - 16:24:48
Document(s) archivé(s) le : vendredi 23 novembre 2012 - 16:01:27

Fichier

paper4.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00677244, version 1

Collections

Citation

Sascha Böhme, Tjark Weber. Designing Proof Formats: A User's Perspective --- Experience Report. Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011. 〈hal-00677244〉

Partager

Métriques

Consultations de la notice

162

Téléchargements de fichiers

184