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 , 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 45)
(assume a1 false)
(assume a2 (cl))
(step t0 (cl (not (! (= (! (not (! (ite d c false) :named @p_5)) :named @p_6) (! (not (! (and d c) :named @p_12)) :named @p_13)) :named @p_14)) (not @p_6) @p_13) :rule equiv_pos2)
(step t1 (cl (= @p_5 @p_12)) :rule all_simplify)
(step t2 (cl @p_14) :rule cong :premises (t1))
(step t3 (and (! (or d b) :named @p_1) (! (= c d) :named @p_7) @p_6 (! (= (! (or b d) :named @p_3) (! (= b d) :named @p_2)) :named @p_4)) :rule assume)
(step t4 (cl @p_6) :rule and :premises (t3))
(step t5 (cl @p_13) :rule resolution :premises (t0 t2 t4))
(step t6 (cl (! (not d) :named @p_11) (not c)) :rule not_and :premises (t5))