LARA

This is an old revision of the document!

Interpolation for Propositional Logic

Given two propositional formulas $F$ and $G$, an interpolant 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)$

$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. We can quantify existentially all variables in $F$ that are not in $G$:
$H = \exists p_1, p_2, ..., p_n.\ F$ where $\{p_1, p_2, ..., p_n \}\ = FV(F)\backslash FV(G)$
Or we can quantify universally all variables in $G$ that are not in $F$:
$H = \forall p_1, p_2, ..., p_n.\ G$ where $\{p_1, p_2, ..., p_n \}\ = FV(G)\backslash FV(F)$

Interpolants from resolution proofs: to be seen after more details on resolution.