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.

Unification in Description Logics has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the Description Logic EL, which is used to define several large biomedical ontologies, unification is NP-complete. An NP unification algorithm for EL based on a translation into propositional satisfiability (SAT) has recently been presented. In this report, we extend this SAT encoding in two directions: on the one hand, we add general concept inclusion axioms, and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the translation to be complete, however, the ontology needs to satisfy a certain cycle restriction. The SAT translation depends on a new rewriting-based characterization of subsumption w.r.t. ELHR+-ontologies.

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. A goal-oriented NP unification algorithm for EL that uses nondeterministic rules to transform a given unification problem into solved form has recently been presented. In this report, we extend this goal-oriented algorithm in two directions: on the one hand, we add general concept inclusion axioms (GCIs), and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the algorithm to be complete, however, the ontology consisting of the GCIs and role axioms needs to satisfy a certain cycle restriction.

We introduce an extension of the Description Logic FL0 that allows us to define concepts in an approximate way. More precisely, we extend FL0 with a threshold concept constructor of the form Ct><l t for t><l ∈ {≤, <, ≥, >}, whose semantics is given by using a membership distance function (mdf). A membership distance function m assigns to each domain element and concept a distance value expressing how “close” is such element to being an instance of the concept. Based on this, a threshold concept Ct><l t is interpreted as the set of all domain elements that have a distance s from C such that s t><l t. We provide a framework to obtain membership distance functions based on functions that compare tuples of languages, and we show how weighted looping tree automata over a semiring can be used to define membership distance functions for FL0 concepts. / This is an extended version of an article accepted at the 36th International Workshop on Description Logics (DL 2023).

Unification has been introduced in Description Logic (DL) as a means to detect redundancies in ontologies. In particular, it was shown that testing unifiability in the DL EL is an NP-complete problem, and this result has been extended in several directions. Surprisingly, it turned out that the complexity increases to PSpace if one disallows the use of the top concept in concept descriptions. Motivated by features of the medical ontology SNOMED CT, we extend this result to a setting where the top concept is disallowed, but there is a background ontology consisting of restricted forms of concept and role inclusion axioms. We are able to show that the presence of such axioms does not increase the complexity of unification without top, i.e., testing for unifiability remains a PSpace-complete problem.

Formal ontologies are of significant importance in artificial intelligence, playing a central role in the Semantic Web, ontology-based information integration, or peer-to-peer data management. In such scenarios, an especially prominent role is played by description logics (DLs) – a robust family of logical formalisms used to describe ontologies and serving as the logical underpinning of contemporary standardised ontology languages. To put knowledge bases to full use as core part of intelligent information systems, much attention is being devoted to the area of ontology-based data-access, with conjunctive queries and their generalisations such as positive conjunctive two-way regular path queries being employed as a fundamental querying formalism. The most expressive exemplars of description logics feature advanced constructors for roles and path expressions. Among the most powerful knowledge representation formalisms on the verge of decidability, are the DLs from the Z family. For its most expressive proponent, ZOIQ (a.k.a. ALCHbSelf reg OIQ), featuring nominals (O), role inverses (I), and number restrictions (Q), querying is undecidable and even decidability of knowledge-base satisfiability is open, owing to the intricate interplay of the three mentioned features. Restricting the interaction of O, I, and Q however (or excluding one of the features altogether) leads to beneficial model-theoretic properties, which give rise to upper bounds of ExpTime for knowledge-base satisfiability and 2ExpTime for querying. Aiming for better understanding of the “expressive power versus computational complexity” trade-off for the Z family of DLs, we provide a more fine-grained complexity analysis for the query entailment problem over ontologies. In the thesis we focus on tame fragments of ZOIQ, namely the fragments in which either one the three features from {I, O, Q} is dropped or the class of models is restricted to the so-called quasi-forests. We employ the query languages ranging from (unions of) conjunctive queries ((U)CQs) to positive two-way regular path queries (P2RPQs). We mostly follow the classical semantics of entailment, but we also provide several results in the “finite-model” scenario. The most important results of the thesis are summarised below. 1. We provide a complete classification of the complexity of the query entailment problem (for various query languages discussed above) for tamed fragments of ZOIQ under the classical semantics. This involves several new ingredients such as: (i) a uniform exponential-time algorithm based on Lutz’s spoiler technique for the entailment of unions of conjunctive queries for ALCHbreg, (ii) new lower bounds for (rooted and unrooted) conjunctive query entailment over ALCSelf ontologies, and (iii) a novel reduction from the entailment of P2RPQs to the satisfiability problem for tamed ZOIQ, yielding a uniform 2ExpTime upper bound for all the considered logics. As a preliminary step towards lifting the above results to the realm of data complexity, we establish that the satisfiability of tamed ZOIQ is NP-complete. 2. Under the finite model semantics, we focus on UCQs only. With the proviso that the finite satisfiability problem for ZIQ is ExpTime-complete, we also provide a complete picture of the complexity of the query entailment problems. The key insight is that ZOI and ZOQ are finitely controllable. 3. We conclude the thesis by investigating the decidability border of further extensions of the Z family of DLs. Our goal is to understand whether the class of regular languages present in path expressions in Z is maximal for guaranteeing decidability of the underlying logic. We provide a series of undecidability results involving simple, non-regular languages (a subclass of visibly pushdown languages). Our proofs rely on well-established model- and graph-theoretic definitions. What is more, most of them generalise (in a uniform way) and solidify multiple results known by the DL community. Our proofs are also easily adjustable to freshly defined logics, without the need to reproduce nearly-identical proofs.

We discuss explanations in Description Logics (DLs), a family of logics used for knowledge representation. Initial work on explaining consequences for DLs had focused on justifications, which are minimal subsets of axioms that entail the consequence. More recently, it was proposed that proofs can provide more detailed information about why a consequence follows. Moreover, several measures have been proposed to estimate the comprehensibility of justifications and proofs, for example, their size or the complexity of logical expressions. In this paper, we analyze the connection between these measures, e.g. whether small justifications necessarily give rise to small proofs. We use a dataset of DL proofs that was constructed last year based on the ontologies of the OWL Reasoner Evaluation 2015. We find that, in general, less complex justifications indeed correspond to less complex proofs, and discuss some exceptions to this rule.

In knowledge bases, relational data is combined with knowledge formalized through logic. This formalized knowledge is often called an ontology. Queries to knowledge bases are then answered with respect to the ontology, yielding more comprehensive results. Real-world knowledge bases contain thousands of relations and many thousand logical statements in their ontology. Writing queries that yield the desired answers therefore requires effort and expertise. In this dissertation, we investigate the learnability of conjunctive queries (CQs) under description logic (DL) ontologies. We focus on learning in the sense of Angluin’s exact learning and of probably approximately correct (PAC) learning, and on description logics of the EL and DL-Lite-core families, which underlie the OWL 2 EL and QL profiles, respectively. In both models of learning, the learner tries to learn a target query based on limited available information. In exact learning, this information is provided by a teacher who answers certain types of questions (membership queries and equivalence queries) truthfully, whereas in PAC learning the learner receives randomly drawn labeled data examples. One key question is whether polynomial-time algorithms exist that allow the learner to always learn the target query, even when the information about the target query is provided with respect to a DL ontology. In this dissertation, we aim to determine for which classes of CQs and for which ontology languages such polynomial-time learning algorithms exist, and which kinds of questions (membership queries and equivalence queries) are necessary for polynomial-time learning in the exact learning model. For this, we build upon existing results on the learnability of queries without ontologies. The following are the main contributions of my thesis: We show that membership queries alone suffice to learn unary acyclic connected CQs (that correspond to concepts of the description logic ELI) in polynomial time under DL-Lite-core ontologies. This result also holds if the ontology includes role hierarchies and a limited form of functionality assertions. In contrast, We show that EL ontologies (and most extensions of DL-Lite-core) make learning with only membership queries difficult: in the worst case, an exponential number of membership queries is required to identify the target query. We show that using both membership queries and equivalence queries, the class of tree-shaped CQs (as well as the larger class of chordal and symmetry-free CQs) is polynomial-time learnable under EL ontologies. This also holds for unary acyclic connected CQs under DL-Lite-horn ontologies, an extension of DL-Lite-core. However, these results do not extend to ontologies formulated in ELI, which extends EL with inverses. Already simple query classes are not polynomial-time learnable under ELI ontologies. We review that equivalence queries alone are not sufficient to learn simple path-shaped CQs in polynomial time, unless NP= RP. This implies that no polynomial-time PAC learning algorithms exist for CQs. Instead, We show that PAC learning of CQs under ontologies, with a required sample size that grows only polynomially, is possible using an algorithm that always returns the smallest query that fits the labeled examples. We implemented such an algorithm for tree-shaped CQs (which correspond to ℰℒ concepts) under EL ontologies and show that the implementation compares favorably to an existing EL concept learning algorithm on benchmarks.