Unificación

En la sección anterior se ha hecho hincapié en el proceso de la demostración, y para ello no se han considerado las variables que pueden aparecer en los predicados, tal como lo expresa la sintaxis de los programas en lógica.

Se asume que las variables de una cláusula están cuantificadas universalmente, y tienen como alcance a la propia cláusula.

En estos casos el procedimiento de demostración es similar a lo ya visto, salvo que es necesario contemplar la presencia de variables. La resolución se realizará sólo cuando es posible encontrar una instanciación de las variables que hacen iguales los predicados a anular.

Por ejemplo, sea el programa siguiente:

        PADRE ( jorge, diego ) <- .                (1)
        HERMANO ( ricardo, jorge ) <- .            (2)
        TIO(X, Y) <- PADRE(Z, Y), HERMANO(X, Z).   (3)

La tercera cláusula, como se ha dicho, está cuantificada universalmente para las variables X, Y y Z.

Si se considera la invocación:

   <- TIO ( W, diego ).                      (4)

La demostración se realiza de la forma siguiente:

i)

La cláusula (3) está cuantificada universalmente. Por lo tanto es también válida para el caso que la variable Y tenga como valor diego, situación que puede representarse por

   TIO(X, diego) <- PADRE(Z, diego), HERMANO(X, Z)  (5)

ii)

Como las variables tienen por alcance la cláusula donde aparecen, entonces (4) no cambia si se reemplaza W por X. Hecho esto es posible resolver (4) y (5), pues se ha encontrado una instanciación de (3) que lo posibilita. De esta forma se obtiene:

   <- PADRE(Z, diego), HERMANO(X, Z)               (6)

iii)

Se busca ahora resolver (1) con (6) a través del predicado PADRE. Nuevamente es necesario encontrar una instanciación, esta vez en (6), obteniéndose:

   PADRE(jorge, diego), HERMANO(X, jorge)          (7)

iv)

Ahora es posible la resolución buscada, realizándola entre (1) y (7), lo que permite inferir:

   HERMANO(X, jorge)                               (8)

v)

Finalmente, e instanciando X en (8) con ricardo se puede resolver la nueva cláusula con (2), obteniéndose:

        [ ]

Los pasos 1) a 5) constituyen la demostración de la fórmula (4). Resulta claro que al escribir dicha fórmula el usuario no estaba directamente interesado en una prueba, sino que más bien quería conocer quién es TIO de diego. La variable W original fue cambiada por X en el paso 1), y esa variable fue instanciada en el paso 5) para completar la prueba. El valor que le fue asignado, es decir, ricardo, es la respuesta que da el sistema, y que corresponde al interés inicial del usuario.

El problema que se plantea para la regla de resolución es entonces cómo resolver dos predicados que tengan el mismo símbolo predicativo, pero que sus argumentos no coinciden.

El mecanismo que va a permitir resolver dicho problema es el llamado de unificación.

Definición 3.13 (Sustitución)
Una sustitución es un conjunto de asignaciones del tipo:

$$X := t$$

donde $X$ es una variable y $t$ es un término, en el sentido de la definición sintáctica de los programas en lógica. En una sustitución no pueden existir más de una asignación a la misma variable.

Hosted by www.Geocities.ws