1. Unification is not only useful in automated theorem proving. A version of it is also used in computational linguistics. See the article by Knight, below.

  2. Can one unify 3 expressions?

    Our use of unification is limited for use with Resolution, and Resolution is a rule of inference that tells you how to infer a sentence from 2 premises (not from 3). Since you never resolve more than 2 sentences at a time, you never have to unify more than 2 at a time.

    Nevertheless, an interesting question remains, if unification is limited to an input set of cardinality 2:

    I.e., let U be a binary operation on expressions such that E1 U E2 is the unification of W = {E1, E2}. Is U associative? I.e., does the following equation hold:

    I will leave this as an open question for those of you who are interested either to try to prove (from the algorithm) or to look up.

Useful references on unification include:

Copyright © 2002 by William J. Rapaport (rapaport@cse.buffalo.edu)
file: 572/S02/unification.08ap02.html