Unification

Summary

Unification is the problem of finding a substitution that makes two terms equal. Such a substitution is a unifier. When two terms have a unifier, they have a most general one, from which every other unifier is obtained by a further substitution. Robinson's unification algorithm computes it, and unification is at the core of resolution theorem proving, logic programming and type inference.