Integrating a SAT Solver with an LCF-style Theorem Prover |
| |
| Authors: | Tjark Weber |
| |
| Affiliation: | Institut für Informatik, Technische Universität München, Boltzmannstr. 3, D-85748 Garching b. München, Germany |
| |
| 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. |
| |
| Keywords: | SAT solver propositional resolution proof checking LCF-style theorem prover |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
