Proof format: AletheLF
Using the flag proof-format-mode=alf , cvc5 outputs proofs in the AletheLF (ALF) proof format.
The ALF proof format is based on the SMT-LIB 3 language. An efficient C++ proof checker for ALF is available here . For details on the checker and a comprehensive overview of the AletheLF language supported by the checker, see the user manual here .
For a quick start, the cvc5 repository contains a script which will download and install the ALF proof checker (alfc), and create scripts for generating proofs with cvc5 and checking them with the ALF proof checker.
The AletheLF language is a meta-framework, meaning that the proof rules used by cvc5 are defined in signature files. The signature files are contained within the cvc5 repository in this directory . Based on these signatures, cvc5 provides basic support for ALF proofs over all theories that it supports.
Note that several proof rules in the internal calculus are not yet supported in ALF signatures. Steps that use such rules are printed as trust steps in the ALF proof. A trust step proves an arbitrary formula with no provided justification. The ALF proof contains warnings for trust steps that indicate which internal proof rules were recorded as trust steps in the ALF proof.
To get more fine-grained proofs, the additional option proof-granularity=theory-rewrite can be passed to cvc5. This often will result in ALF proofs with more detail, and whose trust steps correspond only to equalities corresponding to theory rewrites.
A simple example of cvc5 producing a proof in ALF proof format:
$ bin/cvc5 --dump-proofs --proof-format-mode=alf --proof-granularity=theory-rewrite ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
unsat
(declare-fun c () Bool)
(declare-fun b () Bool)
(declare-fun d () Bool)
(define @t1 () (= b d))
(define @t2 () (or b d))
(define @t3 () (= @t2 @t1))
(define @t4 () (ite d c false))
(define @t5 () (= c d))
(define @t6 () (or d b))
(define @t7 () (not d))
(assume @p1 (and @t6 @t5 (not @t4) @t3))
; WARNING: add trust step for TRUST_THEORY_REWRITE
; trust TRUST_THEORY_REWRITE
(step @p2 :rule trust :args ((= (and @t6 true @t7 @t3) (and @t6 @t7 @t3))))
(step @p3 :rule refl :args (@t6))
; trust TRUST_THEORY_REWRITE
(step @p4 :rule trust :args ((= (= d d) true)))
; trust TRUST_THEORY_REWRITE
(step @p5 :rule trust :args ((= (and d d) d)))
(step @p6 :rule cong :premises (@p5) :args (not))
(step @p7 :rule refl :args (@t3))
(step @p8 :rule nary_cong :premises (@p7 @p6 @p4 @p3) :args (and true))
(step @p9 :rule trans :premises (@p8 @p2))
(step @p10 :rule refl :args (d))
(step @p11 :rule refl :args (@t5))
; trust TRUST_THEORY_REWRITE
(step @p12 :rule trust :args ((= @t4 (and d c))))
(step @p13 :rule cong :premises (@p12) :args (not))
(step @p14 :rule nary_cong :premises (@p7 @p13 @p11 @p3) :args (and true))
(step @p15 :rule eq_resolve :premises (@p1 @p14))
(step @p16 :rule and_elim :premises (@p15) :args (1))
(step @p17 :rule cong :premises (@p16 @p10) :args (=))
(step @p18 :rule nary_cong :premises (@p16 @p10) :args (and true))
(step @p19 :rule cong :premises (@p18) :args (not))
(step @p20 :rule nary_cong :premises (@p7 @p19 @p17 @p3) :args (and true))
(step @p21 :rule trans :premises (@p20 @p9))
(step @p22 :rule trans :premises (@p14 @p21))
(step @p23 :rule eq_resolve :premises (@p1 @p22))
(step @p24 :rule and_elim :premises (@p23) :args (0))
(step @p25 :rule reordering :premises (@p24) :args (@t2))
(step @p26 :rule and_elim :premises (@p23) :args (1))
(step @p27 :rule chain_resolution :premises (@p25 @p26) :args ((and true d)))
(step @p28 :rule cnf_equiv_pos1 :args (@t1))
(step @p29 :rule reordering :premises (@p28) :args ((or d (not b) (not @t1))))
(step @p30 :rule chain_resolution :premises (@p29 @p26 @p27) :args ((and true d false b)))
(step @p31 :rule and_elim :premises (@p23) :args (2))
(step @p32 :rule equiv_elim1 :premises (@p31))
(step @p33 :rule reordering :premises (@p32) :args ((or @t1 (not @t2))))
(step @p34 false :rule chain_resolution :premises (@p33 @p30 @p25) :args ((and true @t1 false @t2)))