Superposition calculus

The superposition calculus is a calculus for reasoning in equational first-order 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). 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, from any unsatisfiable clause set a contradiction will eventually be derived.

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 (official web page)

gollark: Which apparently entirely broke at some point in the last few weeks.

gollark: Now I need to fix Reminding 2™.

gollark: Okay, bridging appears to be fully functional again.

gollark: Great!

gollark: Oh, you mean the BAD LyricLy?

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 article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.