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:interpolation_for_propositional_logic [2008/03/11 16:15] vkuncak |
sav08:interpolation_for_propositional_logic [2008/03/11 16:16] vkuncak |
||
---|---|---|---|
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 28: | Line 29: | ||
{\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:** Then the following properties hold: | ||
- $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)$ |