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.
Attributes | Values |
---|
rdfs:label
| - Càlcul de superposició (ca)
- Superposition calculus (en)
|
rdfs:comment
| - El càlcul de superposició és un càlcul per a de la lògica equacional de primer ordre. Es va desenvolupar a la dècada de 1990 i combina els conceptes de la resolució de primer ordre amb la manipulació d'igualtats basades en sequencies ordenades com es desenvolupa en el context de la . Pot ser vist com una generalització de qualsevol resolució (a la lògica equacional) o terminació constant (a la lògica clausal completa). Com la majoria dels càlculs de primer ordre, la superposició tracta de mostrar la insatisfacibilitat d'un conjunt de clàusules de primer ordre, és a dir, que realitza proves de refutació. (ca)
- 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. (en)
|
dcterms:subject
| |
Wikipage page ID
| |
Wikipage revision ID
| |
Link from a Wikipage to another Wikipage
| |
Link from a Wikipage to an external page
| |
sameAs
| |
dbp:wikiPageUsesTemplate
| |
has abstract
| - El càlcul de superposició és un càlcul per a de la lògica equacional de primer ordre. Es va desenvolupar a la dècada de 1990 i combina els conceptes de la resolució de primer ordre amb la manipulació d'igualtats basades en sequencies ordenades com es desenvolupa en el context de la . Pot ser vist com una generalització de qualsevol resolució (a la lògica equacional) o terminació constant (a la lògica clausal completa). Com la majoria dels càlculs de primer ordre, la superposició tracta de mostrar la insatisfacibilitat d'un conjunt de clàusules de primer ordre, és a dir, que realitza proves de refutació. (ca)
- 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. (en)
|
prov:wasDerivedFrom
| |
page length (characters) of wiki page
| |
foaf:isPrimaryTopicOf
| |
is Link from a Wikipage to another Wikipage
of | |
is Wikipage disambiguates
of | |
is foaf:primaryTopic
of | |