| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 423330 | Electronic Notes in Theoretical Computer Science | 2006 | 12 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
