Interpolation systems for ground proofs and for general proofs

Interpolation means extracting from a proof of inconsistency of A and B a formula, called interpolant, which is implied by A, is inconsistent with B, and only contains symbols they share. If A and B describe system states, an interpolant captures an intermediate state, and therefore interpolation has applications in software model checking and invariant generation:

Maria Paola Bonacina