Untitled

Unifikacja termu
T1: f(X,a(b,c))
T2: f(Z,a(Z,c))
Termy mają tę samą liczbę argumentów. Możliwa jest unifikacja
T_11: X(zmienna)
T_21: Z(zmienna)
Podstawiam t1: X = Z
T1t1: f(X,a(b,c))
T2t1: f(X,a(X,c))
T_12: a(b,c) (term złożony)
T_22: a(X,c) (term złożony)
Mamy dwa termy złożone - porównujemy ich argumenty
T_121: b (stała)
T_221: X (zmienna)
Podstawiam t2: X=b
T1t1t2: f(X,a(X,c))
T2t1t2: f(X,a(X,c))

Wynik: t1t2 = {X = Z, Z=b}

Przykład 2
T1: fu(a,X,f(g(Y))) 
T2: fu(Y,f(Z),f(Z))
Liczba argumentów taka sama - możliwa unifikacja
T_11: a (stała)
T_21: Y (zmienna)
Podstawiam t1: Y = a
T1t1: f(Y,X,f(g(Y)))
T2t1: f(Y,f(Z),f(Z))
T_12: f(g(Y)) (term złożony)
T_22: f(Z) (term złożony)
Termy złożone, porównuje argumenty
T_121: g(Y) (term złożony)
T_221: Z (zmienna)
Podstawiam t2: Z = g(Y)
T1t1t2: f(Y,X,f(Z))
T2t1t2: f(Y,f(Z),f(Z))
Podstawiam t3: X = f(Z)
T1t1t2t3: f(Y,X,X)
T2t1t2t3: f(Y,X,X)
MGU(T1,T2) = t1t2t3 = { X=f(g(a)) ,Z=g(a),Y = a }