The application of automated reasoning approaches to Description Logic (DL) ontologies may produce certain consequences that either are deemed to be wrong or should be hidden for privacy reasons. The question is then how to repair the ontology such that the unwanted consequences can no longer be deduced. An optimal repair is one where the least amount of other consequences is removed. Most of the previous approaches to ontology repair are of a syntactic nature in that they remove or weaken the axioms explicitly present in the ontology, and thus cannot achieve semantic optimality. In previous work, we have addressed the problem of computing optimal repairs of (quantified) ABoxes, where the unwanted consequences are described by concept assertions of the light-weight DL EL. In the present paper, we improve on the results achieved so far in two ways. First, we allow for the presence of terminological knowledge in the form of an EL TBox. This TBox is assumed to be static in the sense that it cannot be changed in the repair process. Second, the construction of optimal repairs described in our previous work is best case exponential. We introduce an optimized construction that is exponential only in the worst case. First experimental results indicate that this reduces the size of the computed optimal repairs considerably.

Errors in Description Logic (DL) ontologies are often detected when a reasoner computes unwanted consequences. The question is then how to repair the ontology such that the unwanted consequences no longer follow, but as many of the other consequences as possible are preserved. The problem of computing such optimal repairs was addressed in our previous work in the setting where the data (expressed by an ABox) may contain errors, but the schema (expressed by an EL TBox) is assumed to be correct. Actually, we consider a generalization of ABoxes called quantified ABoxes (qABoxes) both as input for and as result of the repair process. Using qABoxes for repair allows us to retain more information, but the disadvantage is that standard DL systems do not accept qABoxes as input. This raises the question, investigated in the present paper, whether and how one can obtain optimal repairs if one restricts the output of the repair process to being ABoxes. In general, such optimal ABox repairs need not exist. Our main contribution is that we show how to decide the existence of optimal ABox repairs in exponential time, and how to compute all such repairs in case they exist.

Ontologies based on Description Logic (DL) represent general background knowledge in a terminology (TBox) and the actual data in an ABox. DL systems can then be used to compute consequences (such as answers to certain queries) from an ontology consisting of a TBox and an ABox. Since both human-made and machine-learned data sets may contain errors, which manifest themselves as unintuitive or obviously incorrect consequences, repairing DL-based ontologies in the sense of removing such unwanted consequences is an important topic in DL research. Most of the repair approaches described in the literature produce repairs that are not optimal, in the sense that they do not guarantee that only a minimal set of consequences is removed. In a series of papers, we have developed an approach for computing optimal repairs, starting with the restricted setting of an EL instance store, extending this to the more general setting of a quantified ABox (where some individuals may be anonymous), and then adding a static EL TBox. Here, we extend the expressivity of the underlying DL considerably, by adding nominals, inverse roles, regular role inclusions and the bottom concept to EL, which yields a fragment of the well-known DL Horn-SROIQ. The ideas underlying our repair approach still apply to this DL, though several non-trivial extensions are needed to deal with the new constructors and axioms. The developed repair approach can also be used to treat unwanted consequences expressed by certain conjunctive queries or regular path queries, and to handle Horn-ALCOI TBoxes with regular role inclusions. / This is an extended version of an article accepted at KR 2022.

The Nelson-Oppen combination method can be used to combine decision procedures for the validity of quantifier-free formulae in first-order theories with disjoint signatures, provided that the theories to be combined are stably infinite. We show that, even though equational theories need not satisfy this property, Nelson and Oppen's method can be applied, after some minor modifications, to combine decision procedures for the validity of quantifier-free formulae in equational theories. Unfortunately, and contrary to a common belief, the method cannot be used to combine decision procedures for the word problem. We present a method that solves this kind of combination problem. Our method is based on transformation rules and also applies to equational theories that share a finite number of constant symbols.

Number restrictions are concept constructors that are available in almost all implemented description logic systems. However, even though there has lately been considerable effort on integrating expressive role constructors into description logics, the roles that may occur in number restrictions are usually of a very restricted type. Until now, only languages with number restrictions on atomic roles and inversion of atomic roles, or with number restrictions on intersection of atomic roles have been investigated in detail. In the present paper, we increase the expressive power of description languages by allowing for more complex roles in number restrictions. As role constructors, we consider composition of roles (which will be present in all our languages), and intersection, union and inversion of roles in different combinations. We will present one decidability result (for the basic language that extends ALC by number restrictions on roles with composition), and three undecidability results for three different extensions of the basic language.

Computing the most specific concept (msc) is an inference task that can be used to support the 'bottom-up' construction of knowledge bases for KR systems based on description logics. For description logics that allow for number restrictions or existential restrictions, the msc need not exist, though. Previous work on this problem has concentrated on description logics that allow for universal value restrictions and number restrictions, but not for existential restrictions. The main new contribution of this paper is the treatment of description logics with existential restrictions. More precisely, we show that, for the description logic ALE (which allows for conjunction, universal value restrictions, existential restrictions, negation of atomic concepts) the msc of an ABox-individual only exists in case of acyclic ABoxes. For cyclic ABoxes, we show how to compute an approximation of the msc. Our approach for computing the (approximation of the) msc is based on representing concept descriptions by certain trees and ABoxes by certain graphs, and then characterizing instance relationships by homomorphisms from trees into graphs. The msc/approximation operation then mainly corresponds to unraveling the graphs into trees and translating them back into concept descriptions.

Because of the importance of undecidability and the concern with the high complexity of automated reasoning, a few interval-based temporal description logics (ITDLs) have been designed. Moreover, most existing ITDLs are not able to specify the lengths of intervals. In other words, they are not metric. On the other hand, some domains (e.g., medicine) are inherently interval-based, and require a metric logic in order to formalize defined processes and to check process consistency. Hence, a metric interval-based temporal description logic is required. In this thesis, we introduce such a logic (MITDL) along with two algorithms for the satisfiability checking of its formulas. We first introduce an interval-based temporal logic, called IMPNL, inspired by Metric Propositional Neighbourhood Logic. We also present a sound, com- plete and terminating tableau-based algorithm for checking the satisfiability of IMPNL formulas. Afterwards, we combine a restricted version of IMPNL (IMPNL without a negation operator) with the ALC description logic to form a MITDL. We propose two tableau-based algorithms for checking the satisfia- bility of MITDL formulas. We show and prove they are sound, complete and terminate. These algorithms have PSpace and 2NExp-Time complexities. As a proof of concept, we use IMPNL and MITDL to model some clinical practice guidelines (CPG) and check their consistency. We compare MITDL with several languages commonly used for modeling CPGs. / Thesis / Doctor of Science (PhD)

No description available.

Concrete domains have been introduced in the area of Description Logic (DL) to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability. To regain decidability of the DL ALC in the presence of GCIs, quite strong restrictions, called ω-admissibility, were imposed on the concrete domain. On the one hand, we generalize the notion of ω-admissibility from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate ω-admissibility to well-known notions from model theory. In particular, we show that finitely bounded homogeneous structures yield ω-admissible concrete domains. This allows us to show ω-admissibility of concrete domains using existing results from model theory. When integrating concrete domains into lightweight DLs of the EL family, achieving decidability of reasoning is not enough. One wants the resulting DL to be tractable. This can be achieved by using so-called p-admissible concrete domains and restricting the interaction between the DL and the concrete domain. We investigate p-admissibility from an algebraic point of view. Again, this yields strong algebraic tools for demonstrating p-admissibility. In particular, we obtain an expressive numerical p-admissible concrete domain based on the rational numbers. Although ω-admissibility and p-admissibility are orthogonal conditions that are almost exclusive, our algebraic characterizations of these two properties allow us to locate an infinite class of p-admissible concrete domains whose integration into ALC yields decidable DLs. DL systems that can handle concrete domains allow their users to employ a fixed set of predicates of one or more fixed concrete domains when modelling concepts. They do not provide their users with means for defining new predicates, let alone new concrete domains. The good news is that finitely bounded homogeneous structures offer precisely that. We show that integrating concrete domains based on finitely bounded homogeneous structures into ALC yields decidable DLs even if we allow predicates specified by first-order formulas. This class of structures also provides effective means for defining new ω-admissible concrete domains with at most binary predicates. The bad news is that defining ω-admissible concrete domains with predicates of higher arities is computationally hard. We obtain two new lower bounds for this meta-problem, but leave its decidability open. In contrast, we prove that there is no algorithm that would facilitate defining p-admissible concrete domains already for binary signatures.:1. Introduction . . . 1 2. Preliminaries . . . 5 3. Description Logics with Concrete Domains . . . 9 3.1. Basic definitions and undecidability results . . . 9 3.2. Decidable and tractable DLs with concrete domains . . . 16 4. A Model-Theoretic Analysis of ω-Admissibility . . . 23 4.1. Homomorphism ω-compactness via ω-categoricity . . . 23 4.2. Patchworks via homogeneity . . . 24 4.3. JDJEPD via decomposition into orbits . . . 27 4.4. Upper bounds via finite boundedness . . . 28 4.5. ω-admissible finitely bounded homogeneous structures . . . 32 4.6. ω-admissible homogeneous cores with a decidable CSP . . . 34 4.7. Coverage of the developed sufficient conditions . . . 36 4.8. Closure properties: homogeneity & finite boundedness . . . 39 5. A Model-Theoretic Analysis of p-Admissibility . . . 47 5.1. Convexity via square embeddings . . . 47 5.2. Convex ω-categorical structures . . . 50 5.3. Convex numerical structures . . . 52 5.4. Ages defined by forbidden substructures . . . 54 5.5. Ages defined by forbidden homomorphic images . . . 56 5.6. (Non-)closure properties of convexity . . . 59 6. Towards user-definable concrete domains . . . 61 6.1. A proof-theoretic perspective . . . 65 6.2. Universal Horn sentences and the JEP . . . 66 6.3. Universal sentences and the AP: the Horn case . . . 77 6.4. Universal sentences and the AP: the general case . . . 90 7. Conclusion . . . 99 7.1. Contributions and future outlook . . . 99 A. Concrete Domains without Equality . . . 103 Bibliography . . . 107 List of figures . . . 115 Alphabetical Index . . . 117

Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of „tableau algorithms,' which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.