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.