Skip to Main content Skip to Navigation
Conference papers

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
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-00836845
Contributor : Chantal Keller <>
Submitted on : Friday, June 21, 2013 - 3:38:23 PM
Last modification on : Thursday, March 5, 2020 - 6:24:17 PM
Long-term archiving on: : Wednesday, April 5, 2017 - 1:40:19 AM

File

keller-pxtp13.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00836845, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

566

Files downloads

605