Format cvc5

cvc5 Format (Output)

Names

cvc5 proof output format

Short Description

This format is used by cvc5 to print proofs when no specific output format is selected. It is a textual representation of the internal proof data structures, and is intended for debugging and similar purposes.

Syntax

The syntax of the proof format is based on SMT-LIB. It uses SMT-LIB formulas and let expressions to structure the proof.

Semantics

A comprehensive documentation of the proof rules used by this proof output is available in the cvc5 online documentation.

Other Information

The proof output can differ between cvc5 releases and is not versioned independently.

It is possible to ask cvc5 to print the proofs with different levels of granularity by using the --proof-granularity command line option.

Example

The following is refutation of $f(c) \land \forall x. f(x)$.

unsat
(
(let ((_let_1 (f c))) 
(let ((_let_2 (forall ((x S)) (not (f x))))) 
(let ((_let_3 (_let_2))) 
(let ((_let_4 (ASSUME :args _let_3))) 
(SCOPE (MACRO_RESOLUTION_TRUST 
       (IMPLIES_ELIM (SCOPE 
          (INSTANTIATE _let_4 :args (c QUANTIFIERS_INST_CBQI_CONFLICT)) :args _let_3)) 
       (ASSUME :args (_let_1)) _let_4 :args (false false _let_1 false _let_2)) :args (_let_2 _let_1))))))
)

External Links

• The cvc5 theorem prover
• Documentation of the proof format

References

• Flexible Proof Production in an Industrial-Strength SMT Solver Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark Barrett In Blanchette, J., Kovacs, L., Pattinson, D. (eds.) 11th International Joint Conference on Automated Reasoning (IJCAR 2022), Springer, 2022.

Systems using this format