first-order unification
(55 minutes to learn)
Summary
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.
Context
This concept has the prerequisites:
- first-order logic (Unification is a commonly used operation in first order reasoning.)
Goals
- 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-