La regla de resolución que ya hemos introducido en el Apartado 3.6.1 es importante para la mecanización de procesos deductivos, porque resume muchos esquemas de inferencia clásicos. De hecho, sólo con ella pueden diseñarse sistemas deductivos consistentes y completos. Se aplica esta regla a sentencias que tienen que estar escritas de una forma especial, llamada «forma clausulada» . Veamos primero qué forma es ésta, luego cómo para toda sentencia se puede encontrar una sentencia equivalente en forma clausulada y, finalmente, cómo se aplica la regla de resolución.
DIT-ETSIT-UPM