Unificación

Definición

La unificación busca una sustitución $\theta$ que haga sintácticamente iguales dos términos o átomos de primer orden:

$Subst(\theta ,p)=Subst(\theta ,q).$

Cuando existe, interesa el unificador más general (UMG): uno que impone solo las igualdades necesarias y del cual pueden obtenerse unificadores más específicos mediante sustituciones adicionales.

Formalmente, $\theta$ unifica $p$ y $q$ si $p\theta =q\theta$. Un UMG es más general que cualquier otro unificador: para cada unificador $\sigma$ existe una sustitución $\delta$ tal que $\sigma =\theta \delta$ (salvo renombramiento de variables). Para la notación y aplicación de mapeos, véase sustitución lógica.

Ejemplo mínimo

$Humano(x)\text{y}Humano(S\acute{o}crates)$

se unifican con:

$\theta =\{x/S\acute{o}crates\}.$

También:

$Loves(G(x),x)\text{y}Loves(u,v)$

se unifican con $\theta =\{u/G(x),v/x\}$.

Casos donde falla

• Predicados distintos: $Gato(x)$ y $Perro(x)$.
• Distinta aridad: $P(x)$ y $P(x,y)$.
• Constantes incompatibles: $P(a)$ y $P(b)$, si $a\ne b$.
• Comprobación de ocurrencia: $x$ no puede sustituirse por un término que ya contiene a $x$, como $f(x)$, porque produciría un término infinito.

Papel en resolución

En resolución de primer orden, la unificación permite tratar como complementarios literales que no son idénticos al inicio. Después de calcular $\theta$, la sustitución se aplica a todos los literales restantes del resolvente.

Antes de unificar cláusulas diferentes se estandarizan aparte sus variables para evitar dependencias accidentales por reutilizar nombres como $x$ o $y$.

flowchart TD
  A[Elegir literales complementarios] --> B[Comparar predicado y aridad]
  B --> C{Términos compatibles?}
  C -- No --> D[No hay unificador]
  C -- Sí --> E[Construir sustitución más general]
  E --> F{Pasa comprobación de ocurrencia?}
  F -- No --> D
  F -- Sí --> G[Aplicar θ a toda la cláusula restante]
  G --> H[Obtener resolvente]

Un procedimiento de unificación descompone ecuaciones entre términos: elimina ecuaciones idénticas, descompone funciones con el mismo símbolo y aridad, orienta una ecuación con variable al lado izquierdo y sustituye esa variable en el resto. Falla ante símbolos incompatibles o si la variable aparece dentro del término que se le asignaría (comprobación de ocurrencia). Esta última condición evita soluciones infinitas como $x=f(x)$ en la sintaxis finita ordinaria.

Procedencia y referencias

• Clase: Inferencia en lógica de primer orden, diapositiva 8.
• Russell, S. J. y Norvig, P. (2020). Artificial Intelligence: A Modern Approach (4.ª ed.), §9.2; sitio oficial.
• Genesereth, M. R., Introduction to Logic, unificación y resolución.