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
gollark: ```Despite their great size and strength, Celestial Dragons are a peaceful breed named for their spectral, starry appearance. Little else is known about them, as they spend the vast majority of their lives partially phased out of the plane of existence through the use of powerful magic. Celestial Dragons are thought to assume their corporeal form only long enough to reproduce or to die; the rest of the time, they resemble living, breathing constellations, impervious to all physical and magical harm.```
gollark: And don't forget celestials.
gollark: Actually, Bolts can do stun, which might help in a fight.
gollark: I suppose they're mostly just checked for grammar, time-matchingness and slight sanity.
gollark: I expect that in most fights the Guardian of Nature would win though.

References
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.