Subsumpcja (matematyka)
Z Wikipedii
Subsumpcja (ang. subsumption) to 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 bardzo ważną 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.