Interpolants and Relevance
For a pair of inconsistent formulas , i.e., or unsatisfiable, the Craig Interpolant  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.