Càlcul de superposició: diferència entre les revisions

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ó.

 

 

[[en:Superposition calculus]]