Interpolants and Relevance

  • logic
  • interpolants

For a pair of inconsistent formulas , i.e., or unsatisfiable, the Craig Interpolant [1] for is a formula such that

  • ,
  • , and
  • contains variables common to and .

The interpolant can be viewed as the part of that is sufficient, or relevant, to contradict . Modern SAT solvers produce a proof of unsatisfiability, or resolution proof, if the checked formula is unsatisfiable.