Proof format: DOT ¶

Using the flag proof-format-mode=dot , cvc5 outputs proofs in the DOT format.

The DOT format is a graph description language (see e.g. this description ). It can be used, among other things, for visualization.

We leverage this format for visualizing cvc5 proofs, in the internal calculus, as a graph. One can use a default dot visualizer or the dedicated proof visualizer available here . It suffices to upload the DOT proof outputted by cvc5, saved into a file. The visualizer offers several custom features, such as fold/unfold subproofs, coloring nodes, and stepwise expansion of let terms.