Subsumpcja (matematyka)

Szablon:Dopracować Subsumpcja (Szablon:Ang.) – algorytm eliminacji redundantnych klauzul w rezolucji.

Jest oczywiste, ze jeśli mamy klauzule $p(x)$ oraz $p(A),$ gdzie $A$ to jakaś stała, $x$ natomiast to zmienna, nie ma potrzeby trzymać tej drugiej, bo wynika z bardziej ogólnej klauzuli $p(x).$

Subsumpcja jest częścią systemów automatycznego dowodzenia twierdzeń opartych na rezolucji – dzięki niej zamiast mieć bazę twierdzeń w rosnącym stopniu zapełnioną przez twierdzenia szczegółowe, w miarę postępu dowodu mamy w niej twierdzenia bardziej ogólne, które rokują o wiele większe nadzieje.