Misplaced Pages

Superposition calculus: Difference between revisions

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Browse history interactively← Previous editContent deleted Content addedVisualWikitext
Revision as of 22:24, 12 July 2010 edit67.172.21.121 (talk) →Implementations← Previous edit Latest revision as of 06:19, 31 May 2024 edit undoDavid Eppstein (talk | contribs)Autopatrolled, Administrators225,939 edits rewrite to avoid dated stmt 
(17 intermediate revisions by 15 users not shown)
Line 1: Line 1:
The '''superposition calculus''' is a calculus for ] in equational ]. It has been 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 clausal logic). As most first-order calculi, superposition tries to show the ''unsatisfiability'' of a set of first-order ], i.e. it performs proofs by ]. Superposition is refutation-complete — given unlimited resources and a ''fair'' derivation strategy, every ] clause set can eventually be proved to be unsatisfiable. 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.


As of 2007, most of the (state-of-the-art) ]s for ] are based on superposition (e.g. the ]), although only a few implement the pure calculus. 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:
* ] * ]
* ] * ]
* ] * ]
* ] 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.


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

Stub icon

This mathematical logic-related article is a stub. You can help Misplaced Pages by expanding it.

Categories: