FURTHER THOUGHTS ON UNIFICATION

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:

   Is unification an associative operation?

   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:

   (E1 U E2) U E3 = E1 U (E2 U E3)

   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:

• Chang, Chin-Liang, & Lee, Richard Char-Tung (1973), Symbolic Logic and Mechanical Theorem Proving (San Diego: Academic Press), Ch. 5: "The Resolution Principle", esp. Sect. 5.4: "Unification Algorithm".
  • This is the source of the unification algorithm that I presented in lecture.

• Knight, Kevin (1989), "Unification: A Multidisciplinary Survey", ACM Computing Surveys 21: 93-124.
  • Locally cached version