Tjark Weber. In Chris Benzmüller, Bernd Fischer, and Geoff Sutcliffe, editors, Proceedings of the 6th International Workshop on the Implementation of Logics, volume 212 of CEUR Workshop Proceedings, pages 44-62, November 2006.
This paper describes the integration of zChaff and MiniSat, currently two leading SAT solvers, with Isabelle/HOL. Both SAT solvers generate 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 exhibits counterexamples for unprovable conjectures. It is shown that an LCF-style theorem prover can serve as a viable proof checker even for large SAT problems. An efficient representation of the propositional problem in the theorem prover turns out to be crucial; several possible solutions are discussed.
@inproceedings{weber06efficiently,
author = {Tjark Weber},
title = {Efficiently Checking Propositional Resolution Proofs in {Isabelle/HOL}},
editor = {Chris Benzm{\"u}ller and Bernd Fischer and Geoff Sutcliffe},
booktitle = {Proceedings of the 6th International Workshop on the Implementation of Logics},
volume = {212},
series = {CEUR Workshop Proceedings},
pages = {44--62},
month = nov,
year = {2006},
issn = {1613-0073},
url = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-212/05_Weber.pdf}
}
A revised version of this paper is available.