Unification

• X = Y X and Y are unified.

• X \= Y X and Y are not unifiable.

• (X?=Y) X and Y are unifiable. It is logically equivalent to: not(not(X$=$Y)).

• X := Y Assigns Y to X. It will cause an error if X is not a free variable at the time when the call is executed.

• X <= Y^17.1 Y matches X. It succeeds if X and Y become identical after some variables in X are substituted with some other terms.