El fundamento de la refutación es la «ley de reducción al absurdo»
(enunciada en el Apartado 3.4.2 como equivalencia (10)). Si sustituimos 
por P 
C,
donde P = P1 
P2 ... Pn es la conjunción de las premisas y C la conclusión a
comprobar, resulta:
((¬(P C) (
¬)) 
(P C))
o, lo que es lo mismo,
(((P ¬C) ( ¬)) (P C))
es cualquier sentencia. La resolución ( ¬)) da lugar a la llamada cláusula
vacía, 
, que representa la contradicción.
Es decir, P C se satisface para todas las interpretaciones (y, por tanto, C
es una conclusión de P) si y sólo si de la conjunción de P y ¬C resulta una
contradicción.
En el último párrafo de la página anterior plantéabamos una inferencia que era simplemente aplicación de la regla de introducción de disyunción:
P1: p
P2: q
C: p 
q
La negación de la conclusión, ¬(p q) conduce a dos cláusulas: ¬p y ¬q. Es decir,
el conjunto de cláusulas resulta ser: {p,q,¬p,¬q}, y la refutación se obtiene
resolviendo la primera con la tercera o la segunda con la cuarta.
DIT-ETSIT-UPM