Proof certificates in PVS

Frédéric Gilbert 1, 2
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : The purpose of this work is to allow the proof system PVS to export proof certificates that can be checked externally. This is done through the instrumentation of PVS to record detailed proofs step by step during the proof search process. At the current stage of this work, proofs can be built for any PVS theory. However, some reasoning steps rely on unverified assumptions. For a restricted fragment of PVS, the proofs are exported to the universal proof checker Dedukti, and the un-verified assumptions are proved externally using the automated theorem prover MetiTarski.
Type de document :
Communication dans un congrès
ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. Springer, LNCS, 10499, pp.262-268, 2017, ITP 2017: Interactive Theorem Proving. 〈http://itp2017.cic.unb.br/〉. 〈10.1007/978-3-319-66107-0_17〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01673517
Contributeur : Frédéric Gilbert <>
Soumis le : samedi 30 décembre 2017 - 11:48:17
Dernière modification le : lundi 24 septembre 2018 - 11:34:02

Fichier

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

Identifiants

Citation

Frédéric Gilbert. Proof certificates in PVS. ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. Springer, LNCS, 10499, pp.262-268, 2017, ITP 2017: Interactive Theorem Proving. 〈http://itp2017.cic.unb.br/〉. 〈10.1007/978-3-319-66107-0_17〉. 〈hal-01673517〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

37