Interpolation for Propositional Logic
Definition of Interpolant:
Given two propositional formulas and , such that , an interpolant for is a propositional formula such that:
Note that by transitivity of . The interpolant extracts the essential part of formula which makes imply .
Let 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 that are not in .
- We can quantify universally all variables in that are not in .
Definition: denote the set of all interpolants for , that is,
Theorem: The following properties hold for , , defined above:
We can also derive interpolants from resolution proofs, as we will see in lecture07.