¿Qué es?
Es una regla útil para descartar cláusulas inútiles, y así agilizar la obtención o confimación de la imposibilidad de obtener la contradicción.
Esta regla afirma:
En un conjunto de cláusulas, aquellas que son subsumidas por otras pueden descartarse.
¿Por qué?
Si todos los literales de C1 aparecen en C2, entonces C1 ⊢ C2 (C2 se obtiene por aplicación de la Regla de la introducción de la disyunción a C1). Cualquier cosa que sea demostrable utilizando C2, también se podrá demostrar utilizando C1.
¿Cómo es el proceso de subsumición?
Si se tienen dos cláusulas C1 y C2 en las que todos los literales de C1 también aparecen en C2 se dice que la cláusula C1 subsume la cláusula C2 (o que la cláusula C2 es subsumida por la cláusula C1).
Cuando una cláusula subsume otra, la cláusula subsumida es siempre la más larga (la que contiene más literales).