Higher Order Unification

Unification is an important problem in many areas of automated reasoning, mainly automated theorem proving. However, the problem is not decidable in higher-order logics. Still, practical algorithms exist that work in many cases. In this paper, we explain the semi-decision unification algorithm by Huet. We put special emphasis on the intuitive understanding how the algorithm works.