Proof Production 

cvc5 produces proofs in a proof calculus that faithfully reflects its reasoning. The calculus is called the Cooperating Proof Calculus (CPC). cvc5 supports retrieving a proof object via the API (see how these objects are defined in C++ , C , Java , Base Python ).

Proof Rules 

A comprehensive description of the proof rules of the Cooperating Proof Calculus can be found here:

C++ API
C API
Java API
- enum ProofRule
- enum ProofRewriteRule
Base Python API

Proof Formats 

Optionally, cvc5 allows to convert and output its internal proofs into the following external formats.

Note that the DOT format is only meant for visualization.