# 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

*c*

*?*

**U**_{e}(Г) for

*Г*is a set of

*E*-unifiers, such that for every

*E*-unifier

*т*there exists

*о e c*

*?*

**U**_{e}(Г) with

*о*<

_{E}

*т*.Theset

*p*

**U***?*is called a

_{E}(Г)*minimal complete set*of

*E*-unifiers for

*Г*, if it is complete and for all distinct elements

*о*and

*о'*in

*p*

**U***?*<

_{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 [73] 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 *т = ^{V}E оХ.*