Proof format: Alethe

WARNING: This format is experimental on the main branch of cvc5. To use this format, the option –proof-alethe-experimental must be used, or otherwise an execption is thrown.

Using the flag proof-format-mode=alethe, cvc5 outputs proofs in the Alethe proof format. Additonally, the following additional flags are currently required: simplification=none, and proof-alethe-experimental. The first requirement is due to not yet supporting proofs with non-detailed steps.

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 for Alethe, available here.

Currently, only the theory of equality with uninterpreted functions, parts of the theory of arithmetic and parts of the theory of 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 --simplification=none --proof-alethe-experimental ../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 t1 (cl (not (! (= @p_5 (! (not (! (and d c) :named @p_13)) :named @p_14)) :named @p_15)) (not @p_5) @p_14) :rule equiv_pos2)
(step t2 (cl (= @p_4 @p_13)) :rule all_simplify)
(step t3 (cl @p_15) :rule cong :premises (t2))
(step t4 (cl @p_5) :rule and :premises (a0))
(step t5 (cl @p_14) :rule resolution :premises (t1 t3 t4))
(step t6 (cl (! (not d) :named @p_12) (not c)) :rule not_and :premises (t5))
(step t7 (cl @p_6) :rule and :premises (a0))
(step t8 (cl c @p_12) :rule equiv2 :premises (t7))
(step t9 (cl @p_3) :rule and :premises (a0))
(step t10 (cl (! (not @p_2) :named @p_11) @p_1) :rule equiv1 :premises (t9))
(step t11 (cl @p_1 @p_11) :rule reordering :premises (t10))
(step t12 (cl (! (not @p_1) :named @p_10) (! (not b) :named @p_9) d) :rule equiv_pos2)
(step t13 (cl d @p_9 @p_10) :rule reordering :premises (t12))
(step t14 (cl @p_2 @p_9) :rule or_neg)
(step t15 (cl d @p_9 @p_9) :rule resolution :premises (t11 t13 t14))
(step t16 (cl d @p_9) :rule contraction :premises (t15))
(step t17 (cl @p_7) :rule and :premises (a0))
(step t18 (cl d b) :rule or :premises (t17))
(step t19 (cl b d) :rule reordering :premises (t18))
(step t20 (cl d d) :rule resolution :premises (t16 t19))
(step t21 (cl d) :rule contraction :premises (t20))
(step t22 (cl c) :rule resolution :premises (t8 t21))
(step t23 (cl) :rule resolution :premises (t6 t22 t21))