Ejemplos

1. Dadas las expresiones
   PADRE ( Z , diego) y PADRE ( jorge , diego)
   la sustitución $\theta$ = { Z := jorge } es un unificador de las mismas.

2. Dadas las expresiones
   TIO ( X , diego) y TIO ( W , diego)
   la sustitución $\theta$ = { X := W } es un unificador de las mismas. La sustitución $\theta$ = { W := X } también es un unificador. La sustitución $\theta$ = { X := guillermo, W := guillermo } también es un unificador.

3. Dadas las expresiones
   $$Q( q(X,Y), X, h(4)) \quad \mathrm{y} \quad Q( q(3,Z), W, h(Z))$$
   la sustitución $\theta = \{X:= 3, Z:= 4, W:= 3, Y:= 4\}$ es un unificador de las mismas.

4. Sean las expresiones
   R ( [X . Y] ) y R( [[a.[b.[]]].[c.[d.[]]]] )
   Debe recordarse que el término [[a.[b.[]]].[c.[d.[]]]] corresponde a la lista $((a\ b)\ c\ d)$.

   La sustitución $\theta$ = { X:= [a.[b.[]]], Y := [c.[d.[]]]} es un unificador de las mismas.

   En notación de listas: $\theta = \{ X:= (a\ b), Y:= (c\ d)\}$.

   Si se utiliza la notación de listas, lo que frecuentemente resulta muy cómodo, la expresión [X.Y] representa una lista, donde, según otros lenguajes, X corresponde al «CAR», «head» o «cabeza» de la lista; Y corresponde al «CDR», «tail», o «resto» de la misma; «.» corresponde al constructor «CONS».

5. Dadas las expresiones
   R ( [X . Y] ) y R( [] )
   No existe un unificador para ambas.

De la definición de unificador y de los ejemplos presentados surge que existen expresiones para las cuales no existe un unificador, mientras que en otros casos es posible encontrar más de un unificador.

Para el procedimiento de demostración, y en caso de existir más de un unificador entre dos predicados que permita aplicar la regla de resolución, va a interesar aquel que sea más general, en el sentido que necesite asignaciones menos específicas de términos a variables. En el ejemplo 2. visto anteriormente, los dos primeros unificadores, que en definitiva son el mismo --a menos de un renombramiento-- son más generales que el tercero.

Definición 3.16 (Unificador más general)
Dadas dos sustituciones $\theta_1$ y $\theta_2$ y que ambas son unificadores de las expresiones $E_1$ y $E_2$, se dice que $\theta_1$ es más general que $\theta_2$ si existe una sustitución $\theta_3$ tal que:

$$E_1 \theta_1 \theta_3 = E_2 \theta_2$$

La relación «más general que» es un preorden. Al mínimo del preorden «más general que» se le llama unificador más general.

Existen múltiples propuestas de algoritmos para calcular el unificador más general, y ello se debe a que dicho algoritmo tiene una importancia capital en el proceso de la demostración.

Hosted by www.Geocities.ws