Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav08:interpolants_from_resolution_proofs [2008/03/18 10:05] tatjana |
sav08:interpolants_from_resolution_proofs [2008/03/18 10:49] tatjana |
||
|---|---|---|---|
| Line 21: | Line 21: | ||
| * 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)$ | ||
| - | * if $q \in FV(A) \cap FV(B)$ then $I(C) = ite(q,I(C_1),I(C_2))$ | + | * if $q \in FV(A) \cap FV(B)$ then $I(C) = ite(q,I(C_2),I(C_1))$ |
| We prove that $I(C)$ has the desired property by induction on the structure of the resolution proof tree. | We prove that $I(C)$ has the desired property by induction on the structure of the resolution proof tree. | ||