Interpolant-based model checking is an approximate method

for computing invariants of transition systems. The performance of the

model checker is contingent on the approximation computed, which in

turn depends on the logical strength of the interpolants. A good approx-

imation is coarse enough to enable rapid convergence but strong enough

to be contained within the weakest inductive invariant. We present a

system for constructing propositional interpolants of di erent strength

from a resolution refutation. This system subsumes existing methods and

allows interpolation systems to be ordered by the logical strength of the

obtained interpolants. Interpolants of di erent strength can also be ob-

tained by transforming a resolution proof. We analyse an existing proof

transformation, generalise it, and characterise the interpolants obtained.

%8 17/01/2010 %@ 978-3-642-11318-5