| Revision as of 02:38, 1 February 2013 editRichardMills65 (talk | contribs)Extended confirmed users25,484 editsNo edit summary← Previous edit | Latest revision as of 06:19, 31 May 2024 edit undoDavid Eppstein (talk | contribs)Autopatrolled, Administrators225,942 edits rewrite to avoid dated stmt | ||
| (14 intermediate revisions by 12 users not shown) | |||
| Line 1: | Line 1: | ||
| The '''superposition calculus''' is a calculus for ] in |
The '''superposition calculus''' is a ] for ] in ]. It was developed in the early 1990s and combines concepts from ] with ordering-based equality handling as developed in the context of (unfailing) ]. It can be seen as a generalization of either resolution (to equational logic) or unfailing completion (to full ]). Like most ] calculi, superposition tries to show the ''unsatisfiability'' of a set of first-order ], i.e. it performs proofs by ]. Superposition is ]—given unlimited resources and a ''fair'' derivation strategy, from any ] clause set a contradiction will eventually be derived. | ||
| Many (state-of-the-art) ]s for first-order logic are based on superposition (e.g. the ]), although only a few implement the pure calculus. | |||
| == Implementations == | == Implementations == | ||
| Line 8: | Line 8: | ||
| * ] | * ] | ||
| * ] | * ] | ||
| * Waldmeister theorem prover|Waldmeister | * ] | ||
| * Ayane theorem prover|Ayane at | |||
| == References == | == References == | ||
| * ''Rewrite-Based Equational Theorem Proving with Selection and Simplification'', Leo Bachmair and Harald Ganzinger, Journal of Logic and Computation 3(4), 1994. | * '''', Leo Bachmair and ], ] 3(4), 1994. | ||
| * ''Paramodulation-Based Theorem Proving'', Robert Nieuwenhuis and Alberto Rubio, ] I(7), ] Science and ], 2001. | * ''Paramodulation-Based Theorem Proving'', Robert Nieuwenhuis and Alberto Rubio, ] I(7), ] Science and ], 2001. | ||
| Line 19: | Line 18: | ||
| ] | ] | ||
| {{mathlogic-stub}} | {{mathlogic-stub}} | ||
| ] | |||
Latest revision as of 06:19, 31 May 2024
The superposition calculus is a calculus for reasoning in 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 clausal logic). Like 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.
Many (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. |