EasyChair Publications
Search
Paper Information
Paper:Chantal Keller
Extended Resolution as Certificates for Propositional Logic
Title:Extended Resolution as Certificates for Propositional Logic
Authors:Chantal Keller
Keyphrases:certificates, analytic tableaux, tableaux, binary decision diagrams, extended resolution
Paper:
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 {\bdd}s 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.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:96-109
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:13
Downloads:8
BibTeX entry:
@inproceedings{PxTP2013:Extended_Resolution_as_Certificates_for_Propositional_Logic,
  author    = {Chantal Keller},
  title     = {Extended Resolution as Certificates for Propositional Logic},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {96-109},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}