 # E-Unification

Let E be an equational theory and let ? be the signature of the term algebra. An E-unification problem is a finite set of equations An E-unifier of Г is a substitution о, such that The set of all E-unifiers of Г is denoted U ?E (Г). A complete set of E-unifiers cU ?e (Г) for Г is a set of E-unifiers, such that for every E-unifier т there exists о e cU ?e (Г) with о <E т .Theset pU ?E (Г) is called a minimal complete set of E-unifiers for Г, if it is complete and for all distinct elements о and о' in pU ?E (Г) о <E о' implies о =E о'.

When a minimal complete set of E-unifiers of a unification problem Г exists, it is unique up to subsumption equivalence ~E. Minimal complete sets of E-unifiers need not always exist, and if they do, they might be singular, finite, or infinite. Since minimal complete sets of E-unifiers are isomorphic whenever they exist, they can be used to classify theories with respect to their corresponding unification problem as well. This leads naturally to the concept of a unification hierarchy which was first introduced in Siekmann’s doctoral thesis in 1976  and further refined and extended by himself and his later students as well as by many subsequent workers in the field of unification theory, see [7, 8, 31, 50, 76] for the standard surveys on this aspect.

A unification problem Г is:

• nullary, if Г is unifiable, but the minimal complete set of E-unifiers does not exist.
• unitary, if it is not nullary and the minimal complete set of E-unifiers for Г is of cardinality less or equal to 1.
• finitary, if it is not nullary and the minimal complete set of E-unifiers is always finite.
• infinitary, if it is not nullary and the minimal complete set of E-unifiers is infinite. An equational theory E is:
• unitary, if all unification problems for E are unitary
• finitary, if all unification problems are finitary.
• infinitary, if there is at least one infinitary unification problem and all unification problems have minimal complete sets of E-unifiers.
• • If there exists a solvable unification problem Г not having a minimal complete set of E-unifiers, then the equational theory E is nullary or of type zero.

The subsumption order and the encompassment order for E-unifiers are inherited from the above order on substitutions, that is an E-unifier о is more general than an E-unifier т, denoted as о <E т, if there exists a substitution X such that т =VE оХ.