| Revision as of 17:25, 3 February 2013 editBenea (talk | contribs)Autopatrolled, Pending changes reviewers, Rollbackers32,665 editsm Reverted edits by RichardMills65 (talk) to last version by Wolfgang42← Previous edit | Revision as of 12:37, 23 March 2013 edit undoAddbot (talk | contribs)Bots2,838,809 editsm Bot: Migrating 1 interwiki links, now provided by Wikidata on d:q7644107Next edit → | ||
| Line 19: | Line 19: | ||
| ] | ] | ||
| {{mathlogic-stub}} | {{mathlogic-stub}} | ||
| ] | |||
Revision as of 12:37, 23 March 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 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
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 Misplaced Pages by expanding it. |