1. Initialize the substitution set to be empty. We do this with the set ((t . t)). A nil set indicates failure.

2. Recursively unify expressions:
   1. Identical items match.

   2. If one item is a variable v_i and the other is a term t_i not containing that variable, then:
      1. Substitute t_i / v_i in the existing substitutions.

      2. Add t_i / v_i to the substitution set.

   3. If both items are functions, the function names must be identical and all arguments must unify. Substitutions are made in the rest of the expression as unification proceeds.

Contents    Page-10    Prev    Next    Page+10    Index