# Superposition calculus

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Superposition_calculus
> Markdown URL: https://mediated.wiki/source/Superposition_calculus.md
> Source: https://en.wikipedia.org/wiki/Superposition_calculus
> Source revision: 1226528197
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

The '''superposition calculus''' is a [calculus](/source/Formal_system) for [reasoning](/source/automated_theorem_proving) in [equational logic](/source/equational_logic). It was developed in the early 1990s  and combines concepts from [first-order resolution](/source/first-order_resolution) with ordering-based equality handling as developed in the context of (unfailing) [Knuth–Bendix completion](/source/Knuth%E2%80%93Bendix_completion_algorithm). It can be seen as a generalization of either resolution (to equational logic) or unfailing completion (to full [clausal logic](/source/clause_(logic))). Like most [first-order](/source/first-order_logic) calculi, superposition tries to show the ''unsatisfiability'' of a set of first-order [clauses](/source/clauses), i.e. it performs proofs by [refutation](/source/refutation). Superposition is [refutation complete](/source/Completeness_(logic))—given unlimited resources and a ''fair'' derivation strategy, from any [unsatisfiable](/source/unsatisfiable) clause set a contradiction will eventually be derived.

Many (state-of-the-art) [theorem prover](/source/Automated_theorem_prover)s for first-order logic are based on superposition (e.g. the [E equational theorem prover](/source/E_equational_theorem_prover)), although only a few implement the pure calculus.

== Implementations == 

* [E](/source/E_equational_theorem_prover)
* [SPASS](/source/SPASS_theorem_prover)
* [Vampire](/source/Vampire_theorem_prover)
* [Waldmeister](/source/Waldmeister_theorem_prover) [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 [Harald Ganzinger](/source/Harald_Ganzinger), [Journal of Logic and Computation](/source/Journal_of_Logic_and_Computation) 3(4), 1994.
* ''Paramodulation-Based Theorem Proving'', Robert Nieuwenhuis and Alberto Rubio, [Handbook of Automated Reasoning](/source/Handbook_of_Automated_Reasoning) I(7), [Elsevier](/source/Elsevier) Science and [MIT Press](/source/MIT_Press), 2001.

Category:Mathematical logic
Category:Logical calculi
{{mathlogic-stub}}

---
Adapted from the Wikipedia article [Superposition calculus](https://en.wikipedia.org/wiki/Superposition_calculus) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Superposition_calculus?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.