Proof format: Alethe

Using the flag proof-format-mode=alethe, cvc5 outputs proofs in the Alethe proof format.

The Alethe proof format is a flexible proof format for SMT solvers based on SMT-LIB. It includes both coarse- and fine-grained steps and was first implemented in the veriT solver [BdODeharbeF09]. Alethe proofs can be checked via reconstruction within Isabelle/HOL [BBFF20, SFD21] as well as within Coq, the latter via the SMTCoq plugin [AFGregoire+11, EMT+17]. There is also a high performance Rust proof checker and elaborator for Alethe: Carcara, available here. For a quick start, the cvc5 repository contains a script to download and install the Carcara checker’s version with full support for cvc5 Alethe proofs, and create scripts for generating proofs with cvc5 and checking them with Carcara.

Currently, the theories of equality with uninterpreted functions, linear arithmetic, bit-vectors and parts of the theory of strings (with or without quantifiers) are supported in cvc5’s Alethe proofs.

A simple example of cvc5 producing a proof in the Alethe proof format:

$ bin/cvc5 --dump-proofs --proof-format-mode=alethe ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
unsat
(assume a0 (! (and (! (or d b) :named @p_7) (! (= c d) :named @p_6) (! (not (! (ite d c false) :named @p_4)) :named @p_5) (! (= (! (or b d) :named @p_2) (! (= b d) :named @p_1)) :named @p_3)) :named @p_8))
(step t0 (cl @p_3) :rule and :premises (a0) :args (3))
(step t1 (cl (! (not @p_2) :named @p_19) @p_1) :rule equiv1 :premises (t0))
(step t2 (cl @p_1 @p_19) :rule reordering :premises (t1))
(step t3 (cl (! (not @p_1) :named @p_11) (! (not b) :named @p_10) d) :rule equiv_pos2)
(step t4 (cl d @p_10 @p_11) :rule reordering :premises (t3))
(step t5 (cl (not (! (= @p_5 (! (not d) :named @p_9)) :named @p_12)) (not @p_5) @p_9) :rule equiv_pos2)
(step t6 (cl (! (= @p_4 (! (and d c) :named @p_13)) :named @p_18)) :rule hole :args ("TRUST_THEORY_REWRITE" @p_18 1 6))
(step t7 (cl (= @p_5 (! (not @p_13) :named @p_14))) :rule cong :premises (t6))
(step t8 (cl (= d d)) :rule refl)
(step t9 (cl @p_6) :rule and :premises (a0) :args (1))
(step t10 (cl (= @p_13 (! (and d d) :named @p_15))) :rule cong :premises (t8 t9))
(step t11 (cl (= @p_14 (! (not @p_15) :named @p_16))) :rule cong :premises (t10))
(step t12 (cl (! (= @p_15 d) :named @p_17)) :rule hole :args ("TRUST_THEORY_REWRITE" @p_17 1 6))
(step t13 (cl (= @p_16 @p_9)) :rule cong :premises (t12))
(step t14 (cl (= @p_14 @p_9)) :rule trans :premises (t11 t13))
(step t15 (cl @p_12) :rule trans :premises (t7 t14))
(step t16 (cl @p_5) :rule and :premises (a0) :args (2))
(step t17 (cl @p_9) :rule resolution :premises (t5 t15 t16))
(step t18 (cl @p_7) :rule and :premises (a0) :args (0))
(step t19 (cl d b) :rule or :premises (t18))
(step t20 (cl b d) :rule reordering :premises (t19))
(step t21 (cl b) :rule resolution :premises (t20 t17))
(step t22 (cl @p_11) :rule resolution :premises (t4 t17 t21))
(step t23 (cl @p_2 @p_10) :rule or_neg :args (0))
(step t24 (cl @p_2 @p_9) :rule or_neg :args (1))
(step t25 (cl @p_2 @p_2) :rule resolution :premises (t20 t23 t24))
(step t26 (cl @p_2) :rule contraction :premises (t25))
(step t27 (cl) :rule resolution :premises (t2 t22 t26))