Decidability of Unification in EL without Top Constructor

In recent years, the description logic

$\cal{EL}$

has received a significant interest. The description logic

$\cal{EL}$

is a knowledge representation formalism used e.g in natural language processing, configuration of technical systems, databases and biomedical ontologies. Unification is used there as a tool to recognize equivalent concepts. It has been proven that unification in

$\cal{EL}$

is NP-complete. This result was based on a locality property of certain

$\cal{EL}$

unifiers. In fact, the large medical ontology SNOMED CT was built on a subset of

${\cal{EL}}$

++ formalism, however, without top-concept. It would be interesting to investigate decidability of unification in extensions of

$\cal{EL}$

without using top-concept. In this paper, we look at decidability of unification in

$\cal{EL}$

without top (

$\cal{EL}^{- \top}$

). We show that a similar locality holds for

$\cal{EL}^{- \top}$

, but decidability of

$\cal{EL}^{- \top}$

unification does not follow immediately from locality as it does in the case of unification in

$\cal{EL}$

. However, by restricting further the locality property, we prove that

$\cal{EL}^{- \top}$

unification is decidable and construct an NExpTime decision procedure for the problem. Moreover, the procedure allows us to compute a specific set of solutions to the unification problem.