Tjark Weber. In Alessandro Armando and Alessandro Cimatti, editors, Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005), volume 144(2) of Electronic Notes in Theoretical Computer Science, pages 67-78. Elsevier, January 2006.
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.
@inproceedings{weber06integrating,
author = {Tjark Weber},
title = {Integrating a {SAT} Solver with an {LCF}-style Theorem Prover},
editor = {Alessandro Armando and Alessandro Cimatti},
booktitle = {Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005)},
volume = {144(2)},
series = {Electronic Notes in Theoretical Computer Science},
pages = {67--78},
publisher = {Elsevier},
month = jan,
year = {2006},
url = {http://dx.doi.org/10.1016/j.entcs.2005.12.007}
}
A revised version of this paper is available.