Unification
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.
Contact the MathWorld Team
birthday problem 35 people