Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:interpolants_from_resolution_proofs [2008/03/12 01:11] vkuncak |
sav08:interpolants_from_resolution_proofs [2008/03/12 13:31] vkuncak |
||
---|---|---|---|
Line 18: | Line 18: | ||
* if $C \in A$ then $I(C) = {\it false}$ | * if $C \in A$ then $I(C) = {\it false}$ | ||
* if $C \in B$ then $I(C) = {\it true}$ | * if $C \in B$ then $I(C) = {\it true}$ | ||
- | * if $C$ is result of applying resolution to $C_1$, $C_2$ along propositional variable $q$ then | + | * if $C$ is result of applying resolution to $C_1$, $C_2$ along propositional variable $q$ where $\lnot q \in C_1$, and $q \in C_2$, then |
* if $q \in FV(A) \setminus FV(B)$ then $I(C) = I(C_1) \lor I(C_2)$ | * if $q \in FV(A) \setminus FV(B)$ then $I(C) = I(C_1) \lor I(C_2)$ | ||
* if $q \in FV(B) \setminus FV(A)$ then $I(C) = I(C_1) \land I(C_2)$ | * if $q \in FV(B) \setminus FV(A)$ then $I(C) = I(C_1) \land I(C_2)$ |