Fast LCF-Style Proof Reconstruction for Z3

Sascha Böhme and Tjark Weber

Document: DOI PDF

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