The
superposition calculus is a
calculus for
reasoning in equational
first-order logic. It has been developed in the early 1990s and combines concepts from
first-order resolution with ordering-based equality handling as developed in the context of (unfailing)
Knuth–Bendix completion. It can be seen as a generalization of either resolution (to equational logic) or unfailing completion (to full clausal logic). As most first-order calculi, superposition tries to show the
unsatisfiability of a set of first-order
clauses, i.e. it performs proofs by
refutation. Superposition is refutation-complete — given unlimited resources and a
fair derivation strategy, from any
unsatisfiable clause set a contradiction will eventually be derived.