From Admissibility to a New Hierarchy of Unification Types

ABSTRACT. Motivated by the study of admissible rules, a new hierarchy of ``exact'' unification types is introduced where a unifier is more general than another unifier if all identities unified by the first are unified by the second. A Ghilardi-style algebraic interpretation of this hierarchy is presented that uses exact algebras rather than projective algebras. Examples of equational classes distinguishing the two hierarchies are also provided.