Extended Resolution as Certificates for Propositional Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Extended Resolution as Certificates for Propositional Logic

Résumé

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.
Fichier principal
Vignette du fichier
keller-pxtp13.pdf (330.99 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00836845 , version 1 (21-06-2013)

Identifiants

  • HAL Id : hal-00836845 , version 1

Citer

Chantal Keller. Extended Resolution as Certificates for Propositional Logic. PxTP - 3rd International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. ⟨hal-00836845⟩
243 Consultations
305 Téléchargements

Partager

Gmail Facebook X LinkedIn More