Subsumpcja (ang. subsumption) – algorytm eliminacji redundantnych klauzul w rezolucji.

Jest oczywiste, ze jeśli mamy klauzule ${\displaystyle p(x)}$ oraz ${\displaystyle p(A),}$ gdzie ${\displaystyle A}$ to jakaś stała, ${\displaystyle x}$ natomiast to zmienna, nie ma potrzeby trzymać tej drugiej, bo wynika z bardziej ogólnej klauzuli ${\displaystyle 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.