Consider a verification engineer facing a proof obligation of staggering complexity: a program invariant spanning arithmetic constraints, array manipulations, and bit-vector operations, all entangled in a single verification condition. A monolithic decision procedure would drown in the combinatorial explosion. Yet modern verifiers dispatch such obligations routinely. The secret lies in a theorem proved by William Craig in 1957, whose deep implications the computational community continues to unpack.

Craig's interpolation theorem asserts something quite remarkable about first-order logic: whenever an implication A → B holds, there exists an intermediate formula I, expressed only in the shared vocabulary of A and B, that witnesses the entailment. This shared-vocabulary interpolant acts as a semantic bridge, isolating precisely what A conveys to B.

For the computational logician, this is more than metamathematical curiosity. Interpolation transforms proof theory into an engineering discipline. It licenses the decomposition of reasoning tasks into loosely coupled components, permits heterogeneous decision procedures to cooperate coherently, and yields the abstraction predicates that drive counterexample-guided verification. In what follows, we examine Craig's result, its role in the Nelson-Oppen combination framework, and its central position in modern software verification pipelines built atop SMT solvers like Z3, CVC5, and MathSAT.

Craig's interpolation theorem, in its classical form, states: if A ⊨ B in first-order logic, then there exists a formula I such that A ⊨ I, I ⊨ B, and every non-logical symbol occurring in I occurs in both A and B. The interpolant I lives entirely in the shared signature, filtering out symbols idiosyncratic to either side.

The proof-theoretic construction proceeds by induction on cut-free sequent proofs or resolution refutations. Given a refutation of A ∧ ¬B, one traces how symbols propagate through inference steps, systematically projecting each intermediate formula onto the shared vocabulary. Pudlák's algorithm and McMillan's variant produce interpolants directly from resolution proofs in linear time, making the theorem constructively useful rather than merely existential.

The significance runs deeper than symbol elimination. An interpolant captures the minimal semantic content that A transmits to B. If we think of A and B as modules communicating over an interface—the shared symbols—then I is a valid interface contract. This viewpoint anticipates modular reasoning: local knowledge stays local, only interface facts propagate.

Not every logic enjoys interpolation. Modal logics vary; some description logics fail Craig interpolation while satisfying weaker Beth definability. In quantifier-free fragments with theories, one demands theory-specific interpolation: for theory T, if A ∧ B is T-unsatisfiable, an interpolant exists in the common signature of A and B, possibly extended with theory symbols. Linear arithmetic, uninterpreted functions, and arrays admit such procedures; nonlinear integer arithmetic does not, in general.

This delineation matters computationally. When we choose a logical fragment for verification, we implicitly choose whether modular reasoning is available. The interpolation property is thus a design criterion for reasoning systems, not merely a theorem about them.

Takeaway

An interpolant is the smallest semantic bridge between two formulas—everything one side needs to say to the other, and nothing more. Modularity in reasoning is the ability to identify and honor that bridge.

Real verification problems rarely fit a single theory. A formula might mix linear arithmetic (x + y ≤ z), uninterpreted functions (f(x) = f(y)), and arrays (select(store(a, i, v), j)). The Nelson-Oppen framework combines decision procedures for individual theories into a decision procedure for their union, provided the theories are stably infinite and signature-disjoint.

The mechanism is deceptively simple: purify the input formula by introducing fresh variables so each atomic formula belongs to a single theory, then have the procedures exchange equalities between shared variables. If T₁ deduces x = y, it communicates this to T₂, which incorporates it and may deduce further equalities. Termination follows from the finiteness of shared variables.

Interpolation lies at the semantic heart of why this works. The equalities exchanged between procedures are precisely the shared-signature consequences—the interpolants—that each theory contributes about the shared variables. When Nelson-Oppen exchanges x = y, it is transmitting a Craig interpolant restricted to the pure-equality fragment common to any first-order theory.

This connection becomes explicit in model-based theory combination and in interpolation-based combination frameworks. Instead of merely equalities, procedures can exchange richer interpolants when the shared signature is broader. Ghilardi's work on interpolating combinations shows how to combine interpolating decision procedures to obtain an interpolating procedure for the union—closure under combination is preserved precisely when interpolation is available.

For the implementer, this reframes theory combination as an information-theoretic problem: what is the least each theory must reveal about shared symbols so that the whole is consistent? Interpolation supplies the answer, and modern SMT architectures like DPLL(T) internalize this exchange within their lemma-learning loops.

Takeaway

Theory combination is not about merging logics—it is about disciplined information exchange over shared vocabulary. Each theory reveals only what the interface demands, preserving locality.

The most consequential application of interpolation is in counterexample-guided abstraction refinement (CEGAR), particularly McMillan's interpolation-based model checking. Given a program and an unsafe error location, the model checker unrolls the transition relation into a bounded path formula. If the path is infeasible, its unsatisfiability proof yields interpolants at each program point—formulas that overapproximate reachable states and exclude the error.

These interpolants become predicate abstractions. Rather than manually specifying which predicates matter, the tool derives them from the refutation of concrete counterexamples. This closes a long-standing loop in software verification: lazy abstraction with interpolants, implemented in tools like IMPACT, CPAchecker, and SeaHorn, discovers loop invariants and inductive strengthenings automatically.

The mathematics is elegant. For a path φ₀ ∧ φ₁ ∧ ... ∧ φₙ that is unsatisfiable, we compute interpolants I₀, I₁, ..., Iₙ such that each Iₖ follows from the prefix and refutes the suffix, using only shared variables—precisely the program variables live at that point. The sequence I₀ ⇒ I₁ ⇒ ... ⇒ Iₙ forms an inductive Hoare-style annotation.

Beyond model checking, interpolation drives compositional verification. Assume-guarantee reasoning decomposes a system into components whose interfaces are specified by interpolants extracted from joint refutations. Horn clause solvers like Spacer generalize this to recursive procedures, computing procedure summaries as interpolants over parameter and return values.

The engineering payoff is decisive. Instead of monolithic verification conditions that overwhelm solvers, interpolation yields proof decomposition: independent lemmas, checkable in isolation, that compose into a global proof. This is the same modularity that structured programming brought to code, now brought to correctness arguments.

Takeaway

Interpolation turns a counterexample into a lesson learned—not a fact about one execution, but an invariant about many. Verification becomes the systematic accumulation of shared-vocabulary insights.

Craig's 1957 result was, on its face, a technical curiosity about first-order derivations. Sixty-plus years later, it underwrites the architecture of modern reasoning systems. Interpolation supplies the semantic glue for theory combination, the abstraction predicates for model checking, and the summaries for compositional verification.

The deeper lesson is architectural: modular reasoning requires modular semantics. Systems that cannot expose their shared-signature content cannot be composed reliably. When we design new logics, decision procedures, or verification frameworks, the question of interpolation is not an afterthought—it determines whether the system will scale by composition or collapse under monolithic obligations.

For AI reasoning more broadly, interpolation suggests a principle worth inheriting. As neurosymbolic systems combine learned components with logical reasoners, the interface between them will demand its own interpolants: minimal, shared-vocabulary contracts that let heterogeneous reasoners cooperate without demanding a common ontology.