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 (= (not (ite d c false)) (not (and d c)))) (not (not (ite d c false))) (not (and d c))) :rule equiv_pos2)
(step t2 (cl (= (ite d c false) (and d c))) :rule all_simplify)
(step t3 (cl (= (not (ite d c false)) (not (and d c)))) :rule cong :premises (t2))
(step t4 (cl (not (ite d c false))) :rule and :premises (a0))
(step t5 (cl (not (and d c))) :rule resolution :premises (t1 t3 t4))
(step t6 (cl (not d) (not c)) :rule not_and :premises (t5))
(step t7 (cl (= c d)) :rule and :premises (a0))
(step t8 (cl c (not d)) :rule equiv2 :premises (t7))
(step t9 (cl (= (or b d) (= b d))) :rule and :premises (a0))
(step t10 (cl (not (or b d)) (= b d)) :rule equiv1 :premises (t9))
(step t11 (cl (= b d) (not (or b d))) :rule reordering :premises (t10))
(step t12 (cl (not (= b d)) (not b) d) :rule equiv_pos2)
(step t13 (cl d (not b) (not (= b d))) :rule reordering :premises (t12))
(step t14 (cl (or b d) (not b)) :rule or_neg)
(step t15 (cl d (not b) (not b)) :rule resolution :premises (t11 t13 t14))
(step t16 (cl d (not b)) :rule contraction :premises (t15))
(step t17 (cl (or d b)) :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))

          