Habilitation Theses

@thesis{ Mor-Hab-17,
  address = {Dresden, Germany},
  author = {Barbara {Morawska}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Unification, Matching and Disunification in the Description Logic $\mathcal{E\mkern-1.618mu L}$},
  type = {Habilitation Thesis},
  year = {2017},
}

@thesis{ Pen-Hab-15,
  address = {Dresden, Germany},
  author = {Rafael Pe\~{n}aloza {Nyssen}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Reasoning with Annotated Description Logic Ontologies},
  type = {Habilitation Thesis},
  year = {2015},
}

@thesis{ Turhan-Hab,
  address = {Dresden, Germany},
  author = {Anni-Yasmin {Turhan}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Reasoning Services for the Maintenance and Flexible Access to Description Logic Ontologies},
  type = {Habilitation Thesis},
  year = {2014},
}

@thesis{ Lutz-Hab-2006,
  address = {Dresden, Germany},
  author = {Carsten {Lutz}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Modal Logics for Computer Science},
  type = {Habilitation Thesis},
  year = {2006},
}

Description Logics (DLs) are a family of knowledge representation formalisms designed for the representation of terminological knowledge. A DL knowledge base consists (at least) of a set of concept definitions, namely of those concepts that are relevant for the specific application. Standard inference services provided by DL-based knowledge representation systems include tests whether each defined concept is satisfiable and the computation of the subsumption hierarchy of the defined concepts, i.e., of the specialisation relation between the defined oncepts.

Besides the well-defined semantics of DLs, these inference services make DLs suitable candidates for ontology languages, which have become of increasing importance due to the amount of information available electronically and the vision of the semantic web. For a variety of DLs, decision procedures, tight complexity bounds, and practical inference algorithms for the corresponding inference problems are known. It is clear that, to be of use as an ontology language, a description logic has to provide adequate expressive power, and we are thus concerned with the well-known trade-off between complexity and expressiveness.

After a brief introduction to ontologies, we introduce the basic description logic ALC and describe how DLs can be used as ontology languages. Next, we sketch the relationship between DLs and other formalisms such as first order and modal logic and data base conceptual models. To give a broader view of DLs, some standard expressive means in DLs are mentioned as well as their modal logic counterparts and their effect on the complexity of the inference problems. In Section 3, we give an intuitive explanation of standard reasoning techniques employed for DLs and discuss their respective advantages: tableau-based algorithms turned out to be well-suited for implementations, whereas automata-based algorithms yield elegant upper complexity bounds for Exptime logics. In many cases, first a DL was proven to be in Exptime using automata before a tableau-based algorithm was designed and implemented.

Having thus introduced description logics and how they can be used as ontology languages, in Section 4, we describe how we have designed the rather successful DLs SHIQ and RIQ: we first observe that ALC lacks the expressive power to describe aggregated objects using a transitive part-whole relation, and then extend ALC with a new constructor that overcomes this expressive shortcoming while still allowing for a practical, tableau-based inference algorithm. Step by step, we further extend the resulting DLs with new constructors that were chosen according to the same design goal: to overcome expressive shortcomings while allowing for practical inference algorithms. For each extension, we describe how we have modified the tableau algorithm to take into account the new constructor.

In Section 5, we are concerned with hybrid logics, i.e., description and modal logics that allow to refer to single individuals using nominals. Nominals are a rather special constructor since they destroy a nice model theoretic property that most DLs enjoy, namely the tree model property. Despite this effect, we were able to show, for two example hybrid logics, that automata on trees can still be used to decide satisfiability of hybrid DLs and thus provide tight upper complexity bounds. To this purpose, we use a certain abstraction technique from (non)-tree models to tree structures. This technique turns out to be applicable also for tableau algorithms: we have used it to devise a tableau algorithm for the extension of (a restriction of) SHIQ with nominals.

@thesis{ Sat-Hab-2003,
  address = {Dresden, Germany},
  author = {Ulrike {Sattler}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Description Logics for Ontologies},
  type = {Habilitation Thesis},
  year = {2003},
}