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.

• Type: Conference
• Year: 2010
• Where: ITP
• Authors: Sascha Böhme, Tjark Weber
• Keywords: ITP 2010, LCF-style Proof, LCF-style Proof Reconstruction, Mathematics, Theorem Provers Isabelle/hol