This is an old revision of the document!
Interpolation for Propositional Logic
Given two propositional formulas and
, an interpolant for
is a propositional formula
such that:
1)
2)
3)
denotes the set of free variables in the given propositional formula (see Propositional Logic Syntax).
Note that by transitivity of
. The interpolant extracts what makes
imply
.
Here are two easy ways to create an interpolant. Let denote the operator that eliminates propositional quantifiers (see QBF and Quantifier Elimination):
- We can quantify existentially all variables in
that are not in
.
where
- We can quantify universally all variables in
that are not in
.
where
More precisely, let denote the set of all interpolants for
, that is,
\[
{\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \}
\] Then the following properties hold:
We can also derive interpolants from resolution proofs, as we will see in lecture07.