Càlcul de superposició

De Viquipèdia
Dreceres ràpides: navegació, cerca

El càlcul de superposició és un càlcul per a Demostració automàtica de teoremes 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 terminació de Knuth-Bendix. 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ó.