Unification is the process of finding solutions to equations.
Suppose we have a finite set of equations
between terms and .
The exact nature of and may vary: they might be first-order terms, or they might be terms of the -calculus. What is important is that they have some free variables .
Unification looks for a substitution that maps each free variable to a term such that all these equations hold. 'Holding' can mean a number of things:
Please expand.
Please expand.