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.