## Notes

### Interpolants and Relevance

• logic
• interpolants

For a pair of inconsistent formulas $(A, B)$, i.e., $A \wedge B \equiv \bot$ or unsatisfiable, the Craig Interpolant [1] for $(A, B)$ is a formula $\mathcal{I}$ such that

• $A \to \mathcal{I}$,
• $\mathcal{I} \wedge B \equiv \bot$, and
• $\mathcal{I}$ contains variables common to $A$ and $B$.

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