Càlcul de superposició
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ó.
Bibliografia
modifica- Rewrite-Based Equational Theorem Proving with Selection and Simplification, Leo Bachmair and Harald Ganzinger, Journal of Logic and Computation 3(4), 1994.
- Paramodulation-Based Theorem Proving, Robert Nieuwenhuis and Alberto Rubio, Handbook of Automated Reasoning I(7), Elsevier Science and MIT Press, 2001.