Aus der Einleitung: „Equational unification is a generalization of syntactic unification in which semantic properties of function symbols are taken into account. For example, assume that the function symbol '+' is known to be commutative. Given the unication problem x + y ≐ a + b (where x and y are variables, and a and b are constants), an algorithm for syntactic unification would return the substitution {x ↦ a; y ↦ b} as the only (and most general) unifier: to make x + y and a + b syntactically equal, one must replace the variable x by a and y by b. However, commutativity of '+' implies that {x ↦ b; y ↦ b} also is a unifier in the sense that the terms obtained by its application, namely b + a and a + b, are equal modulo commutativity of '+'. More generally, equational unification is concerned with the problem of how to make terms equal modulo a given equational theory, which specifies semantic properties of the function symbols that occur in the terms to be unified.”

We show that extending description logics by simple aggregation functions as available in database systems may lead to undecidability of inference problems such as satisfiability and subsumption.

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to replace certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language.

Aus der Einleitung: „Description logics (DLs) are a family of logical formalisms well-suited for the representation of and reasoning about conceptual knowledge on an abstract logical level. However, for many knowledge representation applications, it is essential to integrate the abstract logical knowledge with knowledge of a more concrete nature. As an example, consider the modeling of manufacturing processes, where it is necessary to represent 'abstract' entities like subprocesses and workpieces and also 'concrete' knowledge, e.g., about the duration of processes and physical dimensions of the manufactured objects [2; 25].”

From the Motivation: „Description Logics (DLs) are a family of formalisms well-suited for the representation of and reasoning about knowledge. Whereas most Description Logics represent only static aspects of the application domain, recent research resulted in the exploration of various Description Logics that allow to, additionally, represent temporal information, see [4] for an overview. The approaches to integrate time differ in at least two important aspects: First, the basic temporal entity may be a time point or a time interval. Second, the temporal structure may be part of the semantics (yielding a multi-dimensional semantics) or it may be integrated as a so-called concrete domain. Examples for multi-dimensional point-based logics can be find in, e.g., [21;29], while multi-dimensional interval-based logics are used in, e.g., [23;2]. The concrete domain approach needs some more explanation. Concrete domains have been proposed by Baader and Hanschke as an extension of Description Logics that allows reasoning about 'concrete qualities' of the entities of the application domain such as sizes, length, or weights of real-worlds objects [5]. Description Logics with concrete domains do usually not use a fixed concrete domain; instead the concrete domain can be thought of as a parameter to the logic. As was first described in [16], if a 'temporal' concrete domain is employed, then concrete domains may be point-based, interval-based, or both. ...”

Computing the least common subsumer (lcs) in description logics is an inference task first introduced for sublanguages of CLASSIC. Roughly speaking, the lcs of a set of concept descriptions is the most specific concept description that subsumes all of the input descriptions. As such, the lcs allows to extract the commonalities from given concept descriptions, a task essential for several applications like, e.g., inductive learning, information retrieval, or the bottom-up construction of KR-knowledge bases. Previous work on the lcs has concentrated on description logics that either allow for number restrictions or for existential restrictions. Many applications, however, require to combine these constructors. In this work, we present an lcs algorithm for the description logic ALEN, which allows for both constructors (as well as concept conjunction, primitive negation, and value restrictions). The proof of correctness of our lcs algorithm is based on an appropriate structural characterization of subsumption in ALEN also introduced in this paper. / This research was carried out while the second author was still at the LuFG Theoretical Computer Science, RWTH Aachen.

Ontologies based on Description Logics may contain errors, which are usually detected when reasoning produces consequences that follow from the ontology, but do not hold in the modelled application domain. In previous work, we have introduced repair approaches for EL ontologies that are optimal in the sense that they preserve a maximal amount of consequences. In this paper, we will, on the one hand, review these approaches, but with an emphasis on motivation rather than on technical details. On the other hand, we will describe new results that address the problems that optimal repairs may become very large or need not even exist unless strong restrictions on the terminological part of the ontology apply. We will show how one can deal with these problems by introducing concise representations of optimal repairs.

We discuss two ways of using abduction to explain missing entailments from description logic knowledge bases, one more common, one more unusual, and then have a closer look at how current results/implementations on abduction could be used towards generating such explanations, and what still needs to be done. / This is an extended version of an article submitted to XLoKR 2021.

Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can occur within DL concept descriptions. In this setting, reasoning usually becomes quite hard if rigid roles, i.e., roles whose interpretation does not change over time, are available. In this paper, we consider the case where temporal operators are allowed to occur only in front of DL axioms (i.e., ABox assertions and general concept inclusion axioms), but not inside of concepts descriptions. As the temporal component, we use linear temporal logic (LTL) and in the DL component we consider the basic DL ALC. We show that reasoning in the presence of rigid roles becomes considerably simpler in this setting.

Axiom pinpointing has been introduced in description logics (DLs) to help the used understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in consideration. Several pinpointing algorithms have been described as extensions of the standard tableau-based reasoning algorithms for deciding 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, using specific traits of them. In the past, we have developed a general approach for extending tableau-based algorithms into pinpointing algorithms. In this paper we explore some issues of termination of general tableaux and their pinpointing extensions. We also define a subclass of tableaux that allows the use of so-called blocking conditions, which stop the execution of the algorithm once a pattern is found, and adapt the pinpointing extensions accordingly, guaranteeing its correctness and termination.