Format Resolute

RESOLUTE (Output)

Short Description

RESOLUTE is a proof format for SMT solvers. It aims at being solver-independent and easy to check. Therefore, a proof in this format consists basically only of the assumptions, axioms for the theories (even for the Boolean operators), and applications of the resolution rule. The atoms in the proof are simply SMT-LIB terms of Boolean sort. let and let-proof allow for sharing. The proof format allows for omitting certain parts of the proof using an oracle axiom.

Syntax

See the documentation of the proof format linked below.

Semantics

See the documentation of the proof format linked below.

Other Information

The proof format is still under development, in particular, it does not yet include axioms for all SMT-LIB theories.

Example

The following proves unsatisfiability of (not (1+1=2)).

(let  ((eq (= (+ 1 1) 2)))
    (res (not eq)
        (assume (not eq))
        (res eq
            (poly+ (+ 1 1) 2)
            (not- (not eq)))))

External Links

https://ultimate.informatik.uni-freiburg.de/smtinterpol/proof-format.html

References

Jochen Hoenicke, Tanja Schindler: A Simple Proof Format for SMT. SMT 2022: 54-70

Systems using this format

SMTInterpol produces proofs in the RESOLUTE format in three different granularities.

Tools

A webinterface for the proof checker is available.