Superposition Calculus

Origin. Leo Bachmair and Harald Ganzinger, "Rewrite-based equational theorem proving with selection and simplification" (Journal of Logic and Computation 4(3), 1994, 217–247). The ancestry is twofold: George Robinson and Larry Wos's paramodulation (1969) added an equality-replacement rule to resolution, and Donald Knuth and Peter Bendix, "Simple word problems in universal algebras" (in Computational Problems in Abstract Algebra, ed. John Leech, Pergamon 1970, 263–297), showed that orienting equations by a reduction ordering and resolving critical pairs yields a decision procedure whenever completion terminates. Superposition is the merger: paramodulation disciplined by Knuth–Bendix-style orderings, with literal selection and a redundancy criterion that admits simplification into the calculus itself.

Models. Resolution extended to first-order logic with equality, with the extension governed by a term ordering: equations are used left to right only when that rewrites larger to smaller, and inferences touch only maximal or selected literals. Resolution refutes by closing a clause set under one rule; superposition refutes by saturating under rewriting-shaped inferences, and its completeness proof builds a term-rewriting model out of the saturated set itself. It is the calculus the first-order provers with equality actually run.

Formalism.

Setting: Clauses over first-order terms; literals s ≈ t and s ≉ t. ≻: a reduction ordering total on ground terms — KBO or LPO in practice. Selection function: may select negative literals; a selected literal takes part in inferences regardless of maximality.

Superposition: C ∨ s ≈ t D ∨ L[s′] σ = mgu(s, s′) ───────────────────────────────────────── (C ∨ D ∨ L[t])σ L[s′]: a literal with subterm s′ at a nonvariable position. Conditions: s′ is not a variable; ¬(sσ ≼ tσ); (s ≈ t)σ strictly maximal in its clause and nothing selected there; L[s′]σ maximal in its clause, or selected.

Equality resolution: C ∨ s ≉ s′ σ = mgu(s, s′) ───────────────────────────── Cσ

Equality factoring: C ∨ s′ ≈ t′ ∨ s ≈ t σ = mgu(s, s′) ─────────────────────────────────────── (C ∨ t ≉ t′ ∨ s ≈ t′)σ

What is restricted: Rewriting happens only at nonvariable positions of the target clause. Only the larger side of an equation rewrites, and only within maximal or selected literals. Unrestricted paramodulation permits replacement at variable positions and from either side of an equation; superposition forbids both and remains refutationally complete. Predicates fold into the equational setting: P(t̄) is read as an equation with a truth constant, so ordered resolution is the degenerate case.

Redundancy and saturation: A clause is redundant if it follows from smaller clauses; an inference is redundant if its conclusion follows from clauses smaller than its largest premise. Simplification — demodulation by oriented unit equations, subsumption, tautology deletion — is redundancy elimination, and deleting the redundant preserves completeness. The prover's loop is saturation up to redundancy under a fair strategy.

Model construction (the completeness method): Order the ground instances of the saturated set by the clause extension of ≻. Induct along the order: each productive clause contributes one oriented ground equation to a rewrite system R. R is convergent by construction, and if the saturated set lacks □, the equality model generated by R satisfies every clause. Contrapositive: an unsatisfiable saturated set contains □ — refutational completeness.

Symbols.

Metatheory. Bachmair and Ganzinger (1994) proved refutational completeness for the calculus with arbitrary selection of negative literals, by the model-construction method, and formulated the abstract redundancy criterion under which deletion preserves completeness — the result that separates superposition from its ancestors, because it turns simplification from a heuristic outside the completeness proof into a rule inside it. The framework generalizes Knuth–Bendix completion: saturating a set of unit equations specializes to completion, and the closure of a non-trivial clause set under non-redundant inferences is often finite and computable, which certifies satisfiability when the empty clause is absent. Completeness requires the ordering to be a reduction ordering extendable to one total on ground terms; KBO and LPO qualify. Equality factoring, like factoring in resolution, is required for completeness. The calculus inherits resolution's logical status: sound, refutationally complete, and a semi-decision procedure — saturation need not terminate on satisfiable input.

Applies to. Automated theorem proving in first-order logic with equality. The saturation provers E, Vampire, and SPASS. The automation behind proof-assistant hammers. Discharge of verification conditions. Equational reasoning in mathematics, descending from the Knuth–Bendix line.

Limitations. Everything Resolution records about clausal form, refutation-only proving, and semi-decidability carries over unchanged. The ordering is fixed before the search begins: completeness holds for any admissible choice, the size of the search space does not, and the calculus offers no rule for choosing. Permutative axioms resist the discipline: commutativity cannot be oriented by any reduction ordering, so such equations stay two-way and multiply inferences. Interpreted theories — arithmetic above all — are not orientable equations either, and need combination methods of the Nelson–Oppen kind rather than saturation. Termination is the exception: the calculus decides fragments only where saturation provably halts, and on open-ended mathematics it is a fair enumeration of consequences, with the empty clause arriving whenever the input is inconsistent and no bound on when.

© 2026 Lingenic LLC