Unification. Input: a list t_1 = t'_1, ... , t_n = t'_n of equations between terms. Output: NOUNIFIER or a unifying substitution (see p. 436). Algorithm: transform the equations according to the following rules: f(a_1,...,a_k) = f(b_1,...,b_k) => a_1 = b_1, ... , a_k = b_k X = X => (delete X = X) f(a_1,...,a_k) = X => X = f(a_1,...,a_k) (*) X = t, ... , s = s' , ... => X = t, ... , s{X->t} = s'{X->t} ,... (*) provided X doesn't occur in t, but occurs in at least one s or s'. The substitution {X->t} should then be applied to all terms in the list (but not in X = t itself, of course). NB the equation X = t can be picked anywhere from the list, not necessarily the beginning. The algorithm is non-deterministic in that it doesn't matter which rule is applied in case more than one applies. Termination is ensured and the different outcomes are all equivalent. Stop unsuccesfully and return NOUNIFIER in any stage in which an equation X = t is found with X occurring in t but not equal to it (occur-check), or an equation f(..) = g(..) is found with f and g different. Stop succesfully if no rule applies anymore and no offending equation as above has been found. NB the rules for function symbols f are understood to include the case where f has zero arguments (f constant, delete f = f) Example explaining Prolog behavior without occur-check (p. 450): append(X,[a,b|E],E) = append([],Y,Y) => X = [], [a,b|E] = Y, E = Y => X = [], Y = [a,b|E], E = Y => X = [], Y = [a,b|E], E = [a,b|E] => NOUNIFIER since E occurs in [a,b|E] Prolog leaves out the occur check and starts printing out the circular binding for E = [a,b,a,b,a,b,... (infinite)