Using a SAT Solver as a Fast Decision Procedure for Propositional Logic in an LCF-style Theorem Prover

Tjark Weber. In Joe Hurd, Edward Smith, and Ashish Darbari, editors, Theorem Proving in Higher Order Logics - 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005, Emerging Trends Proceedings, pages 180-189, Oxford, UK, August 2005. Oxford University Computing Laboratory, Programming Research Group. Research Report PRG-RR-05-02.

Abstract

This paper describes the integration of a leading SAT solver with Isabelle/HOL, a popular interactive theorem prover. The SAT solver generates resolution-style proofs for (instances of) propositional tautologies. These proofs are verified by the theorem prover. The presented approach significantly improves Isabelle's performance on propositional problems, and furthermore exhibits counterexamples for unprovable conjectures.

Download

• PDF (107 kB)

BibTeX

@inproceedings{weber05using,
  author    = {Tjark Weber},
  title     = {Using a {SAT} Solver as a Fast Decision Procedure for Propositional Logic in an {LCF}-style Theorem Prover},
  editor    = {Joe Hurd and Edward Smith and Ashish Darbari},
  booktitle = {Theorem Proving in Higher Order Logics~-- 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005, Emerging Trends Proceedings},
  pages     = {180--189},
  address   = {Oxford, UK},
  publisher = {Oxford University Computing Laboratory, Programming Research Group},
  note      = {Research Report PRG-RR-05-02},
  month     = aug,
  year      = {2005}
}

Note

A revised version of this paper is available.