Proof production ¶

cvc5 produces proofs in an internal proof calculus that faithfully reflects its reasoning. Here is a comprehensive description of the proof rules .

Optionally cvc5 can convert and output its internal proofs into the following external formats:

where note that the DOT format is only meant for visualization.