The tableau algorithm implemented in the FaCT knowledge representation system decides satisfiability and subsumption in SHIQ, a very expressive description logic providing, e.g., inverse and transitive roles, number restrictions, and general axioms. Intuitively, the algorithm searches for a tree-shaped abstraction of a model. To ensure termination of this algorithm without comprimising correctness, it stops expanding paths in the search tree using a so-called 'double-blocking' condition.

Unification in the Description Logic (DL) FL₀ is known to be ExpTimecomplete, and of unification type zero. We investigate in this paper whether a lower complexity of the unification problem can be achieved by either syntactically restricting the role depth of concepts or semantically restricting the length of role paths in interpretations. We show that the answer to this question depends on whether the number formulating such a restriction is encoded in unary or binary: for unary coding, the complexity drops from ExpTime to PSpace. As an auxiliary result, which is however also of interest in its own right, we prove a PSpace-completeness result for a depth-restricted version of the intersection emptiness problem for deterministic root-to-frontier tree automata. Finally, we show that the unification type of FL₀ improves from type zero to unitary (finitary) for unification without (with) constants in the restricted setting.

Description Logics (DLs) [BCM+07] are prominent modeling formalisms underlying the Web Ontology Language (OWL). The lightweight DL EL in particular is used to formulate many biomedical ontologies. DLs allow to represent subconcept-superconcept relationships between concepts, e.g., diseases, as well as more complex correspondences. Unification in DLs has been proposed as a non-standard reasoning task to detect redundant concepts in ontologies [BN01, BM10b]. Recently, disunification in EL has been investigated and several algorithms were proposed to solve disunification problems [BBM16].

Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic EL to disunification since negative constraints on unifiers can be used to avoid unwanted unifiers. While decidability of the solvability of general EL-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint must be ground, and local solvability of disunification problems, where we restrict the attention to solutions that are built from so-called atoms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of (general) disunification problems.

Recently introduced approaches for relaxed query answering, approximately defining concepts, and approximately solving unification problems in Description Logics have in common that they are based on the use of concept comparison measures together with a threshold construction. In this paper, we will briefly review these approaches, and then show how weighted automata working on infinite trees can be used to construct computable concept comparison measures for FL₀ that are equivalence invariant w.r.t. general TBoxes. This is a first step towards employing such measures in the mentioned approximation approaches. / Accepted to LATA 2017

In the area of Description Logics the least common subsumer (lcs) and the most specific concept (msc) are inferences that generalize a set of concepts or an individual, respectively, into a single concept. If computed w.r.t. a general EL-TBox neither the lcs nor the msc need to exist. So far in this setting no exact conditions for the existence of lcs- or msc-concepts are known. This report provides necessary and suffcient conditions for the existence of these two kinds of concepts. For the lcs of a fixed number of concepts and the msc we show decidability of the existence in PTime and polynomial bounds on the maximal roledepth of the lcs- and msc-concepts. The latter allows to compute the lcs and the msc, respectively.

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NP-complete. However, the unification algorithms for EL developed until recently could not deal with ontologies containing general concept inclusions (GCIs). In a series of recent papers we have made some progress towards addressing this problem, but the ontologies the developed unification algorithms can deal with need to satisfy a certain cycle restriction. In the present paper, we follow a different approach. Instead of restricting the input ontologies, we generalize the notion of unifiers to so-called hybrid unifiers. Whereas classical unifiers can be viewed as acyclic TBoxes, hybrid unifiers are cyclic TBoxes, which are interpreted together with the ontology of the input using a hybrid semantics that combines fixpoint and descriptive semantics. We show that hybrid unification in EL is NP-complete and introduce a goal-oriented algorithm for computing hybrid unifiers.

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of significantly lower complexity than unification in other DLs of similarly restricted expressive power. However, the unification algorithms for EL developed so far cannot deal with general concept inclusion axioms (GCIs). This paper makes a considerable step towards addressing this problem, but the GCIs our new unification algorithm can deal with still need to satisfy a certain cycle restriction.

Fuzzy description logics (DLs) have been investigated for over two decades, due to their capacity to formalize and reason with imprecise concepts. Very recently, it has been shown that for several fuzzy DLs, reasoning becomes undecidable. Although the proofs of these results differ in the details of each specific logic considered, they are all based on the same basic idea. In this report, we formalize this idea and provide sufficient conditions for proving undecidability of a fuzzy DL. We demonstrate the effectiveness of our approach by strengthening all previously-known undecidability results and providing new ones. In particular, we show that undecidability may arise even if only crisp axioms are considered.

We extend previous results on the complexity of solving language equations with one-sided concatenation and all Boolean operations to the case where also disequations (i.e., negated equations) may occur. To show that solvability of systems of equations and disequations is still in ExpTime, we introduce a new type of automata working on infinite trees, which we call looping automata with colors. As applications of these results, we show new complexity results for disunification in the description logic FL₀ and for monadic set constraints with negation. We believe that looping automata with colors may also turn out to be useful in other applications. / A short version of this report has also appeared in Proceedings of LPAR-18, Springer LNCS 7180, 2012.