Craig Interpolation

Every proof of contradiction carries a secret. In 1957, logician William Craig noticed that whenever two formulas $A$ and $B$ together are unsatisfiable — meaning no assignment of truth values can satisfy both at once — there is always a third formula $I$ that:

1. is implied by $A$ (every model of $A$ is also a model of $I$),
2. is inconsistent with $B$ ($I \land B$ is unsatisfiable),
3. only mentions symbols that appear in both $A$ and $B$.

That formula $I$ is the interpolant. It speaks only the shared language of $A$ and $B$, yet it fully explains the contradiction between them. Craig proved such an $I$ always exists for classical propositional and first-order logic.

For half a century the theorem lived quietly in logic textbooks. Then, in 2003, Kenneth McMillan discovered that SAT solvers could compute interpolants from resolution proofs — and suddenly the theorem became the engine behind modern program verification.

Pick two propositional formulas $A$ and $B$ from the presets below, or enter your own. The demo checks that $A \land B$ is unsatisfiable, then derives an interpolant $I$ over the shared variables.

<!-- {{c_html_intro}} -->
<div class="panel">
  <label class="label">{{label_preset}}</label>
  <div class="presets" id="presets"></div>
</div>
<div class="panel two-col">
  <div>
    <label class="label">{{label_a}}</label>
    <textarea id="inputA" rows="2" placeholder="{{placeholder_a}}"></textarea>
  </div>
  <div>
    <label class="label">{{label_b}}</label>
    <textarea id="inputB" rows="2" placeholder="{{placeholder_b}}"></textarea>
  </div>
</div>
<button id="btnDerive" type="button">{{btn_derive}}</button>
<div id="status" class="status"></div>
<div id="result" class="result hidden">
  <div class="row"><span class="tag tagA">A</span><span id="dispA"></span></div>
  <div class="row"><span class="tag tagI">I</span><span id="dispI"></span></div>
  <div class="row"><span class="tag tagB">B</span><span id="dispB"></span></div>
  <div id="explanation" class="explanation"></div>
</div>

/* {{c_css_intro}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.panel { margin-bottom: .75rem; }
.two-col { display: grid; grid-template-columns: 1fr 1fr; gap: .6rem; }
.label { display: block; font-size: .8rem; font-weight: 600; color: #555; margin-bottom: .25rem; text-transform: uppercase; letter-spacing: .04em; }
textarea { width: 100%; font: 14px ui-monospace, monospace; border: 1px solid #cdd9e3; border-radius: 6px; padding: .4rem .5rem; resize: vertical; }
textarea:focus { outline: 2px solid #1d3557; }
.presets { display: flex; flex-wrap: wrap; gap: .4rem; }
.preset-btn { font: 600 12px system-ui; padding: .3rem .7rem; border: 1px solid #1d3557; border-radius: 20px; background: #fff; color: #1d3557; cursor: pointer; transition: background .15s; }
.preset-btn:hover, .preset-btn.active { background: #1d3557; color: #fff; }
button#btnDerive { font: 600 14px system-ui; padding: .45rem 1.1rem; border: 1px solid #1d3557; background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; margin-bottom: .6rem; }
.status { font-size: .9rem; font-weight: 600; min-height: 1.4em; margin-bottom: .5rem; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.result { background: #f6f8fb; border: 1px solid #cdd9e3; border-radius: 8px; padding: .75rem; }
.result.hidden { display: none; }
.row { display: flex; align-items: baseline; gap: .5rem; margin-bottom: .35rem; font: 14px ui-monospace, monospace; }
.tag { display: inline-block; width: 1.5rem; text-align: center; font: 700 12px system-ui; padding: .1rem 0; border-radius: 4px; }
.tagA { background: #dbeafe; color: #1e3a8a; }
.tagI { background: #d1fae5; color: #065f46; font-size: 13px; }
.tagB { background: #ffe4e6; color: #9b1c1c; }
.explanation { font-size: .82rem; color: #444; line-height: 1.5; margin-top: .5rem; border-top: 1px solid #dde3ea; padding-top: .5rem; }

// Code not found

Notice the key property: $I$ only mentions variables that appear in both $A$ and $B$. Variables private to $A$ vanish; variables private to $B$ also vanish. What remains is the exact shared reason the two sides cannot agree.

Craig's theorem guarantees existence but says nothing about size. In practice:

• Computing an interpolant from a resolution proof runs in polynomial time in the proof size — each resolution step contributes at most a small formula fragment.
• The result can be exponentially large as a formula. A compact proof can still produce an interpolant with exponentially many clauses when written in CNF.
• Circuits save the day. Representing the interpolant as a Boolean circuit (DAG) keeps it polynomial in the proof size. McMillan's 2003 key insight was to stay in circuit form and never expand to CNF.
• Minimal interpolants are hard. Finding the smallest formula that separates $A$ from $B$ is $\Sigma_2^P$-complete — one level above NP in the polynomial hierarchy.

The gap between "interpolants exist and are easy to compute" and "the smallest interpolant is hard to find" mirrors a recurring theme in logic: existence is cheap, optimality is expensive.

Craig interpolation turned from a curiosity into a cornerstone of automated reasoning:

• CEGAR (Counterexample-Guided Abstraction Refinement): when a model checker finds a spurious counterexample, it uses interpolation to extract an invariant that rules it out and refine the abstraction. Tools like SLAM and Blast use this to verify millions of lines of code automatically.
• Invariant synthesis: the interpolant between the initial states $A$ and the bad states $B$ is often exactly the inductive invariant a proof needs. The formula says "this is what always holds between the two sides."
• Modular reasoning: interpolants let you summarize what one module "tells" another without exposing internal variables — the shared symbols become a clean interface specification.
• Interpolating theorem provers: tools like iZ3 and SMTInterpol extend Craig interpolation to richer theories (integers, arrays, uninterpreted functions) used in real programs.

Understanding Craig interpolation means understanding why SAT-based verification can scale to real software — it is the mechanism that turns a proof of failure into a formula that prevents the same failure from recurring.

Craig interpolation is one of logic's quiet triumphs: a theorem proved for purely philosophical reasons in 1957 that turned out to be exactly the tool verification engineers needed half a century later.

The interpolant $I$ that sits between $A$ and $B$ is not just any separator — it is the minimal shared explanation of their conflict, speaking only the language both sides understand. Extracting it from a resolution proof is cheap; using it to synthesize invariants and refine abstractions made automated verification of real software possible.

The next time a SAT solver tells you a system is correct, there is a good chance a Craig interpolant is the reason it could figure that out at all.