first-order unification

Fetching content
(55 minutes to learn)


Unification is a procedure which takes two symbolic expressions containing variables, and returns a substitution to the variables which makes the expressions identical. It is a key component of first-order theorem provers and type inference systems.


This concept has the prerequisites:


  • Know what the unification procedure is and what the output is.
  • Be able to simulate it on simple examples.
  • What is the occurs check, why is it needed, and why does it increase the complexity of the algorithm?
  • Why do variables sometimes need to be renamed before performing unification?
  • What does it mean for one unifier to be more general than another, and why does one desire the most general unifier?

See also

-No Additional Notes-