Lógica Computacional
Nota 11. Algoritmos de unificación. Regla de resolución y precedimiento de resolución general

1 Introducción

La diferencia entre resolución en lógica de predicados y resolución en lógica proposicional es la unificación. En lógica proposicional, se aplicaba la regla de resolución a dos cláusulas si contenían literales complementarias, i.e., la literal positiva era idéntica a la literal negativa, omitiendo el símbolo de negación. La misma idea subyace en la resolución en lógica de predicados, excepto que el criterio para clasificar literales complementarias es más relajado. La literal positiva no tiene que ser idéntica a la literal negativa, omitiendo el símbolo de negación; es suficiente con que las dos literales puedan se idénticas al sustituir sus variables.

La unificación es el proceso por el que se determina si dos expresiones pueden ser unificadas, i.e., si pueden ser idénticas al sustituir apropiadamente sus variables. Determinar esto es una parte esencial de la resolución en lógica de predicados.

1.1 Ideas previas

Definición 1.1.

Considere los siguientes conceptos:

• Un cláusula es un conjunto de literales.

• Un cláusula es considerada implícitamente como una disyunción de sus literales.

• Una cláusula unitaria consiste exactamente de una única literal.

• El conjunto vacío de literales es la cláusula vacía, denotada como $\mathrm{\square }$.

• Una fórmula en forma clausular es un conjunto de cláusulas.

• Una fórmula en forma clausular es considerada implícitamente como una conjunción de sus cláusulas.

• La fórmula que es el conjunto vacío de cláusulas se denota como $\mathrm{\varnothing }$.

Definición 1.2.

Sean:

dos sustituciones efectuadas simultáneamente, y sean $X=\{x_1,\mathrm{\dots },x_n\}$ y $Y=\{y_1,\mathrm{\dots },y_k\}$ los conjuntos de las variables que son sustituidas por $\theta$ y $\sigma$, respectivamente. Así $\theta \sigma$, la composición de $\theta$ y $\sigma$, es la sustitución:

$$\theta \sigma =[x_i:=t_i\sigma ,y_j:=s_j]\text{con }{x}_i\in X\text{, }{x}_i\ne t_i\sigma \text{, }{y}_j\in Y\text{ y }{y}_j\notin X$$

Ejemplo 1.3.

Sea

Entonces,

$$\theta \sigma =[x:=f(g(a)),y:=f(a),u:=z,v:=f(f(a))].$$

A partir de esta composición se puede obtener la sustitución $E(\theta \sigma )$ como:

$$E(\theta \sigma )=P(z,f(f(a)),f(g(a)),f(a),z).$$

Bien se pudo haber realizado la sustitución en dos partes:

2 Unificación

Ejemplo 2.1.

Las dos literales $P(f(x),g(y))$ y $\neg P(f(f(a)),g(z))$ no colisionan. Sin embargo, al aplicarles la sustitución

$${\theta }_1=[x:=f(a),y:=f(g(a)),z:=f(g(a))]$$

obtenemos literales cerradas que colisionan: $P(f(f(a)),g(f(g(a))))$ y $\neg P(f(f(a)),g(f(g(a))))$.

La siguiente sustitución es más sencilla:

$${\theta }_2=[x:=f(a),y:=a,z:=a]$$

al aplicarse también genera un par de literales que colisionan: $P(f(f(a)),g(a))$ y $\neg P(f(f(a)),g(a))$.

Considere ahora la siguiente sustitución:

$$\mu =[x:=f(a),z:=y]$$

las literales que resultan son: $P(f(f(a)),g(y))$ y $\neg P(f(f(a)),g(y))$. Cualquier sustitución de $y$ por un término cerrado aplicada a estas dos literales producirá literales cerradas que colisionan.

Al encontrar la sustitución más sencilla que ocasione que dos literales colisionen, el resolvente será el resultado más general obtenido por la regla de resolución y será más propenso a colisionar con otra cláusula después de una sustitución apropiada.

Definición 2.2.

Sea $U=\{A_1,\mathrm{\dots },A_n\}$ un conjunto de átomos. Un unificador $\theta$ es una sustitución tal que:

$$A_1\theta =\mathrm{\cdots }=A_n\theta .$$

Un unificador más general (umg) para $U$ es un unificador $\mu$ tal que cualquier unificador $\theta$ de $U$ puede ser expresado como:

$$\theta =\mu \lambda$$

para alguna sustitución $\lambda$.

3 Algoritmo de unificación por Martelli y Montanari

Si dos átomos son unificables, entonces comparten el mismo símbolo de predicado con la misma paridad. La unificación de átomos se entiende como la unificación de sus argumentos, es decir, la unificación de un conjunto de términos. El conjunto de términos a ser unificados será escrito como un conjunto de ecuaciones de términos.

Ejemplo 3.1

La unificación de $\{P(f(x),g(y)),P(f(f(a)),g(z))\}$ se expresa como un conjunto de ecuaciones de términos:

Definición 3.1.

Un conjunto de ecuaciones de términos está en forma de solución syss:

• Todas las ecuaciones son de la forma $x_i=t_i$ donde $x_i$ es una variable.

• Si la variable $x_i$ figura en el lado izquierdo de una ecuación, no figura en alguna otra ecuación.

Un conjunto de ecuaciones en forma de solución define la sustitución:

$$[x_1:=t_1,\mathrm{\dots },x_n:=t_n]$$

Algoritmo (Algoritmo de unificación de Martelli y Montanari)

Input: Un conjunto de ecuaciones de términos.

Output: Un conjunto de ecuaciones en forma de solución o reportar no unificable.

Ejecutar las siguientes transformaciones sobre el conjunto de ecuaciones mientras alguna de ellas sea aplicable:

1. Transformar $t=x$, donde $t$ no es una variable, en $x=t$.

2. Eliminar la ecuación $x=x$.

3. Sea $t=s$ una ecuación donde $t,s$ no son variables,

   • Si el símbolo de función más externo de $t$ y $s$ no es el mismo, el algoritmo termina reportando no unificable.

   • Si el símbolo de función más externo de $t$ y $s$ sí es el mismo, pero difiere en aridad, el algoritmo termina reportando no unificable.

   • De otro modo, reemplazar la ecuación $f(t_1,\mathrm{\dots },t_k)=f(s_1,\mathrm{\dots },s_k)$ por las $k$ ecuaciones $t_1=s_1,\mathrm{\dots },t_k=s_k$.

4. Sea $x=t$ una ecuación tal que $x$ figura en otro lugar dentro del conjunto.

   • Si $x$ figura en $t$, y el término $t$ no es la variable $x$ misma, el algoritmo termina reportando no unificable.

   • De otro modo, transformar el conjunto al reemplazar todas las presencias de $x$ por $t$ en las otras ecuaciones donde $x$ figura.

Los algoritmos de unificación pueden ser bastante ineficientes por la verificación de la condición descrita en la regla 4, llamada verificación de presencias.

En la aplicación de la unificación en la programación lógica, la verificación de presencias se ignora y se toma el riesgo de una sustitución ilegal.

Ejemplo 3.2.

Considere el siguiente conjunto con dos ecuaciones de términos:

Aplicamos la regla 1 a la primera ecuación y la regla 3 a la segunda ecuación:

Aplicamos la regla 4 a la segunda ecuación reemplazando la presencias de $x$ por $g(z)$ en las demás ecuaciones:

Aplicamos la regla 3 a la primer ecuación:

Aplicamos la regla 4 a la última ecuación reemplazando $y$ por $z$ en la primera ecuación; esto resulta en la ecuación $z=z$ la cual eliminamos usando la regla 2:

Finalmente, transformamos la segunda ecuación mediante la regla 1:

Así terminamos exitosamente el algoritmo, y afirmamos que

$$\mu =[x:=g(z),w:=h(g(z)),y:=z]$$

es un unificador más general del conjunto original de ecuaciones. Podemos verificar también que el unificador:

$$\theta =[x:=g(h(b)),w:=h(g(h(b))),y:=h(b),z:=h(b)]$$

puede expresarse como $\theta =\mu [z:=h(b)]$.

Ejercicios 3.3.

1. Ejecute el algoritmo de unificación de Martelli y Montanari para encontrar el umg, si es que existe, de los siguientes pares de átomos:

   • $P(x,x)$ y $P(f(y),z)$.

   • $P(x,x)$ y $P(f(y),y)$.

   • $P(f(x,y),g(z,z))$ y $P(f(f(w,z),v),w)$.

   • $P(x,y)$ y $P(f(z),x)$.

2. Resolver el conjunto de ecuaciones de término siguiente mediante el algoritmo de Martelli y Montanari.

   $$x=g(y),x=g(z),h(x)=w,y=z.$$

4 Algoritmo de unificación de Robinson

Definición 4.1.

Sean $A$ y $A^{\prime }$ dos átomos con el mismo símbolo de predicado y misma aridad, considere a cada uno como una secuencia de símbolos. Sea $k$ la posición más a la izquierda en la que las secuencias difieren. El par de términos $\{t,t^{\prime }\}$, que comienzan en la posición $k$ de $A$ y $A^{\prime }$, es el conjunto de desacuerdo de los dos átomos.

Algoritmo (Algoritmo de unificación de Robinson)

Input: Dos átomos $A$ y $A^{\prime }$ con el mismo símbolo de predicado y misma aridad.

Output: Un unificador más general para $A$ y $A^{\prime }$ o reportar no unificable.

Inicializar el algoritmo al definir $A_0=A$ y $A_0^{\prime }=A^{\prime }$. Ejecutar sucesivamente la siguiente acción:

• Sea $\{t,t^{\prime }\}$ el conjunto de desacuerdo de $A_i$ y $A_i^{\prime }$. Si un término es una variable $x_{i+1}$ y el otro es un término $t_{i+1}$ tal que $x_{i+1}$ no figura en $t_{i+1}$, entonces definimos ${\sigma }_{i+1}=[x_{i+1}:=t_{i+1}]$, y generamos los átomos $A_{i+1}=A_i{\sigma }_{i+1}$ y $A_{i+1}^{\prime }=A_i^{\prime }{\sigma }_{i+1}$ para una nueva iteración del algoritmo.

Si no es posible ejecutar esta acción (debido a que ambos elementos $t$ y $t^{\prime }$ no son variables; o debido a que un término, digamos $t$, es una variable y ésta figura en el otro término, $t^{\prime }$), los átomos no son unificables. Si después de ejecutar esta acción $A_n=A_n^{\prime }$, entonces $A,A^{\prime }$ son unificables y el umg es $\mu ={\sigma }_1\mathrm{\cdots }{\sigma }_n$.

Ejemplo 4.2.

Considere el par de átomos:

$$A=P(g(y),f(x,h(x),y)),A^{\prime }=P(x,f(g(z),w,z)).$$

Comenzamos definiendo $A_0=A$ y $A_0^{\prime }=A^{\prime }$. El conjunto de desacuerdo inicial es $\{x,g(y)\}$. Un término es la variable $x$ que no está presente en el otro término, así ${\sigma }_1=[x:=g(y)]$, y:

El conjunto de desacuerdo de $A_1$ y $A_1^{\prime }$ es $\{y,z\}$ así ${\sigma }_2=[y:=z]$, y:

El conjunto de desacuerdo de $A_2$ y $A_2^{\prime }$ es $\{w,h(g(z))\}$ así ${\sigma }_3=[w:=h(g(z))]$, y:

Como $A_3=A_3^{\prime }$, los átomos son unificables y un umg es:

$$\mu ={\sigma }_1{\sigma }_2{\sigma }_3=[x:=g(z),y:=z,w:=h(g(z))].$$

Ejercicios 4.3.

Ejecute el algoritmo de unificación de Robinson para encontrar el umg, si es que existe, de los siguientes conjuntos de literales:

• $\{P(a,x,f(g(y))),P(z,f(z),f(u))\}$.

• $\{P(a,x,h(g(z))),P(z,h(y),h(y))\}$.

• $\{Q(a,x,f(x)),Q(a,y,y)\}$.

• $\{Q(x,y,z),Q(u,h(v,v),u)\}$.

• $\{Q(f(x,g(x,a)),z),Q(y,h(x)),Q(f(b,w),z)\}$.

5 Resolución general

Definición 5.1.

Sea $L=\{l_1,\mathrm{\dots },l_n\}$ un conjunto de literales. Entonces $L^c=\{l_1^c,\mathrm{\dots },l_n^c\}$, es decir, $L^c$ es el conjunto de literales complementarias de las que están en $L$.

Definición 5.2.

(Regla de resolución general) Sean $C_1$ y $C_2$ cláusulas sin variables en común. Sean $L_1=\{l_1^1,\mathrm{\dots },l_{n_1}^1\}\subseteq C_1$ y $L_2=\{l_1^2,\mathrm{\dots },l_{n_2}^2\}\subseteq C_2$ dos subconjuntos de literales tales que $L_1$ y $L_2^c$ se unifican por un umg $\sigma$. $C_1$ y $C_2$ se conocen como cláusulas de colisión y colisionan en el conjunto de literales $L_1$ y $L_2$. $C$, el resolvente de $C_1$ y $C_2$, es la cláusula:

$$Res(C_1,C_2)=(C_1\sigma -L_1\sigma )\cup (C_2\sigma -L_2\sigma ).$$

Ejemplo 5.3.

Sean $C_1=\{P(f(x),g(y)),Q(x,y)\}$ y $C_2=\{\neg P(f(f(a)),g(z)),Q(f(a),z)\}$ dos cláusulas, un umg para $L_1=\{P(f(x),g(y))\}$ y $L_2^c=\{P(f(f(a)),g(z))\}$ es $[x:=f(a),y:=z]$. El resolvente para las cláusulas $C_1$ y $C_2$ es

$$\{Q(f(a),z),Q(f(a),z)\}=\{Q(f(a),z)\}$$

Las cláusulas son conjuntos de literales, así que cuando tomamos la unión de las cláusulas en la regla de resolución, literales idénticas se colapsarán; esto se llama factorización.

La regla de resolución general requiere en general que las cláusulas de colisión no tengan variables en común. Esto se logra mediante un proceso que se conoce como estandarización por partes: renombramos todas las variables en una de las cláusulas antes de ser usada por la regla de resolución. Todas las variables en una cláusula están implícitamente cuantificadas universalmente así que el renombre no cambia su satisfacibilidad.

Ejemplo 5.4.

Sean $C_1=\{P(x),P(y)\}$ y $C_2=\{\neg P(x),\neg P(y)\}$ dos cláusulas. Aplicando estandarización por partes tenemos que $C_2^{{}^{\prime }}=\{\neg P(x^{\prime }),\neg P(y^{\prime })\}$. Sea $L_1=\{P(x),P(y)\}$ y $L_2^c=\{P(x^{\prime }),P(y^{\prime })\}$; estos conjuntos tienen un umg $\sigma =[y:=x,x^{\prime }:=x,y^{\prime }:=x]$. La regla de resolución opera del siguiente modo:

Algoritmo (Procedimiento de Resolución General)

Input: Un conjunto de cláusulas $S$.

Output: Si el algoritmo termina, reporta que el conjunto de cláusulas es satisfacible o insatisfacible.

Sea $S_0=S$. Escoja dos cláusulas de colisión $C_1,C_2\in S_i$ y sea $C=Res(C_1,C_2)$. Si $C=\mathrm{\square }$, el algoritmo termina y reporta que $S$ es insatisfacible. De otro modo, construir $S_{i+1}=S_i\cup \{C\}$. Si $S_{i+1}=S_i$ para todos los posibles pares de cláusulas de colisión, el algoritmo termina y reporta $S$ es satisfacible.

Aunque un conjunto de cláusulas insatisfacible producirá eventualmente $\mathrm{\square }$ con una adecuada ejecución sistemática del procedimiento, la existencia de modelos infinitos significa que el procedimiento de resolución sobre un conjunto de cláusulas satisfacible puede nunca terminar, así que el procedimiento de resolución general no es un procedimiento de decisión.

Ejemplo 5.5.

Las líneas de la 1 a la 7 contienen un conjunto de cláusulas inicial. La refutación por resolución a partir de la línea 8 muestra que el conjunto de cláusulas inicial es insatisfacible. Cada linea contiene el resolvente, el unificador más general y los números con las cláusulas padre.

Ejercicios 5.6.

1. Determine si los siguientes conjuntos de cláusulas son insatisfacibles.

   • $\{\{P(a,b),Q(a,c)\},\{\neg P(x,y),R(x)\},\{\neg Q(x,y),R(x)\},\{\neg R(z)\}\}$.

   • $\{\{\neg C(x),P(f(x))\},\{\neg C(x),A(x,f(x))\},\{C(a)\},\{\neg P(w),\neg A(a,w)\}\}$.

   • $\{\{\neg P(x,y),P(y,x)\},\{\neg P(x,y),\neg P(y,z),P(x,z)\},\{P(x,f(x))\},\{\neg P(x,x)\}\}$.

   • $\{\{\neg P(x,y),Q(x,y,f(x,y))\},\{R(y,z),\neg Q(a,y,z))\},\{P(x,g(x)),Q(x,g(x),z)\},\{\neg R(x,y),\neg Q(x,w,z)\}\}$

2. Mediante resolución determine si el siguiente argumento es correcto o no.

   $$\{\neg \exists x\left((V(x)\vee P(x)\wedge \neg M(x))\right),\forall x\left(R(x)\wedge \neg A(x)\to V(x)\vee P(x)\right)\}\vDash \exists x\left(R(x)\wedge \neg A(x)\right)\to \exists yM(y)$$

6 El método de resolución general el correcto y completo

Teorema 6.1 (La resolución es correcta).

Sea $S$ un conjunto de cláusulas. Si al aplicar el procedimiento de resolución se obtiene la cláusula vacía $\mathrm{\square }$, entonces $S$ es insatisfacible.

Teorema 6.2 (La resolución es completa).

Si un conjunto de cláusulas es insatisfacible, la cláusula vacía $\mathrm{\square }$ puede obtenerse mediante el procedimiento de resolución.