A substitution t_i / v_i specifies substitution of term t_i for variable v_i. Unification will produce a set of substitutions that make two literals the same.

A substitution set can be represented as either sequential substitutions (done one at a time in sequence) or as simultaneous substitutions (done all at once). Unification can be done correctly either way.

We will assume a simultaneous substitution, using the Lisp function sublis. (sublis alist form ) performs the substitutions specified by alist in the formula form. alist is of the form (( var . term ) ... ).

Suppose we want to substitute {a/x, f(b)/y} in P(x, y). In Lisp form, this is:

(sublis '((x . (a)) (y . (f (b))))
        '(p x y))

      = (P (A) (F (B)))

Contents    Page-10    Prev    Next    Page+10    Index