What is unification? - Question & Answer Book

 

Answer: The idea of unification is to describe values by logical equations which can be resolved automatically by some unification algorithm. First-order unification is a form of unification whose values are trees. There are several kinds of first-order unification which differ in the choice of the notion of trees. Trees may be ground terms (tuples) or feature trees (records), they may be finite or infinite. Forst-order unification for feature trees is called feature unification.