Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:interpolation_for_propositional_logic [2008/03/11 16:15] vkuncak |
sav08:interpolation_for_propositional_logic [2008/03/17 20:24] piskac |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| **Definition of Interpolant:** | **Definition of Interpolant:** | ||
| - | Given two propositional formulas $F$ and $G$, an interpolant for $(F,G)$ is a propositional formula $H$ such that: \\ | + | Given two propositional formulas $F$ and $G$, such that $\models F \rightarrow G$, an interpolant for $(F,G)$ is a propositional formula $H$ such that: \\ |
| 1) $\models F \rightarrow H$ \\ | 1) $\models F \rightarrow H$ \\ | ||
| 2) $\models H \rightarrow G$ \\ | 2) $\models H \rightarrow G$ \\ | ||
| Line 11: | Line 11: | ||
| ++++ | ++++ | ||
| - | Note that $F \rightarrow G$ by transitivity of $\rightarrow$. The interpolant extracts what makes $F$ imply $G$. | + | |
| + | Note that $F \rightarrow G$ by transitivity of $\rightarrow$. The interpolant extracts the essential part of formula $F$ which makes $F$ imply $G$. | ||
| Let $elim$ denote the operator that eliminates propositional quantifiers (see [[QBF and Quantifier Elimination]]). | Let $elim$ denote the operator that eliminates propositional quantifiers (see [[QBF and Quantifier Elimination]]). | ||
| - | Here are two simple ways to construct an interpolant: | + | Here are two **simple ways to construct an interpolant:** |
| * We can quantify existentially all variables in $F$ that are not in $G$. | * We can quantify existentially all variables in $F$ that are not in $G$. | ||
| Line 24: | Line 25: | ||
| $H_{max} \equiv elim(\forall q_1, q_2, ..., q_m.\ G)$ where $\{q_1, q_2, ..., q_m \}\ = FV(G)\backslash FV(F)$ \\ | $H_{max} \equiv elim(\forall q_1, q_2, ..., q_m.\ G)$ where $\{q_1, q_2, ..., q_m \}\ = FV(G)\backslash FV(F)$ \\ | ||
| - | More precisely, let ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$, that is, | + | **Definition:** ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$, that is, |
| \[ | \[ | ||
| {\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \} | {\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \} | ||
| \] | \] | ||
| - | Then the following properties hold: | + | |
| + | **Theorem:** The following properties hold for $H_{min}$, $H_{max}$, ${\cal I}(F,G)$ defined above: | ||
| - $H_{min} \in {\cal I}(F,G)$ | - $H_{min} \in {\cal I}(F,G)$ | ||
| - $\forall H \in {\cal I}(F,G).\ \models (H_{min} \rightarrow H)$ | - $\forall H \in {\cal I}(F,G).\ \models (H_{min} \rightarrow H)$ | ||