Edició de «Càlcul de superposició»
Anar a la navegació
Anar a la busca
Advertencia: No has iniciat sessió. La teua direcció IP serà visible públicament si realises qualsevol edició. Si inicies sessió o crees un conte, les teues edicions s'atribuiran al teu nom d'usuari, junt en atres beneficis.
Pot desfer-se la modificació. Per favor, revisa la comparació més avall per a assegurar-te que es lo que vols fer; llavors deixa els canvis per a la finalisació de la desfeta de l'edició.
Revisió actual | El teu text | ||
Llínea 1: | Llínea 1: | ||
− | El '''càlcul de superposició''' és un càlcul per a Demostració automàtica de teoremes de la | + | El '''càlcul de superposició''' és un càlcul per a Demostració automàtica de teoremes de la lògica de primer orde. |
− | Es va | + | Es va desenvolupar en la dècada de [[1990]] i combina els conceptes de la resolució de primer orde en la manipulació d'igualtats basades en seqüències ordenades com es desenvolupar en el context de la terminació de Knuth-Bendix. |
− | Pot ser vist com una | + | Pot ser vist com una generalització de qualsevol resolució (lògica equacional) o terminació constant (lògica clausal completa). Com la majoria dels càlculs de primer orde, la superposició tracta de mostrar la insatisfactibilitat d'un conjunt de clàusules de primer orde, és dir, que realitza proves de refutació. |
[[Categoria: Matemàtiques]] | [[Categoria: Matemàtiques]] |