Superposition calculus: Difference between revisions
Wolfgang42 (talk | contribs) Disambiguated: theorem prover → Automated theorem prover |
No edit summary |
||
| Line 1: | Line 1: | ||
The '''superposition calculus''' is a calculus for [[automated theorem proving|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 algorithm|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, every |
The '''superposition calculus''' is a calculus for [[automated theorem proving|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 algorithm|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, every unsatisfiable (logic)|unsatisfiable clause set can eventually be proved to be unsatisfiable. |
||
As of 2007, most of the (state-of-the-art) [[Automated theorem prover|theorem prover]]s for [[first-order logic]] are based on superposition (e.g. the [[E equational theorem prover]]), although only a few implement the pure calculus. |
As of 2007, most of the (state-of-the-art) [[Automated theorem prover|theorem prover]]s for [[first-order logic]] are based on superposition (e.g. the [[E equational theorem prover]]), although only a few implement the pure calculus. |
||
| Line 8: | Line 8: | ||
* [[SPASS theorem prover|SPASS]] |
* [[SPASS theorem prover|SPASS]] |
||
* [[Vampire theorem prover|Vampire]] |
* [[Vampire theorem prover|Vampire]] |
||
* |
* Waldmeister theorem prover|Waldmeister |
||
* |
* Ayane theorem prover|Ayane at [http://code.google.com/p/ayane/ Google Code ] |
||
== References == |
== References == |
||
Revision as of 02:38, 1 February 2013
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, every unsatisfiable (logic)|unsatisfiable clause set can eventually be proved to be unsatisfiable.
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 theorem prover|Waldmeister
- Ayane theorem prover|Ayane at Google Code
References
- Rewrite-Based Equational Theorem Proving with Selection and Simplification, Leo Bachmair and 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), Elsevier Science and MIT Press, 2001.
 | This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |