Proof Reconstruction for Z3 in Isabelle/HOL
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 }