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:
(x)(y)((sobre(x,y) (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} | {A/x,B/y} | ||
{P2,R1} | {B/x,C/y} | ||
{P3,R1} | {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} | {C/z} | ||