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 @p_6) :rule and :premises (a0) :args (1))
(step t9 (cl (= @p_13 (! (and d d) :named @p_15))) :rule cong :premises (t8))
(step t10 (cl (= @p_14 (! (not @p_15) :named @p_16))) :rule cong :premises (t9))
(step t11 (cl (! (= @p_15 d) :named @p_17)) :rule hole :args ("TRUST_THEORY_REWRITE" @p_17 1 6))
(step t12 (cl (= @p_16 @p_9)) :rule cong :premises (t11))
(step t13 (cl (= @p_14 @p_9)) :rule trans :premises (t10 t12))
(step t14 (cl @p_12) :rule trans :premises (t7 t13))
(step t15 (cl @p_5) :rule and :premises (a0) :args (2))
(step t16 (cl @p_9) :rule resolution :premises (t5 t14 t15))
(step t17 (cl @p_7) :rule and :premises (a0) :args (0))
(step t18 (cl d b) :rule or :premises (t17))
(step t19 (cl b d) :rule reordering :premises (t18))
(step t20 (cl b) :rule resolution :premises (t19 t16))
(step t21 (cl @p_11) :rule resolution :premises (t4 t16 t20))
(step t22 (cl @p_2 @p_10) :rule or_neg :args (0))
(step t23 (cl @p_2 @p_9) :rule or_neg :args (1))
(step t24 (cl @p_2 @p_2) :rule resolution :premises (t19 t22 t23))
(step t25 (cl @p_2) :rule contraction :premises (t24))
(step t26 (cl) :rule resolution :premises (t2 t21 t25))
)