Fast LCF-Style Proof Reconstruction for Z3
Abstract: The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs of unsatisfiability. We present independent reconstruction of these proofs in the theorem provers Isabelle/HOL and HOL4 with particular focus on efficiency. Our highly optimized implementations outperform previous LCF-style proof checkers for SMT, often by orders of magnitude. Detailed performance data shows that LCF-style proof reconstruction can be faster than proof search in Z3.
Data: logs.tar.gz (54 KB)
Bibtex entry:
@inproceedings{ author = {B{\"o}hme, Sascha and Weber, Tjark}, title = {Fast {LCF}-Style Proof Reconstruction for {Z3}}, booktitle = {Interactive Theorem Proving}, editor = {Kaufmann, Matt and Paulson, Lawrence}, series = {Lecture Notes in Computer Science}, volume = 6172, year = 2010, pages = {179--194}, publisher = {Springer}, doi = {http://dx.doi.org/10.1007/978-3-642-14052-5_14} }