The "evidence" produced by Z3 is not intended for human consumption. An outdated version of the format is described in the document: Evidence and Disclaimer and Z3 . The z3_api.h
file has a long description of each of the evidence. Verification rule identifiers begin with Z3_OP_PR
. I know about two applications that use Z3 proof objects. The following documents contain many examples and describe how evidence objects can be used.
1- Isabella Interactive Theoretical Theorem: Z3 proofs are reconstructed inside Isabelle using a trusted kernel. You can find several works describing this work, and the Z3 proof format on the Sascha Bohme Home page
2- Interpolation Generation
As the pack says, unsat-cores
much easier to use.
source share