Fast LCF-Style Proof Reconstruction for Z3

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.

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.

Download

The original publication is available at www.springerlink.com.

BibTeX

@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}
}

Benchmarks

Detailed logs and profiling data are available here (53 kB).


Last modified: 2011-12-09