KR Conference 2012 Conference Paper
- Yevgeny Kazakov
- Markus Krötzsch
- Frantisek Simancik
The EL family of description logics (DLs) has been designed to provide a restricted syntax for commonly used DL constructors with the goal to guarantee polynomial complexity of reasoning. Yet, polynomial complexity does not always mean that the underlying reasoning procedure is efficient in practice. In this paper we consider a simple DL ELO from the EL family that admits nominals, and argue that existing polynomial reasoning procedures for ELO can be impractical for many realistic ontologies. To solve the problem, we describe an optimization strategy in which the inference rules required for reasoning with nominals are avoided as much as possible. The optimized procedure is evaluated within the reasoner ELK and demonstrated to perform well in practice. LossOfScalpHair u ∃hasPhenotypicalSex. ∃hasAbsoluteState. {maleSex}. The nominal {maleSex} denotes a concept with a single element, and the definition thus asserts that the role hasAbsoluteState has exactly this single value for every instance of MalePatternBaldness. This is generally expressed with concept expressions of the form ∃R. {c} for which the OWL standard even introduces a dedicated syntactic shortcut “ObjectHasValue. ” In practice, however, nominals are hardly used in OWL EL ontologies. Even Galen models maleSex as an atomic concept, which seems unintuitive since there is only one male sex. A closer look reveals many other atomic concepts that are used as values for roles rather than as classes of objects, e. g., blue, soluble, and even sixteen. What is the reason for this apparent lack of nominals in current ontologies? One possible explanation is that practical tool support for nominals in OWL EL is extremely limited. Amongst the currently available EL reasoners, Snorocket provides no support for nominals, CEL only supports ABox assertions, and the support for nominals in jCEL is incomplete. One could hope this to be a minor omission, given that reasoning is still known to be polynomial in the worst case. However, the implementation of algorithms that can handle nominals efficiently turned out to be challenging. A difficulty in this case is that, in the presence of nominals, mere non-emptiness of concepts can lead to new entailments, e. g., asserting that a particular concept has at least one instance may lead to a new subsumption between atomic concepts. This contrasts strongly to the case of EL without nominals, where non-emptiness of concepts (and, in fact, arbitrary ABox assertions) can never entail a new TBox fact. To deal with this difficulty, algorithms must take nonemptiness of concepts into account during reasoning, e. g., by tracking whether non-emptiness of one concept implies non-emptiness of another. Baader et al. (2005) proposed to