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.

REFERENCES

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.