# Interpolation for Propositional Logic

**Definition of Interpolant:**
Given two propositional formulas and , such that , an interpolant for is a propositional formula such that:

1)

2)

3)

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 .

where

- We can quantify universally all variables in that are not in .

where

**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.