Consider expressions built up from variables and constants using function symbols. If 
, ..., 
are variables and 
, ..., 
are expressions, then a set of mappings between variables
and expressions 
is called a substitution.
If 
and 
is an expression, then 
is called an instance of 
if it is received from 
by simultaneously replacing all occurrences of 
(for 
) by the respective 
.
If 
and 
are two substitutions, then the
composition of 
and 
(denoted 
) is obtained from 
by removing
all elements 
such that 
and all elements 
such that 
is one of 
,
..., 
.
A substitution 
is called a unifier for the set of expressions 
if 
. A unifier 
for the set of expressions 
is called the most general unifier if, for any
other unifier for the same set of expressions 
, there is yet another unifier 
such that 
.
A unification algorithm takes a set of expressions as its input. If this set is not unifiable, the algorithm terminates and yields a negative result. If there exists a unifier for the input set of expressions, the algorithm yields the most general unifier for this set of expressions. The unification algorithm serves as a tool for the resolution principle. It is also a basis for term rewriting systems.
