Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:interpolants_from_resolution_proofs [2008/03/12 13:31] vkuncak |
sav08:interpolants_from_resolution_proofs [2008/03/26 20:26] piskac |
||
|---|---|---|---|
| Line 5: | Line 5: | ||
| Let $A$, $B$ be sets of clauses such that $A \land B$ is not satisfiable. An interpolant is a formula $H$ such that | Let $A$, $B$ be sets of clauses such that $A \land B$ is not satisfiable. An interpolant is a formula $H$ such that | ||
| * $\models (A \rightarrow H)$ and $H \land B$ is not satisfiable and | * $\models (A \rightarrow H)$ and $H \land B$ is not satisfiable and | ||
| - | * $FV(H) \subseteq FV(A) \cup FV(B)$ | + | * $FV(H) \subseteq FV(A) \cap FV(B)$ |
| Construct resolution tree that derives a contradiction from $A \cup B$. The tree has elements of $A \cup B$ as leaves and results of application of resolution as nodes. For each clause $C$ in resolution tree we define recursively formula $I(C)$ and show that $I(C)$ is interpolant for these two formulas: | Construct resolution tree that derives a contradiction from $A \cup B$. The tree has elements of $A \cup B$ as leaves and results of application of resolution as nodes. For each clause $C$ in resolution tree we define recursively formula $I(C)$ and show that $I(C)$ is interpolant for these two formulas: | ||
| 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$ where $\lnot q \in C_1$, and $q \in C$, 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)$ | ||