P1: 
P2: ¬ 
C:
vemos que se puede aplicar a dos cláusulas cualesquiera que compartan un literal con distinto signo. Estas cláusulas le llaman generatrices, y la conclusión, cláusula resultante de la disyunción del resto de literales, resolvente.
En sistema deductivo con resolución todas las sentencias deben estar en forma
clausulada. Si hay n premisas inicialmente en 
0, al ponerlas en forma clausulada
resultarán m > n cláusulas, y la estrategia de control (Apartado 3.7.1) se reduce al
problema de decidir, en cada i, a qué pareja de cláusulas aplicar una regla de
resolución única, la regla de resolución.
En efecto, la propiedad extraordinaria de la regla de resolución es que casi todas las reglas de inferencia se reducen a ella si previamente se escriben las premisas en forma clausulada. Así, para las definidas en el Apartado 3.6.1:
| Regla de inferencia | Resolución |
| modus ponens: | |
| P1: | G1: |
P2:  | G2: ¬ |
| C: | R: |
| modus tollens: | |
| P1: ¬ | G1: ¬ |
| P2: | G2: ¬ |
| C: ¬ | R: ¬ |
| encadenamiento: | |
| P1: | G1: ¬ |
| P2: | G2: ¬ |
| C: | R: ¬ |
Las reglas de inferencia que se justifican por equivalencias son triviales, puesto que dos sentencias equivalentes resultan tener las mismas formas clausuladas. Por ejemplo, en el Apartado 3.6.1 citábamos:
( ( )) 
( ( ))
Como es fácil comprobar (teniendo en cuenta la asociatividad y la conmutatividad de la disyunción), las dos sentencias tienen la misma forma clausulada:
¬ ¬
Como ejemplo, veamos una demostración que en el Apartado 3.6.2 habíamos realizado utilizando sucesivamente la regla de encadenamiento, la derivada de la equivalencia anterior y la de modus ponens.
Las premisas, en su forma original y en forma clausulada son:
| P1: | p q |  | ¬p q |
| P2: | q (¬s r) | | ¬q s r |
| P3: | ¬s | | ¬s |
| C: | p r | | ¬p r |
La demostración se reduce a dos pasos:
| {P1,P2} | | C1 : ¬p s r |
| {C1,P3} | | C : ¬p r |
Decíamos que «casi»
todas las reglas de inferencia se pueden reducir a la de resolución porque hay algunas
triviales que no lo hacen. Por ejemplo, la de introducción de disyunción: dadas las
premisas p y q, la resolución no permite inferir p q, a pesar de que (p 
q)
(p q).
Un sistema deductivo con resolución es, por tanto, consistente, pero no completo
(Apartado 3.7.2). Sin embargo, sí es completo si está basado en refutación.
Veámoslo.
DIT-ETSIT-UPM