Superposition calculus (original) (raw)
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ó.
| Property | Value |
|---|---|
| dbo: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) |
| dbo:wikiPageExternalLink | http://pubman.mpdl.mpg.de/pubman/item/escidoc:1834970/component/escidoc:1857487/MPI-I-91-208.pdf https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/waldmeister/ |
| dbo:wikiPageID | 2648614 (xsd:integer) |
| dbo:wikiPageLength | 1899 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1111958311 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:SPASS_theorem_prover dbr:Clauses dbr:Elsevier dbr:MIT_Press dbc:Logical_calculi dbr:Automated_theorem_proving dbr:E_equational_theorem_prover dbr:First-order_logic dbr:Formal_system dbr:Handbook_of_Automated_Reasoning dbr:Harald_Ganzinger dbr:First-order_resolution dbc:Mathematical_logic dbr:Automated_theorem_prover dbr:Knuth–Bendix_completion_algorithm dbr:Unsatisfiable dbr:Vampire_theorem_prover dbr:Refutation dbr:Waldmeister_theorem_prover |
| dbp:wikiPageUsesTemplate | dbt:As_of dbt:Mathlogic-stub |
| dct:subject | dbc:Logical_calculi dbc:Mathematical_logic |
| 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) |
| rdfs:label | Càlcul de superposició (ca) Superposition calculus (en) |
| owl:sameAs | freebase:Superposition calculus wikidata:Superposition calculus dbpedia-ca:Superposition calculus https://global.dbpedia.org/id/4vRYA |
| prov:wasDerivedFrom | wikipedia-en:Superposition_calculus?oldid=1111958311&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Superposition_calculus |
| is dbo:wikiPageDisambiguates of | dbr:Superposition |
| is dbo:wikiPageWikiLink of | dbr:Vampire_(theorem_prover) dbr:E_(theorem_prover) dbr:Otter_(theorem_prover) dbr:SPASS dbr:Completeness_(logic) dbr:Superposition dbr:Automated_theorem_proving dbr:Harald_Ganzinger |
| is foaf:primaryTopic of | wikipedia-en:Superposition_calculus |