Sascha Böhme and Tjark Weber. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 179-194. Springer, 2010.
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.
The original publication is available at www.springerlink.com.
@inproceedings{boehme10fast,
author = {Sascha B{\"o}hme and Tjark Weber},
title = {Fast {LCF}-Style Proof Reconstruction for {Z3}},
editor = {Matt Kaufmann and Lawrence C. Paulson},
booktitle = {Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July~11-14, 2010. Proceedings},
volume = {6172},
series = {Lecture Notes in Computer Science},
pages = {179--194},
publisher = {Springer},
year = {2010},
url = {http://dx.doi.org/10.1007/978-3-642-14052-5_14}
}
Detailed logs and profiling data are available here (53 kB).