View source for Superposition calculus

The '''superposition calculus''' is a [[Formal system|calculus]] for [[Automated theorem proving|reasoning]] in [[Equational logic|equational 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 (unfailing) Knuth–Bendix completion. It can be seen as a generalization of either resolution (to equational logic) or unfailing completion (to full [[Philosophy:Clause (logic)|clausal logic]]). Like most [[First-order logic|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 [[Philosophy:Completeness (logic)#Refutation completeness|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 (state-of-the-art) theorem provers for first-order logic are based on superposition (e.g. the E equational theorem prover), although only a few implement the pure calculus.

== Implementations == 

* E
* SPASS
* Vampire
* Waldmeister [https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/waldmeister/ (official web page)]

== References ==

* ''[http://pubman.mpdl.mpg.de/pubman/item/escidoc:1834970/component/escidoc:1857487/MPI-I-91-208.pdf Rewrite-Based Equational Theorem Proving with Selection and Simplification]'', Leo Bachmair and [[Biography:Harald Ganzinger|Harald Ganzinger]], [[Journal of Logic and Computation]] 3(4), 1994.
* ''Paramodulation-Based Theorem Proving'', Robert Nieuwenhuis and Alberto Rubio, [[Handbook of Automated Reasoning]] I(7), [[Company:Elsevier|Elsevier]] Science and MIT Press, 2001.

[[Category:Mathematical logic]]

{{Sourceattribution|Superposition calculus}}