Proofs
SMTInterpol uses its own proof format RESOLUTE to represent proofs. This is a simple proof format based on resolution.
- See the online documentation of RESOLUTE.
- We have a web demo for the proof generator/verifier.
Publication
- Jochen Hoenicke and Tanja Schindler. A Simple Proof Format for SMT. In SMT 2022. [pdf]