Differences

This shows you the differences between two versions of the page.

--- sav08:interpolation_for_propositional_logic [2008/03/11 16:15]
vkuncak
+++ sav08:interpolation_for_propositional_logic [2008/03/11 16:18]
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]]).
-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$.
@@ 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)$ \\
-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)$ \}
 \]
-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)$
   - $\forall H \in {\cal I}(F,G).\ \models (H_{min} \rightarrow H)$