Differences

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

--- sav08:interpolation_for_propositional_logic [2008/03/10 10:57]
vkuncak
+++ sav08:interpolation_for_propositional_logic [2015/04/21 17:30] (current)
@@ Line 1: / Line 1: @@
 ====== Interpolation for Propositional Logic ======
-Given two propositional formulas $F$ and $G$, an interpolant is a propositional formula $H$ such that: \\
+**Definition of Interpolant:**
+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: \\
 ) $\models F \rightarrow H$ \\
 ) $\models H \rightarrow G$ \\
 ) $FV(H)\subseteq FV(F) \cap FV(G)$
-$FV$ denotes the set of free variables in the given propositional formula (see [[Propositional Logic Syntax]]).
+++++What is FV?|
+$FV$ denotes the set of free variables in the given propositional formula, see [[Propositional Logic Syntax]].
+++++
-Note that $F \rightarrow G$ by transitivity of $\rightarrow$. The interpolant extracts what makes $F$ imply $G$.
-Here are two easy ways to create an interpolant.
+Note that $F \rightarrow G$ by transitivity of $\rightarrow$. The interpolant extracts the essential part of formula $F$ which makes $F$ imply $G$.
-  * We can quantify existentially all variables in $F$ that are not in $G$.  We obtain the //weakest interpolant//:
-$H_{min} \equiv \exists p_1, p_2, ..., p_n.\  F$ where $\{p_1, p_2, ..., p_n \}\ = FV(F)\backslash FV(G)$ \\
+Let $elim$ denote the operator that eliminates propositional quantifiers (see [[QBF and Quantifier Elimination]]).
-  * We can quantify universally all variables in $G$ that are not in $F$.  We obtain the //strongest interpolant//:
+Here are two **simple ways to construct an interpolant:**
+  * We can quantify existentially all variables in $F$ that are not in $G$.
-$H_{max} \equiv \forall p_1, p_2, ..., p_n.\ G$ where $\{p_1, p_2, ..., p_n \}\ = FV(G)\backslash FV(F)$ \\
+$H_{min} \equiv elim(\exists p_1, p_2, ..., p_n.\  F)$ where $\{p_1, p_2, ..., p_n \}\ = FV(F)\backslash FV(G)$ \\
-We can also derive interpolants from resolution proofs, as we will see in [[lecture07]].
+  * We can quantify universally all variables in $G$ that are not in $F$.
-  * [[http://citeseer.ist.psu.edu/36219.html|Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations]]
+$H_{max} \equiv elim(\forall q_1, q_2, ..., q_m.\ G)$ where $\{q_1, q_2, ..., q_m \}\ = FV(G)\backslash FV(F)$ \\
-  * [[http://citeseer.ist.psu.edu/700371.html|The Complexity of Boolean Functions]]
+**Definition:** ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$, that is,
+\begin{equation*}
+   {\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \}
+\end{equation*}
+**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)$
+  - $H_{max} \in {\cal I}(F,G)$
+  - $\forall H \in {\cal I}(F,G).\ \models (H \rightarrow H_{max})$
+We can also derive interpolants from resolution proofs, as we will see in [[lecture07]].