# 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-