Proof format: Alethe ¶

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 , dag-thresh=0 , proof-granularity=theory-rewrite . These requirements are due to not yet supporting printing proofs with term sharing and 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 --dag-thresh=0 --proof-granularity=theory-rewrite ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
unsat
(assume a0 (and (or d b) (= c d) (not (ite d c false)) (= (or b d) (= b d))))
(step t1 (cl (not (= (and (or d b) (= c d) (not (ite d c false)) (= (or b d) (= b d))) (and (or d b) (= c d) (not (and d c)) (= (or b d) (= b d))))) (not (and (or d b) (= c d) (not (ite d c false)) (= (or b d) (= b d)))) (and (or d b) (= c d) (not (and d c)) (= (or b d) (= b d)))) :rule equiv_pos2)
(step t2 (cl (= (or d b) (or d b))) :rule refl)
(step t3 (cl (= (= c d) (= c d))) :rule refl)
(step t4 (cl (= (ite d c false) (and d c))) :rule all_simplify)
(step t5 (cl (= (not (ite d c false)) (not (and d c)))) :rule cong :premises (t4))
(step t6 (cl (= (= (or b d) (= b d)) (= (or b d) (= b d)))) :rule refl)
(step t7 (cl (= (and (or d b) (= c d) (not (ite d c false)) (= (or b d) (= b d))) (and (or d b) (= c d) (not (and d c)) (= (or b d) (= b d))))) :rule cong :premises (t2 t3 t5 t6))
(step t8 (cl (and (or d b) (= c d) (not (and d c)) (= (or b d) (= b d)))) :rule resolution :premises (t1 t7 a0))
(step t9 (cl (not (and d c))) :rule and :premises (t8))
(step t10 (cl (not d) (not c)) :rule not_and :premises (t9))
(step t11 (cl (= c d)) :rule and :premises (t8))
(step t12 (cl c (not d)) :rule equiv2 :premises (t11))
(step t13 (cl (= (or b d) (= b d))) :rule and :premises (t8))
(step t14 (cl (not (or b d)) (= b d)) :rule equiv1 :premises (t13))
(step t15 (cl (= b d) (not (or b d))) :rule reordering :premises (t14))
(step t16 (cl (not (= b d)) (not b) d) :rule equiv_pos2)
(step t17 (cl d (not b) (not (= b d))) :rule reordering :premises (t16))
(step t18 (cl (or b d) (not b)) :rule or_neg)
(step t19 (cl d (not b) (not b)) :rule resolution :premises (t15 t17 t18))
(step t20 (cl d (not b)) :rule contraction :premises (t19))
(step t21 (cl (or d b)) :rule and :premises (t8))
(step t22 (cl d b) :rule or :premises (t21))
(step t23 (cl b d) :rule reordering :premises (t22))
(step t24 (cl d d) :rule resolution :premises (t20 t23))
(step t25 (cl d) :rule contraction :premises (t24))
(step t26 (cl c) :rule resolution :premises (t12 t25))
(step t27 (cl d (not b) (not b)) :rule resolution :premises (t15 t17 t18))
(step t28 (cl d (not b)) :rule contraction :premises (t27))
(step t29 (cl d d) :rule resolution :premises (t28 t23))
(step t30 (cl d) :rule contraction :premises (t29))
(step t31 (cl) :rule resolution :premises (t10 t26 t30))

          