Documentation for the Z3 proof language #5671
-
|
Is there a specification of Z3 proof language? |
Beta Was this translation helpful? Give feedback.
Answered by
NikolajBjorner
Nov 18, 2021
Replies: 1 comment
-
|
There is a workshop paper, IWIL 2008, that describes the design and main proof rules. |
Beta Was this translation helpful? Give feedback.
0 replies
Answer selected by
wenkokke
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
There is a workshop paper, IWIL 2008, that describes the design and main proof rules.
Select rules have been added over time, hyper-resolution.
The proof checker code serves as an entry point for providing an independent description of what is expected,
https://github.com/Z3Prover/z3/blob/master/src/ast/proofs/proof_checker.h