Proof Reconstruction for Z3 in Isabelle/HOL

Sascha Böhme

Document: PDF slides

Abstract: Currently, only a few Satisfiability Modulo Theories (SMT) solvers are able to produce proof objects, although there is a strong incentive: Proof objects can be reconstructed in a different system to the check soundness of an SMT solver. We present proof reconstruction for the SMT solver Z3 in Isabelle/HOL and give experimental results of its application.

SMT binding to Isabelle/HOL: See the Isabelle distribution.

Bibtex entry:

@inproceedings{
  author    = {Sascha B{\"o}hme},
  title     = {Proof Reconstruction for {Z3} in {Isabelle/HOL}},
  booktitle = {7th International Workshop on
               Satisfiability Modulo Theories (SMT '09)},
  year      = 2009
}