siguiente anterior arriba atrasadelante (solo si previamente se ha ido
atras)

4.8.4. Refutación

Como en lógica de proposiciones (Apartado 3.8.4), la refutación consiste en añadir la conclusión negada a las premisas; si se demuestra la cláusula vacía se ha refutado la conclusión negada, y, por tanto, se ha demostrado la conclusión.

Ahora la conclusión buscada puede contener variables, y en el proceso de demostración se pueden obtener los valores concretos con los que estas variables pueden unificarse. Así, en el último ejemplo de la página anterior podríamos poner como conclusión «q(y,z)» , es decir:

P1: ¬p(A,x)  \/ q(x,B)

P2: p(A,C)

P3: ¬q(y,z)

Y la refutación se obtiene con la unificación {C/x,C/y,B/z}. Si añadimos a las premisas la cláusula p(A,D) se obtiene otra refutación con la unificación {D/x,D/y,B/z}

El hecho de añadir la conclusión negada a las premisas puede interpretarse como una consulta. Veámoslo con un ejemplo más concreto: el del mundo de los bloques. Supongamos que la conceptuación consiste en la relación «Sobre» definida intensionalmente por la situación de la Figura 1.6 y la relación «Más-arriba-que» definida intensionalmente, y representada por la sentencia:

( A x)( A y)((sobre(x,y)  \/ ( E z)(sobre(x,z)  /\ maq(z,y))) ==> maq(x,y))

Pasando todo a cláusulas resulta:

P1: sobre(A,B)

P2: sobre(B,C)

P3: sobre(D,E)

P4: ¬sobre(x1,y1)  \/ maq(x1,y1)

P5: ¬sobre(x2,z)  \/ ¬sobre(z,y2)  \/ maq(x2,y2)

La conclusión «maq(x,y)» representa a la consulta «¿qué bloques están más arriba que otros?» .

Añadiendo la conclusión negada a las premisas tenemos una nueva cláusula:

P6: ¬maq(x,y)

Veamos las resoluciones que pueden hacerse:

Generatrices Resolvente Unificaciones




{P4,P6} ~>R1: ¬sobre(x,y) {x/x1,y/y1}
{P1,R1} ~>P {A/x,B/y}
{P2,R1} ~>P {B/x,C/y}
{P3,R1} ~>P {D/x,E/y}
{P5,P6} ~>R2: ¬sobre(x,z)  \/ ¬sobre(z,y){x/x2,y/y2}
{P1,R2} ~>R3: ¬sobre(B,y) {A/x,B/z}
{P2,R3} ~>P {C/z}


siguiente
anterior arriba atrasadelante (sólo si previamente se ha ido atras)


algunos derechos reservados DIT-ETSIT-UPM
Portada