Proof format: Cooperating Proof Calculus

Using option proof-format-mode=cpc, cvc5 outputs proofs in the Cooperating Proof Calculus proof format.

This calculus was designed to faithfully represent cvc5’s internal reasoning. As a disclaimer, this means that it treats certain operators differently from the SMT-LIB standard. As an example, cvc5 uses mixed arithmetic internally, where integers and reals can appear together. A comprehensive list of these differences can be found in the Eunoia definition of CPC, as described below.

Ethos is an efficient proof checker written in C++ which can check proofs in the CPC format. For a quick start, the cvc5 repository contains a script to download and install the Ethos checker, and create scripts for generating proofs with cvc5 and checking them with the Ethos proof checker.

The Ethos checker is based on the logical framework Eunoia. The Cooperating Proof Calculus has been formalized in a Eunoia signature, which is contained within the cvc5 repository in this file. Based on this signature, Ethos can check CPC proofs over all theories that are formalized in this signature. For more details on Eunoia and a comprehensive overview of the language supported by the Ethos checker, see the user manual here.

Note that several proof rules in the Cooperating Proof Calculus are not yet supported in Eunoia signatures. Steps that use such rules are printed as trust steps in the proof. A trust step proves an arbitrary formula with no provided justification. The resulting proof contains warnings for trust steps that indicate which internal proof rules were recorded as trust steps in the proof.

Upon successful exit, ethos will return the output incomplete if any trust step is used in the proof, indicating that the reasoning in the proof was incomplete. Otherwise, if all proof steps are fully specified, ethos will return the output correct. All proofs in the cpc format are closed refutations of the input, in that the proof will assume formulas from the input and end with a step proving false.

For more fine-grained proofs, the additional option proof-granularity=dsl-rewrite can be passed to cvc5. This will result in proofs with more detail.

A simple example of cvc5 producing a proof in CPC proof format is shown below. Notice that the concrete syntax of CPC is very similar to the Alethe format. However, the proof rules used by these two formats are different.

$ bin/cvc5 --dump-proofs --proof-format-mode=cpc --proof-granularity=dsl-rewrite ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
unsat
(declare-const c Bool)
(declare-const b Bool)
(declare-const d Bool)
(define @t1 () (= b d))
(define @t2 () (or b d))
(define @t3 () (@list true false))
(assume @p1 (and (or d b) (= c d) (not (ite d c false)) (= @t2 @t1)))
(step @p2 :rule and_elim :premises (@p1) :args (0))
(step @p3 :rule reordering :premises (@p2) :args (@t2))
(step @p4 :rule aci_norm :args ((= (and d d) d)))
(step @p5 :rule cong :premises (@p4) :args (not))
(step @p6 :rule and_elim :premises (@p1) :args (1))
(step @p7 :rule refl :args (d))
(step @p8 :rule nary_cong :premises (@p7 @p6) :args (and))
(step @p9 :rule cong :premises (@p8) :args (not))
(step @p10 :rule trans :premises (@p9 @p5))
(step @p11 :rule ite-else-false :args (d c))
(step @p12 :rule cong :premises (@p11) :args (not))
(step @p13 :rule trans :premises (@p12 @p10))
(step @p14 :rule and_elim :premises (@p1) :args (2))
(step @p15 :rule eq_resolve :premises (@p14 @p13))
(step @p16 :rule chain_resolution :premises (@p3 @p15) :args ((@list true) (@list d)))
(step @p17 :rule cnf_equiv_pos1 :args (@t1))
(step @p18 :rule reordering :premises (@p17) :args ((or d (not b) (not @t1))))
(step @p19 :rule chain_resolution :premises (@p18 @p15 @p16) :args (@t3 (@list d b)))
(step @p20 :rule and_elim :premises (@p1) :args (3))
(step @p21 :rule equiv_elim1 :premises (@p20))
(step @p22 :rule reordering :premises (@p21) :args ((or @t1 (not @t2))))
(step @p23 false :rule chain_resolution :premises (@p22 @p19 @p3) :args (@t3 (@list @t1 @t2)))