Ci, którzy programują w Prologu, wiedzą, co to jest term. Term, to wyrażenie składające się ze stałych, zmiennych i wyrażeń typu f(x1, x2, ... ) gdzie f jest nazwą funktora (symbolem) a x1, x2, ... też są termami. Jeśli oznaczymy zmienne nazwami zaczynającymi się od dużych liter (X, Y, Z itp) a stałe innymi nazwami , liczbami itp, term może wyglądać tak:
f ala( f, f(X, Y, 10), X) ala( 0 )i tak dalej. W skrócie mówiąc - unifikacja termów, to takie dopasowanie wartości zmiennych (wartości zmiennych też mają być termami) aby dwa unifikowane termy uzyskały tę samą wartość. Unifikacja może się nie udać, zmienne nie są wtedy zmieniane (mówi się też - ukonkretnione) Jeśli oznaczymy symbolem == operację unifikacji, możemy napisać:
f( X, 1 ) == f( 2, Y ) -> zmienna X zyskuje wartość 2, Y wartość 1 f( X, g( Y, 0 ), Y ) == f( 1, Z, g( 2 )) -> zmienna X zyskuje wartość 1, Y wartość g(2) a Z wartość g(g(2), 0) f( X, g( 1 )) == f( 0, 2 ) -> unifikacja zawodzi, zmienne pozostają wolne.
