Extended Resolution as Certificates for Propositional Logic

Chantal Keller 1, 2
1 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : When checking answers coming from automatic provers, or when skeptically integrating them into proof assistants, a major problem is the wide variety of formats of certificates, which forces to write lots of different checkers. In this paper, we propose to use the extended resolution as a common format for every propositional prover. To be able to do this, we detail two algorithms transforming proofs computed respectively by tableaux provers and provers based on BDDs into this format. Since this latter is already implemented for SAT solvers, it is now possible for the three most common propositional provers to share the same certificates.
Type de document :
Communication dans un congrès
Blanchette, Jasmin Christian and Josef Urban. PxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. 2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00836845
Contributeur : Chantal Keller <>
Soumis le : vendredi 21 juin 2013 - 15:38:23
Dernière modification le : jeudi 10 mai 2018 - 02:06:56
Document(s) archivé(s) le : mercredi 5 avril 2017 - 01:40:19

Fichier

keller-pxtp13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00836845, version 1

Collections

Citation

Chantal Keller. Extended Resolution as Certificates for Propositional Logic. Blanchette, Jasmin Christian and Josef Urban. PxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. 2013. 〈hal-00836845〉

Partager

Métriques

Consultations de la notice

422

Téléchargements de fichiers

213