mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-31 19:29:13 +00:00
Code Activity

update docuemntation for codeplex question 29927489/z3-proofs-are-hypothesis-and-lemma-rules-always-cleanly-nested

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-19 08:38:07 -07:00
parent 92cfc242d2
commit 15e1c84592
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/api/z3_api.h
View file

@ -594,7 +594,10 @@ typedef enum
} }
This proof object has one antecedent: a hypothetical proof for false. This proof object has one antecedent: a hypothetical proof for false.
It converts the proof in a proof for (or (not l_1) ... (not l_n)), It converts the proof in a proof for (or (not l_1) ... (not l_n)),
when T1 contains the hypotheses: l_1, ..., l_n. when T1 contains the open hypotheses: l_1, ..., l_n.
The hypotheses are closed after an application of a lemma.
Furthermore, there are no other open hypotheses in the subtree covered by
the lemma.
- Z3_OP_PR_UNIT_RESOLUTION: - Z3_OP_PR_UNIT_RESOLUTION:
\nicebox{ \nicebox{