Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:interpolants_from_resolution_proofs [2008/03/12 01:10] vkuncak |
sav08:interpolants_from_resolution_proofs [2008/03/12 01:11] vkuncak |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| * $A \land ((\lnot C)|_A)$ | * $A \land ((\lnot C)|_A)$ | ||
| * $B \land ((\lnot C)|_B)$ | * $B \land ((\lnot C)|_B)$ | ||
| - | where $(\lnto C)|_A$ denotes the conjunction of those literals from $C$ whose propositional variables belong to $FV(A)$. | + | where $(\lnot C)|_A$ denotes the conjunction of those literals from $C$ whose propositional variables belong to $FV(A)$, similarly for $(\lnot C)|_B$. |
| It follows that for empty clause the $I(\emptyset)$ is the interpolant for $(A,B)$. | It follows that for empty clause the $I(\emptyset)$ is the interpolant for $(A,B)$. | ||