Proving Theorems of Higher-Order Logic with SMT Solvers

Abstract: Following the demand for increased proof automation in the interactive theorem prover Isabelle, this thesis describes how satisfiability modulo theories (SMT) solvers improve on the state of the art. SMT solvers are automatic theorem provers with decision procedures for several theories such as equality and linear arithmetic.
Our main contributions are a sound translation from Isabelle's higher-order logic to the first-order logic of SMT solvers, and efficient checking of proofs found by the solver Z3.
Based on a large evaluation, we find that many theorems can now be proved automatically and almost instantaneously for which time-consuming user ingenuity was previously required. Checking Z3's proofs is fast thanks to our extensive optimizations.
Further contributions are a new tool and methodology to verify the functional correctness of C code in conjunction with the automatic program verifier VCC. We demonstrate their suitability on real-world implementations of tree and graph algorithms.

Bibtex entry:

@phdthesis{
  author = {Sascha B\"ohme},
  title = {Proving Theorems of Higher-Order Logic with SMT Solvers},
  school = {Technische Universit\"at M\"unchen},
  year = 2012
}