id: 05949451
dt: a
an: 05949451
au: Binh, Nguyen Thanh
ti: Decidability of unification in EL without top constructor.
so: Rudolph, Sebastian (ed.) et al., Web reasoning and rule systems. 5th
    international conference, RR 2011, Galway, Ireland, August 29‒30,
    2011. Proceedings. Berlin: Springer (ISBN 978-3-642-23579-5/pbk).
    Lecture Notes in Computer Science 6902, 170-184 (2011).
py: 2011
pu: Berlin: Springer
la: EN
cc: 
ut: 
ci: 
li: doi:10.1007/978-3-642-23580-1_13
ab: Summary: 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.
rv: