4.3.3 Unificación.

El siguiente par de clausulas:

y
no pueden ser resueltas debido a que los argumentos no “embonan”, sin embargo, aplicando sustitución:

,

Obtenemos el siguiente par de clausulas:

y

Otra forma de sustitución más sencilla que la anterior, sería:

, así obtendríamos:

y

Por lo que no sería dificil observar que la sustitución anterior puede descomponerse aún más:

, dando como resultado:

y

MGU. (Most general Unifier). Dado un conjunto de clausulas, un unificador es la sustitución que hace que los átomos contenidos en en conjunto de clausulas sean idénticos. Un MGU es un unificador

tal que cualquier otro unificador
puede ser obtenido para
por otra sustitución
tal que:
.

Conjunto de Discrepancia. Dado que

y
son un par de átomos con los mismos símbolos de predicados. Considerémoslos como una secuencia de simbolos, donde
indica la posición más hacia la izquierda en donde las secuencias de los átomos son diferentes. El par de terminos
empiezan en la posición
de
y
, por lo tanto, es este el que será denominado como “Conjunto de Discrepancia” de los dos átomos.

Algoritmo de Unificación de Robinson.

Entrada: Un par de átomos

y
con los mismos símbolos de predicados.

Salida: Un

para
y
, o bien, que no sean unificables.

Dados: 

     


 y 


.

El Conjunto de Discrepancia inicial sería:

. Como uno de los terminos es una variable:
, entonces:

.

El siguiente conjunto de discrepancia es:

, y
entonces:

.

El tercer conjunto de discrepancia es:

, y
entonces:

.
, los átomos son unificables y el MGU es:
<=Regresar Tema 4.3.2 Sustitucion en Logica de Primer Orden
=>Siguiente Tema: 4.3.4 Resolucion General
Regresar al TEMARIO: Matematicas Para Maestria
Alma Isabel Martinez Alvarez Tema de Unificacion

Búsqueda personalizada

GFDL