Superposition calculus
The superposition calculus is a calculus for reasoning in equational first-order logic. It was developed in the early 1990s and combines concepts from first-order resolution with ordering-based equality handling as developed in the context of Knuth–Bendix completion. It can be seen as a generalization of either resolution or unfailing completion. 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.
As of 2007, most of the theorem provers for first-order logic are based on superposition, although only a few implement the pure calculus.Implementations
