Interpolation for Propositional Logic

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:
1) $\models F \rightarrow H$
2) $\models H \rightarrow G$
3) $FV(H)\subseteq FV(F) \cap FV(G)$

What is FV?

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:

We can quantify existentially all variables in $F$ that are not in $G$ .

$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 quantify universally all variables in $G$ that are not in $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)$

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.