A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo

Guillaume Burel 1, 2, *
* Auteur correspondant
2 CPR
CEDRIC - Centre d'Etude et De Recherche en Informatique du Cnam
Abstract : The λΠ-calculus modulo is a proof language that has been proposed as a proof standard for (re-)checking and interoperability. Resolution and superposition are proof-search methods that are used in state-of-the-art first-order automated theorem provers. We provide a shallow embedding of resolution and superposition proofs in the λΠ-calculus modulo, thus offering a way to check these proofs in a trusted setting, and to combine them with other proofs. We implement this embedding as a back-end of the prover iProver Modulo.
Type de document :
Communication dans un congrès
Jasmin Christian Blanchette and Josef Urban. PxTP - Third International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. EasyChair, 14, pp.43-57, 2013, PxTP 2013. 〈http://www.easychair.org/publications/?page=90156058〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00921513
Contributeur : Guillaume Burel <>
Soumis le : vendredi 20 décembre 2013 - 15:10:49
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : vendredi 21 mars 2014 - 12:10:49

Fichier

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

Identifiants

  • HAL Id : hal-00921513, version 1

Collections

Citation

Guillaume Burel. A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. Jasmin Christian Blanchette and Josef Urban. PxTP - Third International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. EasyChair, 14, pp.43-57, 2013, PxTP 2013. 〈http://www.easychair.org/publications/?page=90156058〉. 〈hal-00921513〉

Partager

Métriques

Consultations de la notice

305

Téléchargements de fichiers

232