# Interpolants from Resolution Proofs

Interpolants in resolution: instead of validity of implication, we look at unsatisfiability.

Let , be sets of clauses such that is not satisfiable. An interpolant is a formula such that

• and is not satisfiable and

Construct resolution tree that derives a contradiction from . The tree has elements of as leaves and results of application of resolution as nodes. For each clause in resolution tree we define recursively formula and show that is interpolant for these two formulas:

where denotes the conjunction of those literals from whose propositional variables belong to , similarly for .

It follows that for empty clause the is the interpolant for .

Construction of :

• if then
• if then
• if then
• if is result of applying resolution to , along propositional variable where , and , then
• if then
• if then
• if then

We prove that has the desired property by induction on the structure of the resolution proof tree.