Falsification of HOL Formulas by means of SAT Solvers
From PUMA Graduiertenkolleg
Theorem proving - interactive or automatic - teaches us that most of the time one is trying to prove a non-theorem, i.e. and incorrect proposition. To detect such situations automatically, the theorem prover Isabelle can search for (finite) counterexamples by translating formulae in HOL (higher-order logic) to propositional logic and asking a fast external SAT solver for a satisfying assignment. Now it turns out that despite the amazing performance of modern SAT solvers, the feasibility of this approach depends crucially on an intelligent translation from HOL to SAT. The focus of this project is to develop and implement application-specific translation schemes adapted to the various specification constructs in HOL. Two applications we intend to focus on are state transition systems (where techniques from bounded model checking should be made available in HOL) and programming language semantics.