## Notes

### 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.