Theses

Many real-world processes, like the weather, are time-dependent, a dimension to data that is not widely supported in ontology-based representations. Therefore, this thesis is dedicated to implementing the reasoning algorithm from Borgwardt, Forkel, and Kovtunova, which decides entailment for TELH(♢,lhs)⊥, a lightweight and tractable temporal description logic, in the Datalog-based rule engine Nemo. The implementation works on normalised ontologies specified in a temporalised sublanguage of OWL 2 EL. Furthermore, the implementation is evaluated on an ontology using real-world weather data, which shows promising results but also suggests specific optimisations to make reasoning viable on large datasets.

@thesis{ Hosc-24,
  address = {Dresden, Germany},
  author = {Timon Bertold {Hoschke}},
  school = {Technische Universit{\"a}t Dresden},
  title = {Efficient Reasoning for Lightweight Temporal Description Logics},
  type = {Bachelor's Thesis},
  year = {2024},
}

The role-based paradigm has been introduced for the design of adaptive and context sensitive software systems. Naturally, a system built on top of the paradigm is expected to thrive in dynamic environments. In consequence, reasoning services over temporal aspect are essential in such a system. To represent context-dependent domains, various extensions of Description Logics (DLs) with context are introduced and studied. We focus on the family of Contextualized Description Logics (ConDLs) that have been shown capable to represent role-based modelling languages while retaining decidability. However, reasoning problems over dynamic settings under the logics are rather unexplored.

@thesis{ Tirtarasa-Diss-2023,
  address = {Dresden, Germany},
  author = {Satyadharma {Tirtarasa}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Context-Sensitive Description Logics in Dynamic Settings},
  type = {Doctoral Thesis},
  year = {2023},
}

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 \(\mathcal{ALC}\) in the presence of GCIs, quite strong restrictions, called \(\omega\)-admissibility, were imposed on the concrete domain. On the one hand, we generalize the notion of \(\omega\)-admissibility from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate \(\omega\)-admissibility to well-known notions from model theory. In particular, we show that finitely bounded homogeneous structures yield \(\omega\)-admissible concrete domains. This allows us to show \(\omega\)-admissibility of concrete domains using existing results from model theory. When integrating concrete domains into lightweight DLs of the \(\mathcal{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 \(\omega\)-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 \(\mathcal{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 \(\mathcal{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 \(\omega\)-admissible concrete domains with at most binary predicates. The bad news is that defining \(\omega\)-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.

@thesis{ Rydval-Diss-2022,
  address = {Dresden, Germany},
  author = {Jakub {Rydval}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains},
  type = {Doctoral Thesis},
  year = {2022},
}

Description logics (DLs) are a family of formal knowl- edge representation languages used in artificial intelligence to describe and reason about the concepts of an application domain. In particular, they are providing formalization for ontologies and the semantic web. The most specific concept (msc) is an inference task that can support the bottom-up construction of knowledge bases in description logics. The most specific concept of an individual is the least concept that has this individual as an instance. In description logics which contain existential restrictions, the most specific concept does not always exist in the case of acyclic ABoxes. However, the latest results show that the existence of the msc w.r.t. an individual can be decided in polynomial time. Also, the role-depth of these most specific generalizations is polynomially bounded by the size of the input, which yields a decision procedure for the existence problem. The polynomial bound can be used to compute the msc if it exists. Otherwise, the computed concept can still serve as an approximation. However, computing the msc could take at least exponential time if the msc is exponentially large. Also, the previous approach does not make it clear how to compute the most specific concept in practice. First, we revisit the previous approach for constructing the msc of an individual w.r.t. a general EL-TBox. We present a new method for tree unravelling of an interpretation and introduce a characteristic concept w.r.t. the least tree unravelling. Moreover, we provide a new approach and an algorithm to decide the existence of the msc in polynomial time without relying on computing the concept. Then, one can compute the actual msc in exponential time. Finally, we provide an experimental evaluation to state that the concept constructed from the new approach has a smaller bound than the bound of the concept constructed from the previous approach.

@thesis{ Nad-22,
  address = {Dresden, Germany},
  author = {Mohamed {Nadeem}},
  school = {Technische Universit{\"a}t Dresden},
  title = {A Polynomial Approach for Finding Most Specific Concepts w.r.t General {$\mathcal{EL}$}-TBoxes},
  type = {Master's Thesis},
  year = {2022},
}

In the research field of Description Logics (DLs) checking satisfiability of ALCQ has been investigated thoroughly and is therefore well-known. The DL ALCSCC extends ALCQ with constraints over role successors using quantifier-free fragments (QF) of Boolean Algebra (BA) and Presburger Arithmetics (PA). Checking satisfiability of this DL has been proven to be decidable and PSpace-complete. In this work we provide a tableau algorithm to check satisfiability of ALCSCC concepts and prove its correctness.

@thesis{ Khy-21,
  address = {Dresden, Germany},
  author = {Ryny {Khy}},
  school = {Technische Universit{\"a}t Dresden},
  title = {A Tableau Algorithm for the Numerical Description Logic {$\mathcal{ALCSCC}$}},
  type = {Master's Thesis},
  year = {2021},
}

Description Logics are used in a range of different fields. The main research areas study the applications, extensions and their complexity. This thesis is dedicated to evaluate the quality of models for Description Logics. For this purpose, it is shown how weighted alternating tree automata can be used to measure features of models. Afterwards, based on these automata, methods are proposed to enforce features of models to given thresholds. Finally, an alternating tree automaton is defined which accepts exactly those models that conform to the given feature restrictions.

@thesis{ Krud-21,
  address = {Dresden, Germany},
  author = {Jakob {Krude}},
  school = {Technische Universit{\"a}t Dresden},
  title = {Measuring Description Logic Models using Weighted Tree Automata},
  type = {Bachelor's Thesis},
  year = {2021},
}

Ontology-mediated query answering is a popular paradigm for enriching answers to user queries with background knowledge. For querying the absence of information, however, there exist only few ontology-based approaches. Moreover, these proposals conflate the closed-domain and closed-world assumption, and therefore are not suited to deal with the anonymous objects that are common in ontological reasoning. Many real-world applications, like processing electronic health records (EHRs), also contain a temporal dimension, and require efficient reasoning algorithms. Moreover, since medical data is not recorded on a regular basis, reasoners must deal with sparse data with potentially large temporal gaps. Our contribution consists of three main parts: Firstly, we introduce a new closed-world semantics for answering conjunctive queries with negation over ontologies formulated in the description logic ELH⊥, which is based on the minimal universal model. We propose a rewriting strategy for dealing with negated query atoms, which shows that query answering is possible in polynomial time in data complexity. Secondly, we introduce a new temporal variant of ELH⊥ that features a convexity operator. We extend this minimal-world semantics for answering metric temporal conjunctive queries with negation over the logic and obtain similar rewritability and complexity results. Thirdly, apart from the theoretical results, we evaluate minimal-world semantics in practice by selecting patients, based on their EHRs, that match given criteria.

@thesis{ Forkel-Diss-20,
  address = {Dresden, Germany},
  author = {Walter {Forkel}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Closed-World Semantics for Query Answering in Temporal Description Logics},
  type = {Doctoral Thesis},
  year = {2020},
}

The reasoning task of a temporal version of ontology-based data access can be solved with the help of a bounded history encoding (BHE). By rewriting temporal queries, the reasoning task can be reduced to query answering over temporal databases. The BHE under consideration in this work is one approach to solve this task [1]. In this thesis, an implementation of this BHE is evaluated, to investigate its helpfulness in a practical application. Criteria to assess the degree of helpfulness are the size of the encoding, the time it takes to answer one query per time point, and the usefulness of the answers. The BHE is applied to observe an online automotive marketplace and then to answer a set of specified queries at each time point. The queries were explicitly chosen to help evaluate the BHE's degree of helpfulness. To provide useful answers, the BHE had to be extended by appropriate operators. The evaluation of the extended BHE shows that it can provide useful answers in reasonable time. An upper bound was found for the size of the encoding, which determines from what number of time points on the BHE is superior.

@thesis{ Nebe-Bac-20,
  address = {Dresden, Germany},
  author = {Thure {Nebendahl}},
  school = {Technische Universit{\"a}t Dresden},
  title = {Experimental Evaluation of a Bounded History Encoding},
  type = {Bachelor's Thesis},
  year = {2020},
}

Description Logic (abbrv. DL) belongs to the field of knowledge representation and reasoning. DL researchers have developed a large family of logic-based languages, so-called description logics (abbrv. DLs). These logics allow their users to explicitly represent knowledge as ontologies, which are finite sets of (human- and machine-readable) axioms, and provide them with automated inference services to derive implicit knowledge. The landscape of decidability and computational complexity of common reasoning tasks for various description logics has been explored in large parts: there is always a trade-off between expressibility and reasoning costs. It is therefore not surprising that DLs are nowadays applied in a large variety of domains: agriculture, astronomy, biology, defense, education, energy management, geography, geoscience, medicine, oceanography, and oil and gas. Furthermore, the most notable success of DLs is that these constitute the logical underpinning of the Web Ontology Language (abbrv. OWL) in the Semantic Web.

Formal Concept Analysis (abbrv. FCA) is a subfield of lattice theory that allows to analyze data-sets that can be represented as formal contexts. Put simply, such a formal context binds a set of objects to a set of attributes by specifying which objects have which attributes. There are two major techniques that can be applied in various ways for purposes of conceptual clustering, data mining, machine learning, knowledge management, knowledge visualization, etc. On the one hand, it is possible to describe the hierarchical structure of such a data-set in form of a formal concept lattice. On the other hand, the theory of implications (dependencies between attributes) valid in a given formal context can be axiomatized in a sound and complete manner by the so-called canonical base, which furthermore contains a minimal number of implications w.r.t. the properties of soundness and completeness.

In spite of the different notions used in FCA and in DLs, there has been a very fruitful interaction between these two research areas. My thesis continues this line of research and, more specifically, I will describe how methods from FCA can be used to support the automatic construction and extension of DL ontologies from data.

@thesis{ Kriegel-Diss-2019,
  address = {Dresden, Germany},
  author = {Francesco {Kriegel}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Constructing and Extending Description Logic Ontologies using Methods of Formal Concept Analysis},
  type = {Doctoral Thesis},
  year = {2019},
}

Unification in description logics (DLs) has been introduced as a novel inference service that can be used to detect redundancies in ontologies, by finding different concepts that may potentially stand for the same intuitive notion. Together with the special case of matching, they were first investigated in detail for the DL FL0, where these problems can be reduced to solving certain language equations. In this thesis, we extend this service in two directions. In order to increase the recall of this method for finding redundancies, we introduce and investigate the notion of approximate unification, which basically finds pairs of concepts that “almost” unify, in order to account for potential small modelling errors. The meaning of “almost” is formalized using distance measures between concepts. We show that approximate unification in FL0 can be reduced to approximately solving language equations, and devise algorithms for solving the latter problem for particular distance measures. Furthermore, we make a first step towards integrating background knowledge, formulated in so-called TBoxes, by investigating the special case of matching in the presence of TBoxes of different forms. We acquire a tight complexity bound for the general case, while we prove that the problem becomes easier in a restricted setting. To achieve these bounds, we take advantage of an equivalence characterization of FL0 concepts that is based on formal languages. In addition, we incorporate TBoxes in computing concept distances. Even though our results on the approximate setting cannot deal with TBoxes yet, we prepare the framework that future research can build on. Before we journey to the technical details of the above investigations, we showcase our program in the simpler setting of the equational theory ACUI, where we are able to also combine the two extensions. In the course of studying the above problems, we make heavy use of automata theory, where we also derive novel results that could be of independent interest.

@thesis{ Marantidis-Diss-2019,
  address = {Dresden, Germany},
  author = {Pavlos {Marantidis}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Quantitative Variants of Language Equations and their Applications to Description Logics},
  type = {Doctoral Thesis},
  year = {2019},
}

A rise in the number of ontologies that are integrated and distributed in numerous application systems may provide the users to access the ontologies with different privileges and purposes. In this situation, preserving confidential information from possible unauthorized disclosures becomes a critical requirement. For instance, in the clinical sciences, unauthorized disclosures of medical information do not only threaten the system but also, most importantly, the patient data. Motivated by this situation, this thesis initially investigates a privacy problem, called the identity problem, where the identity of (anonymous) objects stored in Description Logic ontologies can be revealed or not. Then, we consider this problem in the context of role-based access control to ontologies and extend it to the problem asking if the identity belongs to a set of known individuals of cardinality smaller than the number k. If it is the case that some confidential information of persons, such as their identity, their relationships or their other properties, can be deduced from an ontology, which implies that some privacy policy is not fulfilled, then one needs to repair this ontology such that the modified one complies with the policies and preserves the information from the original ontology as much as possible. The repair mechanism we provide is called gentle repair and performed via axiom weakening instead of axiom deletion which was commonly used in classical approaches of ontology repair. However, policy compliance itself is not enough if there is a possible attacker that can obtain relevant information from other sources, which together with the modified ontology still violates the privacy policies. Safety property is proposed to alleviate this issue and we investigate this in the context of privacy-preserving ontology publishing. Inference procedures to solve those privacy problems and additional investigations on the complexity of the procedures, as well as the worst-case complexity of the problems, become the main contributions of this thesis.

@thesis{ Nuradiansyah-Diss-2019,
  address = {Dresden, Germany},
  author = {Adrian {Nuradiansyah}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Reasoning in Description Logic Ontologies for Privacy Management},
  type = {Doctoral Thesis},
  year = {2019},
}

Description Logics (DLs) are increasingly successful knowledge representation formalisms, useful for any application requiring implicit derivation of knowledge from explicitly known facts. A prominent example domain benefiting from these formalisms since the 1990s is the biomedical field. This area contributes an intangible amount of facts and relations between low- and high-level concepts such as the constitution of cells or interactions between studied illnesses, their symptoms and remedies. DLs are well-suited for handling large formal knowledge repositories and computing inferable coherences throughout such data, relying on their well-founded first-order semantics. In particular, DLs of reduced expressivity have proven a tremendous worth for handling large ontologies due to their computational tractability. In spite of these assets and prevailing influence, classical DLs are not well-suited to adequately model some of the most intuitive forms of reasoning. The capability for abductive reasoning is imperative for any field subjected to incomplete knowledge and the motivation to complete it with typical expectations. When such default expectations receive contradicting evidence, an abductive formalism is able to retract previously drawn, conflicting conclusions. Common examples often include human reasoning or a default characterisation of properties in biology, such as the normal arrangement of organs in the human body. Treatment of such defeasible knowledge must be aware of exceptional cases - such as a human suffering from the congenital condition situs inversus - and therefore accommodate for the ability to retract defeasible conclusions in a non-monotonic fashion. Specifically tailored non-monotonic semantics have been continuously investigated for DLs in the past 30 years. A particularly promising approach, is rooted in the research by Kraus, Lehmann and Magidor for preferential (propositional) logics and Rational Closure (RC). The biggest advantages of RC are its well-behaviour in terms of formal inference postulates and the efficient computation of defeasible entailments, by relying on a tractable reduction to classical reasoning in the underlying formalism. A major contribution of this work is a reorganisation of the core of this reasoning method, into an abstract framework formalisation. This framework is then easily instantiated to provide the reduction method for RC in DLs as well as more advanced closure operators, such as Relevant or Lexicographic Closure. In spite of their practical aptitude, we discovered that all reduction approaches fail to provide any defeasible conclusions for elements that only occur in the relational neighbourhood of the inspected elements. More explicitly, a distinguishing advantage of DLs over propositional logic is the capability to model binary relations and describe aspects of a related concept in terms of existential and universal quantification. Previous approaches to RC (and more advanced closures) are not able to derive typical behaviour for the concepts that occur within such quantification. The main contribution of this work is to introduce stronger semantics for the lightweight DL EL_bot with the capability to infer the expected entailments, while maintaining a close relation to the reduction method. We achieve this by introducing a new kind of first-order interpretation that allocates defeasible information on its elements directly. This allows to compare the level of typicality of such interpretations in terms of defeasible information satisfied at elements in the relational neighbourhood. A typicality preference relation then provides the means to single out those sets of models with maximal typicality. Based on this notion, we introduce two types of nested rational semantics, a sceptical and a selective variant, each capable of deriving the missing entailments under RC for arbitrarily nested quantified concepts. As a proof of versatility for our new semantics, we also show that the stronger Relevant Closure, can be imbued with typical information in the successors of binary relations. An extensive investigation into the computational complexity of our new semantics shows that the sceptical nested variant comes at considerable additional effort, while the selective semantics reside in the complexity of classical reasoning in the underlying DL, which remains tractable in our case.

@thesis{ Pensel-Diss-2019,
  address = {Dresden, Germany},
  author = {Maximilian {Pensel}},
  school = {Technische Universit\"{a}t Dresden},
  title = {A Lightweight Defeasible Description Logic in Depth: Quantification in Rational Reasoning and Beyond},
  type = {Doctoral Thesis},
  year = {2019},
}

Recent research in the field of Description Logic (DL) investigated the complexity of the satisfiability problem for description logics that are obtained by enriching the well-known DL ALCQ with more complex set and cardinality constraints over role successors. The algorithms that have been proposed so far, despite providing worst-case optimal decision procedures for the concept satisfiability problem (both without and with a terminology) lack the efficiency needed to obtain usable implementations. In particular, the algorithm for the case without terminology is non-deterministic and the one for the case with a terminology is also best-case exponential. The goal of this thesis is to use well-established techniques from the field of numerical optimization, such as column generation, in order to obtain more practical algorithms. As a starting point, efficient approaches for dealing with counting quantifiers over unary predicates based on SAT-based column generation should be considered.

@thesis{ DeBo-Mas-19,
  address = {Dresden, Germany},
  author = {Filippo {De Bortoli}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Integrating Reasoning Services for Description Logics with Cardinality Constraints with Numerical Optimization Techniques},
  type = {Master's Thesis},
  year = {2019},
}

@thesis{ Kes-Bac-19,
  address = {Dresden, Germany},
  author = {Christian {Kesting}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Weakening Relations for Gently Repairing Ontologies},
  type = {Bachelor's Thesis},
  year = {2019},
}

@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},
}

In a modern world software systems are literally everywhere. These should cope with very complex scenarios including the ability of context-awareness and self-adaptability. The concept of roles provide the means to model such complex, context-dependent systems. In role-based systems, the relational and context-dependent properties of objects are transferred into the roles that the object plays in a certain context. However, even if the domain can be expressed in a well-structured and modular way, role-based models can still be hard to comprehend due to the sophisticated semantics of roles, contexts and different constraints. Hence, unintended implications or inconsistencies may be overlooked. A feasible logical formalism is required here. In this setting Description Logics (DLs) fit very well as a starting point for further considerations since as a decidable fragment of first-order logic they have both an underlying formal semantics and decidable reasoning problems. DLs are a well-understood family of knowledge representation formalisms which allow to represent application domains in a well-structured way by DL-concepts, i.e. unary predicates, and DL-roles, i.e. binary predicates. However, classical DLs lack expressive power to formalise contextual knowledge which is crucial for formalising role-based systems. We investigate a novel family of contextualised description logics that is capable of expressing contextual knowledge and preserves decidability even in the presence of rigid DL-roles, i.e. relational structures that are context-independent. For these contextualised description logics we thoroughly analyse the complexity of the consistency problem. Furthermore, we present a mapping algorithm that allows for an automated translation from a formal role-based model, namely a Compartment Role Object Model (CROM), into a contextualised DL ontology. We prove the semantical correctness and provide ideas how features extending CROM can be expressed in our contextualised DLs. As final step for a completely automated analysis of role-based models, we investigate a practical reasoning algorithm and implement the first reasoner that can process contextual ontologies.

@thesis{ Boehme-Diss-2017,
  address = {Dresden, Germany},
  author = {Stephan {B\"{o}hme}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Context Reasoning for Role-Based Models},
  type = {Doctoral Thesis},
  year = {2017},
}

Probabilistic data and knowledge bases are becoming increasingly important in academia and industry. They are continuously extended with new data, powered by modern information extraction tools that associate probabilities with knowledge base facts. The state of the art to store and process such data is founded on probabilistic database systems, which are widely and successfully employed. Beyond all the success stories, however, such systems still lack the fundamental machinery to convey some of the valuable knowledge hidden in them to the end user, which limits their potential applications in practice. In particular, in their classical form, such systems are typically based on strong, unrealistic limitations, such as the closed-world assumption, the closed-domain assumption, the tuple-independence assumption, and the lack of commonsense knowledge. These limitations do not only lead to unwanted consequences, but also put such systems on weak footing in important tasks, querying answering being a very central one. In this thesis, we enhance probabilistic data and knowledge bases with more realistic data models, thereby allowing for better means for querying them. Building on the long endeavor of unifying logic and probability, we develop different rigorous semantics for probabilistic data and knowledge bases, analyze their computational properties and identify sources of (in)tractability and design practical scalable query answering algorithms whenever possible. To achieve this, the current work brings together some recent paradigms from logics, probabilistic inference, and database theory.

@thesis{ Ceylan-Diss-2017,
  address = {Dresden, Germany},
  author = {{\.I}smail {\.I}lkan {Ceylan}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Query Answering in Probabilistic Data and Knowledge Bases},
  type = {Doctoral Thesis},
  year = {2017},
}

Ontology-based data access (OBDA) augments classical query answering in databases by including domain knowledge provided by an ontology. An ontology captures the terminology of an application domain and describes domain knowledge in a machine-processable way. Formal ontology languages additionally provide semantics to these specifications. Systems for OBDA thus may apply logical reasoning to answer queries; they use the ontological knowledge to infer new information, which is only implicitly given in the data. Moreover, they usually employ the open-world assumption, which means that knowledge not stated explicitly in the data or inferred is neither assumed to be true nor false. Classical OBDA regards the knowledge however only w.r.t. a single moment, which means that information about time is not used for reasoning and hence lost; in particular, the queries generally cannot express temporal aspects. We investigate temporal query languages that allow to access temporal data through classical ontologies. In particular, we study the computational complexity of temporal query answering regarding ontologies written in lightweight description logics, which are known to allow for efficient reasoning in the atemporal setting and are successfully applied in practice. Furthermore, we present a so-called rewritability result for ontology-based temporal query answering, which suggests ways for implementation. Our results may thus guide the choice of a query language for temporal OBDA in data-intensive applications that require fast processing, such as context recognition.

@thesis{ Thost-Diss-2017,
  address = {Dresden, Germany},
  author = {Veronika {Thost}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Using Ontology-Based Data Access to Enable Context Recognition in the Presence of Incomplete Information},
  type = {Doctoral Thesis},
  year = {2017},
}

Golog is a powerful programming language for logic-based agents. The primitives of the language are actions whose preconditions and effects are defined in a Situation Calculus action theory using first-order logic. To describe possible courses of actions the programmer can freely combine imperative control structures with constructs for non-deterministic choice, leaving it to the system to resolve the non-determinism in a suitable manner. Golog has been successfully used for high-level decision making in the area of cognitive robotics. Obviously, it is important to verify certain properties of a Golog program before executing it on a physical robot. However, due to the high expressiveness of the language the verification problem is in general undecidable. In this thesis, we study the verification problem for Golog programs over actions defined in action languages based on Description Logics and explore the boundary between decidable and undecidable fragments.

@thesis{ Zarriess-Diss-2017,
  address = {Dresden, Germany},
  author = {Benjamin {Zarrie{\ss}}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Verification of Golog Programs over Description Logic Actions},
  type = {Doctoral Thesis},
  year = {2017},
}

In der Beschreibungslogik FL0 stellt das Entscheiden von Subsumptionsrelationen bzgl. genereller TBoxen ein EXPTIME vollständiges Problem dar, wie auch in der ausdrucksstärkeren Beschreibungslogik ALC. Diese Arbeit beschäftigt sich mit dem Entwurf und der konkreten Implementierung eines Systems, welches Subsumption in FL0 entscheidet. Die Grundlage hierfür bildet ein 2015 von Maximilian Pensel vorgeschlagener Algorithmus. Im Vergleich mit etablierten ALC Reasonern stellt sich diese Implementierung als nicht nachteilhaft im Entscheiden von Subsumptionsrelationen und als überlegen im Finden der Subsumierermenge heraus.

@thesis{ Mic-Bac-17,
  address = {Dresden, Germany},
  author = {Friedrich {Michel}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Entwurf und Implementierung eines Systems zur Entscheidung von Subsumption in der Beschreibungslogik FL0},
  type = {Bachelor's Thesis},
  year = {2017},
}

@mastersthesis{ Stu-Bac-17,
  address = {Dresden, Germany},
  author = {Dominik {Sturm}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Modellierung molekularbiologischer Prozesse mittels P-Automaten},
  type = {Bachelor's Thesis},
  year = {2017},
}

Description Logics (DLs) are a family of logic-based knowledge representation languages used to describe the knowledge of an application domain and reason about it in formally well-defined way. They allow users to describe the important notions and classes of the knowledge domain as concepts, which formalize the necessary and sufficient conditions for individual objects to belong to that concept. A variety of different DLs exist, differing in the set of properties one can use to express concepts, the so-called concept constructors, as well as the set of axioms available to describe the relations between concepts or individuals. However, all classical DLs have in common that they can only express exact knowledge, and correspondingly only allow exact inferences. Either we can infer that some individual belongs to a concept, or we can't, there is no in-between. In practice though, knowledge is rarely exact. Many definitions have their exceptions or are vaguely formulated in the first place, and people might not only be interested in exact answers, but also in alternatives that are "close enough".

This thesis is aimed at tackling how to express that something "close enough", and how to integrate this notion into the formalism of Description Logics. To this end, we will use the notion of similarity and dissimilarity measures as a way to quantify how close exactly two concepts are. We will look at how useful measures can be defined in the context of DLs, and how they can be incorporated into the formal framework in order to generalize it. In particular, we will look closer at two applications of thus measures to DLs: Relaxed instance queries will incorporate a similarity measure in order to not just give the exact answer to some query, but all answers that are reasonably similar. Prototypical definitions on the other hand use a measure of dissimilarity or distance between concepts in order to allow the definitions of and reasoning with concepts that capture not just those individuals that satisfy exactly the stated properties, but also those that are "close enough".

@thesis{ Ecke-PhD-2016,
  address = {Dresden, Germany},
  author = {Andreas {Ecke}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Quantitative Methods for Similarity in Description Logics},
  type = {Doctoral Thesis},
  year = {2016},
}

Finite tree automata consist of a set of states and a set of transitions. Input trees are accepted if it is possible to label the tree with states such that the relationship between the state at every node and the state at its child nodes conforms to a transition. Thus, the transitions only define how a state must be labeled with respect to its children or vice versa.

This work investigates how finite tree automata behave when transitions are made more expressive. Two extensions are considered: a new finite tree automaton model with transitions of arbitrary size and a model where a regular tree language defines the set of transitions. The first extension allows transitions in the shape of trees to have any size. The main difference to conventional tree automata is that larger transitions can overlap. Nevertheless, the new tree automaton model has the same expressive power as conventional tree automata models. The main challenge of the provided proof is eliminating overlappings.

The second extension contains a separate tree automaton called the transition automaton. The language recognized by the transition automaton defines the set of transitions. Consequently, transitions are no longer bounded in size and amount. Nevertheless, this second tree automaton model is not more expressive than conventional models. A constructive proof is provided that uses a conventional tree automaton for simulating the extended tree automaton together with its transition automaton.

@thesis{ Dzi-Mas-16,
  address = {Dresden, Germany},
  author = {Sven {Dziadek}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Tree Automata with Generalized Transition Relations},
  type = {Master's Thesis},
  year = {2016},
}

Metta et al. introduced the concept of Spiking Neural systems with cooperating rules, bringing the ideas behind cooperating distributed grammar systems (CD grammar systems) to the world of Spiking Neural P systems (SN P systems), a model for computation inspired by the functioning of neurons in a nervous system. An essential feature in these systems is the cooperation of multiple components according to some fixed cooperation protocol. We provide a comprehensive introduction to the theory of these systems, as well as an overview of the underlying models of both CD grammar systems and SN P systems. Building on the proof by Metta et al. for the terminating protocol, we show that universality can be retained for the other cooperation protocols by slightly lifting some of the model's restrictions, such as using the maximally parallel mode of derivation instead of the strongly sequential mode, or allowing for local synchronization in the asynchronous case. We present a concrete example demonstrating the power of the model by generating a non-semi-linear (and hence non-context-free) set of numbers, and contrast it with a CD grammar system generating the same set. We conclude by listing some remaining open questions and opportunities for further research in the area.

@thesis{ Mar-Dip-16,
  address = {Dresden, Germany},
  author = {Maximilian {Marx}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Universality Results for Spiking Neural P Systems with Cooperating Rules},
  type = {Diploma Thesis},
  year = {2016},
}

Generalizations of a collection of concepts can be computed by the least common subsumer (lcs) which is a useful inference for building knowledge bases. For general FL0-TBoxes the lcs need not exist. In this thesis, we devise a condition to check whether a concept is the lcs of two concepts w.r.t. a general FL0-TBox. We also define the characterizations for the existence of the lcs. Last, we show that if the lcs exists, then we can compute the lcs and the upper bound for the role-depth of the lcs.

@thesis{ Nur-Mas-16,
  address = {Dresden, Germany},
  author = {Adrian {Nuradiansyah}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Algorithms for Computing Least Common Subsumers w.r.t. General FL0-TBoxes},
  type = {Master's Thesis},
  year = {2016},
}

Decidability of First Order Logic (FOL) is a key and active research area in logic and computer science. As FOL is undecidable in its general form, a lot of research is focused on finding classes of FOL which are decidable and studying their properties. In this thesis, we work on one such decidable fragment that only allows monadic predicate and function symbols (with the exception of one constant). We also allow just one variable in the formulas.
Research in Logic generally does not concentrate on the finiteness of interpretations. Yet, for any realistic and practical knowledge representation purpose we only have finitely many resources to represent the real world. Therefore we focus on finding the finite Herbrand models for the above mentioned class. We also provide a terminating decision procedure for the existence of a finite Herbrand model for this restricted fragment of FOL. In the end we provide some optimizations and variants of the original algorithm for better performance on certain problems.

@thesis{ Masters_Thesis_Zia,
  address = {Dresden, Germany},
  author = {Muhammad Zahid {Zia}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Finite Herbrand Models for Monadic Clauses with Unary Function Symbols},
  type = {Master's Thesis},
  year = {2016},
}

Die vorliegende Bachelorarbeit beschäftigt sich mit Splicing-P-Systemen, einer Zusammenführung der aus dem Membrane-Computing stammenden P-Systeme mit den dem DNA-Computing zuzuordnenden H-Systemen. Dazu werden alle genannten Systeme vorgestellt und für verschiedene Klassen von Splicing-P-Systemen Resultate zur Berechenbarkeit gegeben. Diese werden in den Kontext vergleichbarer Resultate für H-Systeme eingeordnet. Abschließend gibt die Behandlung des NP-vollständigen Hamiltonkreis-Problems in polynomieller Zeit ein Beispiel für die Anwendung und Leistungsfähigkeit von Splicing-P-Systemen.

@thesis{ Ran-Bac-16,
  address = {Dresden, Germany},
  author = {Benjamin {Range}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Splicing-P-Systeme},
  type = {Bachelor's Thesis},
  year = {2016},
}

@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},
}

Description Logics (DL) are a well investigated family of logics for knowledge representation. Concept Similarity Measures (CSM) are functions that assess the similarity of pairs of concepts. The Simi-Framework provides several CSMs for the widely used DL EL, which fulfills certain formal properties. We will expand this framework to value restrictions, disjunction, and even a primitive negation. For these new and EL constructors, we investigate the conditions under which the resulting CSMs do or do not fulfill the formal properties. By the use of Formal Concept Analysis (FCA) we can determine the formal properties for a multitude of constructor sets and relations between the formal properties, that hold within our expansion. We also were able to prove some of them for more general cases.

@thesis{ Lae-Dip-15,
  address = {Dresden, Germany},
  author = {Paul {L\"{a}tsch}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Simi-Framework for Concept-Similarity-Measures: property analysis and expansion to more powerful Description Logics},
  type = {Diploma Thesis},
  year = {2015},
}

In description logic (DL) based knowledge representation and reasoning systems it is always important to weigh expressivity against computational tractability. Sometimes theoretical investigations towards the complexity of reasoning are only weak indicators for realistic algorithmic performances. For an example, special purpose algorithms for reasoning in certain exponential extensions of the otherwise polynomial lightweight DL EL have been shown to behave very well in practice. For the DL FL0, deciding subsumption w.r.t. general concept inclusions is known to be EXPTIME-complete, just like in the considerably more expressive DL ALC. We take on the task of deciding subsumption in FL0 with general concept inclusions by a special purpose algorithm, as an alternative to the employment of non-deterministic tableaux algorithms for ALC. Motivated by the realistic performance results for reasoning with exponential EL extensions, we claim that this algorithm may yield a similar computational behaviour. Due to the characteristics of FL0, we are able to consider an automata-based approach to devise such a practical subsumption algorithm. As a side result, we are able to show a correlation between subsumption in FL0 with general TBoxes and FLreg, an extension of FL0 with several role constructors. Subsequent to our work it remains to implement the algorithm and evaluate its performance within realistic test scenarios.

@thesis{ Pen-Mas-15,
  address = {Dresden, Germany},
  author = {Maximilian {Pensel}},
  school = {Technische Universit\"{a}t Dresden},
  title = {An Automata Based Approach for Subsumption w.r.t. General Concept Inclusions in the Description Logic FL0},
  type = {Master's Thesis},
  year = {2015},
}

Ontologies, which form the core of Semantic Web systems, need to evolve to meet the changing needs of the system and its users. The dynamic nature of ontology development has motivated the formal study of ontology evolution problems, which is one of the important problems in the current Semantic Web research. Ontology evolution approaches suffer from intrinsic information loss. The current study deals with the problem of minimizing information loss during iterative ontology update. It provides a framework combining the ontology evolution tasks with context-based reasoning method. Using this framework, all the solutions obtained in an ontology evolution task, which are partly redundant, can be described as contexts and compactly represented in a single labelled ontology. Further updates and reasoning can be done on this ontology efficiently. We propose new approaches to do ontology contraction, ontology expansion and ontology revision using context-based reasoning method. These approaches show how ontology evolution can be done with minimum information loss by using all the solutions obtained at every stage of the evolution task, efficiently using our framework. We also propose theoretical methods to extract the optimal solutions from the ontology obtained as the result of iterative ontology update. We show that, optimal solutions in the intermediate stages of iterative ontology update may not be the optimal solutions in the result obtained at the end of all the stages. We handle various notions of an optimal solution: the solution which changes the semantics of the ontology as minimum as possible, the solution which contains some of the intended consequences, the solution which has the most original axioms of the ontology. We also propose theoretical methods to do context-based reasoning over the optimal solutions extracted. We present the first prototypical implementation of the theoretical methods developed in this thesis and show the preliminary results of our implementation on the real-world ontologies.

@thesis{ Master_Thesis_Aparna,
  address = {Dresden, Germany},
  author = {Aparna Saisree {Thuluva}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Iterative Ontology Update with Minimum Change},
  type = {Master's Thesis},
  year = {2015},
}

@thesis{ Pue-Bac-15,
  address = {Dresden, Germany},
  author = {Andy {P\"{u}schel}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Spiking Neural P-Systeme},
  type = {Bachelor's Thesis},
  year = {2015},
}

In der vorliegenden Arbeit wird gezeigt, wie zwei unkonventionelle Berechnungsmodelle sinnvoll zu einem hybriden System kombiniert werden können: Membran- und Quantenrechner. Das beschriebene Modell basiert dabei auf einem P-System, in dem ausgewiesene Membranen Quantenschaltkreise enthalten, und hat zum Ziel, inhärente Nachteile beider Berechnungsmodelle zu kompensieren. Anhand einer konkreten Anwendung wird die Funktionsweise hybrider Systeme ausführlich demonstriert.

@thesis{ Sch-Bac-15,
  address = {Dresden, Germany},
  author = {Timo {Schick}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Hybrides Membrane-Quantum Computing},
  type = {Bachelor's 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},
}

Description logics (DLs) are used to represent knowledge of an application domain and provide standard reasoning services to infer consequences of this knowledge. However, classical DLs are not suited to represent vagueness in the description of the knowledge. We consider a combination of DLs and Fuzzy Logics to address this task. In particular, we consider the t-norm-based semantics for fuzzy DLs introduced by Hajek in 2005. Since then, many tableau algorithms have been developed for reasoning in fuzzy DLs. Another popular approach is to reduce fuzzy ontologies to classical ones and use existing highly optimized classical reasoners to deal with them. However, a systematic study of the computational complexity of the different reasoning problems is so far missing from the literature on fuzzy DLs. Recently, some of the developed tableau algorithms have been shown to be incorrect in the presence of general concept inclusion axioms (GCIs). In some fuzzy DLs, reasoning with GCIs has even turned out to be undecidable. This work provides a rigorous analysis of the boundary between decidable and undecidable reasoning problems in t-norm-based fuzzy DLs, in particular for GCIs. Existing undecidability proofs are extended to cover large classes of fuzzy DLs, and decidability is shown for most of the remaining logics considered here. Additionally, the computational complexity of reasoning in fuzzy DLs with semantics based on finite lattices is analyzed. For most decidability results, tight complexity bounds can be derived.

@thesis{ Borgwardt-Diss-2014,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Fuzzy Description Logics with General Concept Inclusions},
  type = {Doctoral Thesis},
  year = {2014},
}

Inevitably, it becomes more and more important to verify that the systems surrounding us have certain properties. This is indeed unavoidable for safety-critical systems such as power plants and intensive-care units. We refer to the term system in a broad sense: it may be man-made (e.g. a computer system) or natural (e.g. a patient in an intensive-care unit). Whereas in Model Checking it is assumed that one has complete knowledge about the functioning of the system, we consider an open-world scenario and assume that we can only observe the behaviour of the actual running system by sensors. Such an abstract sensor could sense e.g. the blood pressure of a patient or the air traffic observed by radar.

Then the observed data are preprocessed appropriately and stored in a fact base. Based on the data available in the fact base, situation-awareness tools are supposed to help the user to detect certain situations that require intervention by an expert. Such situations could be that the heart-rate of a patient is rather high while the blood pressure is low, or that a collision of two aeroplanes is about to happen.

Moreover, the information in the fact base can be used by monitors to verify that the system has certain properties. It is not realistic, however, to assume that the sensors always yield a complete description of the current state of the observed system. Thus, it makes sense to assume that information that is not present in the fact base is unknown rather than false. Moreover, very often one has some knowledge about the functioning of the system. This background knowledge can be used to draw conclusions about the possible future behaviour of the system. Employing description logics (DLs) is one way to deal with these requirements. In this thesis, we tackle the sketched problem in three different contexts: (i) runtime verification using a temporalised DL, (ii) temporalised query entailment, and (iii) verification in DL-based action formalisms.

@thesis{ Lippmann-Diss-2014,
  address = {Dresden, Germany},
  author = {Marcel {Lippmann}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Temporalised Description Logics for Monitoring Partially Observable Events},
  type = {Doctoral Thesis},
  year = {2014},
}

The least common subsumer (lcs) in EL computed w.r.t. general TBoxes need not exist. Recently conditions for the existence for this kind of lcs were devised. This thesis investigates similar conditions for the case, where lcs in EL is computed w.r.t. general Horn ALC- TBoxes.

@thesis{ Abd-Mas-14,
  address = {Dresden, Germany},
  author = {Adilzhan {Abdrakhmanov}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Conditions for the Existence of the lcs of EL-concepts w.r.t. General Horn-ALC TBoxes},
  type = {Master's Thesis},
  year = {2014},
}

Based on the results in the article "Integrating Description Logics and Action Formalisms: First Results" and the accompanying technical report the projection problem is investigated in a more general setting. First we present several reasoning problems for the fragments of ALCQIO^U. From this we derive decision procedures and obtain complexity results for executability and projection of composite actions in presence of a universal role by a reduction to ABox consequence. Thereby the reduction formalism is considered from a more abstract point of view by using the effect function to define the semantics of applying actions. Furthermore we replace the ABox assertion considered in the projection problem by answering Boolean conjunctive queries within the fragments of ALCQIO. From a reduction to query entailment we obtain decision procedures and complexity results for the projection problem concerning Boolean conjunctive queries.

@thesis{ Pes-Dip-14,
  address = {Dresden, Germany},
  author = {Stephanie {Pester}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Investigations on an Action Formalism based on the Description Logic ALCQIO},
  type = {Diploma Thesis},
  year = {2014},
}

Research embracing context-sensitivity in the domain of knowledge representation (KR) has been scarce, especially when the context is uncertain. This work deals with this problem from a logic perspective and provides a framework combining Description Logics (DLs) with Bayesian Networks (BNs). We use BNs to describe contexts that are semantically linked to classical DL axioms.

As an application scenario, we consider the Bayesian extension BEL of the light-weight DL EL. We define four reasoning problems; namely, precise subsumption, positive subsumption, certain subsumption and finding the most likely context for a subsumption. We provide an algorithm that solves the precise subsumption in PSPACE. Positive subsumption is shown to be NP-complete and certain subsumption coNP-complete. We present a completion-like algorithm, which is in EXPTIME, to find the most likely context for a subsumption.

The scenario is generalised to Bayesian extensions of classic-valued, monotonic DLs. It is shown that precise entailment, positive entailment and certain entailment can be solved by generalising the algorithms developed for the corresponding reasoning problems in BEL. The complexities of these problems are shown to be bound with the complexity of entailment checking in the underlying DL, provided this is PSPACE-hard. Lastly, we discuss the problem of finding the most likely context for an entailment.

@thesis{ Cey-Mas-13,
  address = {Dresden, Germany},
  author = {\.{I}smail \.{I}lkan {Ceylan}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Context-Sensitive Bayesian Description Logics},
  type = {Master's Thesis},
  year = {2013},
}

Because of the simplicity in the structure of the Description Logic (DL) FL0, it has been commonly taken as the first example for the presentation of new notions and their associated problems. Fuzzy Description Logics extend classical Description Logics by allowing truth degrees to deal with imprecise concepts. In this work we show that in the fuzzy DL FL0 with greatest fixed-point semantics, the subsumption problem can be stated in terms of weighted automata. Furthermore, following this characterization, we show that this inference problem lies in the PSPACE-complete complexity class.

@thesis{ Ley-Mas-13,
  address = {Dresden, Germany},
  author = {Jos\'{e} A. Leyva {Galano}},
  school = {Technische Universit\"{a}t Dresden},
  title = {The Subsumption Problem for FL0 with Greatest Fixed-point Semantics},
  type = {Master's Thesis},
  year = {2013},
}

This thesis introduces fuzzy constraint systems as concrete domains in ALC. The extension of crisp constraint systems to fuzzy knowledge is performed by addition of sets of membership degrees for tuples in relations. The main goal is the proof of decidability of concept satisfiability with respect to general TBoxes for that enhanced description logic. For that purpose fuzzy concrete domains and ALC are restricted in several ways. The approach given in a paper by Lutz and Milicic on ALC(D) with crisp constraint systems inspired the adaptation and application of omega-admissibility and the overall proving method on fuzzy constraint systems. We present a detailed definition of the fuzzy extension of constraint systems, their integration into ALC, and a tableau algorithm that decides satisfiability of concepts w.r.t. general TBoxes.

@thesis{ Mer-Dip-13,
  address = {Dresden, Germany},
  author = {Dorian {Merz}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Decidability of Reasoning in ALC with Fuzzy Concrete Domains},
  type = {Diploma Thesis},
  year = {2013},
}

In software enterprise with large organizations, reduction of the time to determine the processor who should solve an issue reported by customers can accelerate software support. Formal Concept Analysis (FCA) is currntly a focused topic for analyzing large data. Applying FCA to historical records of completely processed issues can construct the rules that can be used to determine the potentially best processor for newly reported issues.

In this report we define a basis that is error tolerant, which contains rules that can deal with erroneous data, and provide the degree of recommendation for every candidate component. We implemented our approach and achieved a classification rate above 90%.

@thesis{ Wan-Mas-13,
  address = {Dresden, Germany},
  author = {Wenqian {Wang}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Error-Tolerant Direct Bases},
  type = {Master's Thesis},
  year = {2013},
}

Given the increasing number of ontologies which are independently developed, but which represent overlapping domain knowledge, there is an urgent need to integrate them. Most ontology matching methods are based on statistics. In contrast, this thesis is devoted to enhancing ontology matching by logic-based reasoning, both for mapping generation and for mapping refinement. We present a system with two components: a semantically enriched ontology matching mechanism (SEOM) and a logic-based mapping refinement procedure (LOMR).

We show experimentally that 1) SEOM generates a set of logically consistent and accurate mapping suggestions; 2) LOMR is able to improve the quality of mapping suggestions by removing logically unintended mappings while keeping the logically sound ones.

@thesis{ Wu-Mas-13,
  address = {Dresden, Germany},
  author = {Xichuan {Wu}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Enhancing Ontology Matching Using Logic-based Reasoning},
  type = {Master's Thesis},
  year = {2013},
}

In recent years, the Description Logic EL has received a significant interest. It has been shown to be useful as a knowledge representation formalism, to define large biomedical ontologies. Moreover, important inference problems like subsumption have been shown to be decidable in polynomial time in EL. In particular, unification in EL can be used to detect redundancies in big ontologies. The unification problem in EL has been shown to be an NP-complete problem even in the presence of background knowledge in the form of an acyclic TBox. Recently, the result was also extended to the case of cycle-restricted TBoxes. Unification in EL w.r.t. general TBoxes is still an open problem. Here we define a more general notion of unification problem called hybrid unification. In contrast to the usual unification problem, hybrid unification allows solutions that contain cyclic definitions of concept names. We show that hybrid unification in EL is NP complete. Furthermore, we provide a goal-oriented NP-decision procedure for the hybrid unification problem.

@thesis{ Gil-Mas-12,
  address = {Dresden, Germany},
  author = {Oliver {Fern\'{a}ndez Gil}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Hybrid Unification in the Description Logic EL},
  type = {Master's Thesis},
  year = {2012},
}

In this thesis we present similarity measures for concept descriptions in Description Logics. In many practical applications these measures are an important means to compare concept descriptions, i.e., to assess their similarity. We present several properties for similarity measures which aim to aid the evaluation of a measure and we use this properties to point out that current measures show unintuitive behaviour. For instance, some similarity measures do not yield the same values, if equivalent concepts are compared with a third one. Additionally, a similarity-measure framework for concept descriptions written in the Description Logic ELH is presented and its properties are analysed.

@thesis{ Leh-Dip-12,
  address = {Dresden, Germany},
  author = {Karsten {Lehmann}},
  school = {Technische Universit\"{a}t Dresden},
  title = {A Framework for Semantic Invariant Similarity Measures for ELH Concept Descriptions},
  type = {Diploma Thesis},
  year = {2012},
}

Physical law restricts the duplicability of certain data in quantum computations. Selinger's and Valiron's Quantum Lambda Calculus successfully copes with these restrictions by means of a linear type system that prevents implicit copying of quantum data. However, as soon as we equip this calculus with parametric polymorphism in order to obtain a system-F-like calculus, new challenges arise.

In this work we propose a polymorphically typed Quantum Lambda Calculus and investigate its characteristics. In order to implement parametric polymorphism in accordance with the laws of quantum mechanics, we employ bounded quantification: a powerful combination of the subtyping concept and universally quantified types. Supplemented with an appropriate subtype relation, bounded quantification provides the key mechanisms to enforce linearity of certain types in the presence of parametric polymorphism.

@thesis{ Voi-Dip-12,
  address = {Dresden, Germany},
  author = {Marco {Voigt}},
  school = {Technische Universit\"{a}t Dresden},
  title = {On Polymorphic Types with Enforceable Linearity for A Quantum Lambda Calculus},
  type = {Diploma Thesis},
  year = {2012},
}

Der Least Common Subsumer (LCS) in einer Beschreibungslogik wie EL ist das speziellste Konzept, das eine Reihe von Konzepten generalisiert. Bezüglich einer generellen EL-TBox existiert diese speziellste Generalisierung im Allgemeinen nicht. Daher wurden Methoden zur Approximation des LCS entwickelt.

In dieser Arbeit wird eine hinreichende und notwendige Bedingung vorgestellt, unter welcher der LCS von zwei EL-Konzepten bezüglich einer generellen EL-TBox existiert, sodass entschieden werden kann, ob eine berechnete Approximation des LCS exakt ist oder nicht. Zudem wird gezeigt, dass die Existenz des LCS in diesem Zusammenhang entscheidbar ist und, darauf aufbauend, dass eine obere Schranke für die Rollentiefe des LCS angegeben werden kann, falls der LCS existiert.

@thesis{ Zar-Dip-12,
  address = {Dresden, Germany},
  author = {Benjamin {Zarrie\ss}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Existenz des Least Common Subsumers in der Beschreibungslogik EL bez\"{u}glich genereller Terminologien},
  type = {Diploma Thesis},
  year = {2012},
}

Das DNA-Computing ist ein interdisziplinäres Gebiet, welches auf der Biochemie, Molekularbiologie und Theoretischen Informatik aufbaut und sich in den letzten Jahren äußerst rasant entwickelt hat. Dabei werden DNA-Moleküle als Speichermedium und Datenträger für Berechnungen genutzt. Die Watson-Crick-Automaten sind Automaten, welche auf doppelsträngigen Bändern lesen und eingeführt wurden, um die Leistungsfähigkeit von DNA-Molekülen zu untersuchen. Entsprechend gehört das Modell der Watson-Crick-Automaten zu dem Gebiet des DNA-Computing und soll in dieser Arbeit auf Universalität untersucht werden. Im Speziellen werden die Modelle der endlichen Watson-Crick-Automaten, der Reverse Watson-Crick-Automaten und der Watson-Crick-Transducer vorgestellt, die Sprachfamilien eingeschränkter Watson-Crick-Automaten untersucht, die Universalität der Watson-Crick-Transducer gezeigt und ein universeller Watson-Crick-Transducer konstruiert.

@thesis{ Nit-Bac-12,
  address = {Dresden, Germany},
  author = {Paul {Nitzsche}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Universalit\"{a}tsresultate f\"{u}r Watson-Crick-Automaten},
  type = {Bachelor's Thesis},
  year = {2012},
}

Da konventionelle Computing-Konzepte zunehmend auf physikalische sowie auf technische Grenzen stoßen, wurde in den vergangenen Jahren nach alternativen Computing-Konzepten gesucht, welche in der Lage sein sollen Berechnungen in kürzerer Zeit durchzuführen sowie kombinatorische Suchprobleme (NP-Probleme) mit angemessenen Ressourcenverbrauch zu lösen. Das Molecular-Computing (das Rechnen mit Molekülen) stellt hierbei ein vielversprechendes Konzept dar. Ein Teilgebiet des Molecular-Computings ist das Rechnen mit DNA-Strängen, das sog. DNA-Computing, dessen zentrales Forschungsziel die Modellierung eines universellen DNA-Computers darstellt. Insertion-Deletion-Systeme sind ein formales Modell auf dem Gebiet des DNA-Computings. Daher ist die Frage, ob diese Systeme universelle Berechnungsstärke besitzen, ein interessantes Thema, welches in der Bachelorarbeit betrachtet wurde. In der Arbeit werden Insertion-Deletion-Systeme definiert und darauf aufbauend gezeigt, dass diese Systeme universelle Berechnungsstärke besitzen.

@thesis{ Rot-Bac-12,
  address = {Dresden, Germany},
  author = {Monika {Roth}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Untersuchung der Berechnungsst\"{a}rke eines gewichteten Insertion-Deletion-Systems},
  type = {Bachelor's Thesis},
  year = {2012},
}

Description Logics (DLs) are a class of knowledge representation formalisms that can represent terminological and assertional knowledge using a well-defined semantics. Often, knowledge engineers are experts in their own fields, but not in logics, and require assistance in the process of ontology design. This thesis presents three methods that can extract terminological knowledge from existing data and thereby assist in the design process. They are based on similar formalisms from Formal Concept Analysis (FCA), in particular the Next-Closure Algorithm and Attribute-Exploration. The first of the three methods computes terminological knowledge from the data, without any expert interaction. The two other methods use expert interaction, where a human expert can confirm each terminological axiom or refute it by providing a counterexample. These two methods differ only in the way counterexamples are provided.

@thesis{ dis-diss-2011,
  address = {Dresden, Germany},
  author = {Felix {Distel}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Learning Description Logic Knowledge Bases from Data Using Methods from Formal Concept Analysis},
  type = {Doctoral Thesis},
  year = {2011},
}

Ontologies, as understood in Knowledge Representation area, are conceived as a means to represent conceptual knowledge. An ontology is typically shared between a number of users. When sharing an ontology, it is common that each user has different views, i.e. the sub-ontology that is accessible to him. However, specially for large-scale ontologies, it is a difficult task to predict which users will be able to deduce a consequence from sub-ontology they can access. A lattice-based approach has been developed for solving this problem, by computing an access label for every ontological consequence. If the knowledge engineer wants then to modify the access label of one of these consequences (e.g. make a consequence unavailable to some users), then he must find the axioms that need to be relabeled. In this work we present algorithms for finding a set of these axioms with minimal cardinality such that, when relabeled to a specified element of the lattice grant or remove access of a set of users to a consequence. These algorithms deal with some range-based access label modifications. The implementation of the algorithms is using programming language Java with Pellet as the OWL reasoner. An empirical evaluation is performed on two large-scale ontologies with different expressiveness, i.e. Snomed CT [sno] and Funct [GKL09].

@thesis{ Eld-Mas-11,
  address = {Dresden, Germany},
  author = {{Eldora}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Correcting Access Restrictions: a Range-based Approach},
  type = {Master's Thesis},
  year = {2011},
}

We consider the problem of computing the maximal truth value for a consequence derived from a set of multi-valued axioms, arranged in a total order. We extend general tableaux procedures with a labeling approach and provide sufficient conditions for termination. We also explore the issue of blocking on so-called tree tableaux and their extensions.

@thesis{ Fu-Mas-11,
  address = {Dresden, Germany},
  author = {W. {Fu}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Labeling-extensions of General Tableaux with Many Values},
  type = {Master's Thesis},
  year = {2011},
}

Description logics are a family of knowledge representation formalisms for representing and reasoning about conceptual knowledge. Every description logic system has reasoning services that infer implicit knowledge from that explicitly given. Standard reasoning problems include concept satisfiability, concept subsumption, ABox consistency and the instance problem. This thesis focuses on the concept subsumption service, which is considered to be the most common service. Some years ago, a polynomial-time algorithm for the subsumption problem in the description logic EL was developed. After that, algorithms for different problems in tractable extensions of EL have been developed. These description logics are sufficient to represent many knowledge bases, e.g. a large medical ontology called SNOMED CT. However, there are ontologies requiring extensions of EL that are not tractable. In particular, GALEN, another important medical ontology, requires ELHIfR+, an extension of EL that includes role hierarchies, inverse, functional and transitive roles. This thesis presents a classification algorithm for ELHIfR+. Together with this thesis there is an implementation available.

@thesis{ Men-Mas-11,
  address = {Dresden, Germany},
  author = {Julian Alfredo {Mendez}},
  school = {Technische Universit\"{a}t Dresden},
  title = {A Classification Algorithm For ELHIfR+},
  type = {Master's Thesis},
  year = {2011},
}

A recurring problem in many ontology based applications is delivering a huge result set for user's query causing an information overload. The reasons for this could be in-accurateness of the query provided by the user, a naive user who is not familiar with ontologies, or existence of a huge knowledge base. Though various techniques to reduce information overload are developed for web based search and Database querying, Description Logic knowledge bases are in need of customized techniques to solve this problem.

In this thesis, we present two approaches to solve the problem of information overload of conjunctive query result sets over EL++-KBs. The first approach is based on the minimal query intensification such that the new queries (called specializations) obtained are syntactically similar to the original query. The second approach is based on clustering of query results. We also implemented our two approaches in Java on top of Pellet reasoner and tested them for their effectiveness using an extended LUBM benchmark ontology.

@thesis{ Nut-Mas-11,
  address = {Dresden, Germany},
  author = {Premchand {Nutakki}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Specializing conjunctive queries in the EL-family for better comprehension of result sets},
  type = {Master's Thesis},
  year = {2011},
}

Spiking Neural P-Systeme (SN P-Systeme) als Vertreter des Natural Computing stellen ein Rechnermodell auf der Basis von Neuronen und Synapsen dar. SN P-Systeme besitzen einen hohen Grad an Parallelität, weshalb sie im Fokus aktueller Forschung an parallelen Systemen stehen. PSPACE Probleme können deterministisch in einer polynomialen Anzahl an Zeitschritten (in Hinsicht auf die Problemgröße) gelöst werden, erfordern jedoch die Vorberechnung eines exponentiell großen Systems aus Neuronen und Synapsen (genannt Workspace). In der vorliegenden Diplomarbeit wird eine biologisch motivierte Erweiterung der konventionellen SN P-Systeme vorgestellt, die es ermöglicht, auf die Vorberechnung eines exponentiellen Workspaces zu verzichten. Die erweiterten SN P-Systeme werden anschließend durch eine Lösung des Erfüllbarkeitsproblems für quantifizierte boolesche Formeln (QBF) demonstriert.

@thesis{ Sch-Dip-11,
  address = {Dresden, Germany},
  author = {Daniel {Schr\"{o}der}},
  school = {Technische Universit\"{a}t Dresden},
  title = {About Expanding Spiking Neural P Systems},
  type = {Diploma Thesis},
  year = {2011},
}

Access restrictions are essential in standard information systems and became an issue for ontologies in the following two aspects. Ontologies can represent explicit and implicit knowledge about an access policy. For this aspect we provided a methodology to represent and systematically complete role-based access control policies. Orthogonally, an ontology might be available for limited reading access. Independently of a specific ontology language or reasoner, we provided a lattice-based framework to assign labels to an ontology's axioms and consequences. We looked at the problems to compute and repair one or multiple consequence labels and to assign a query-based access restriction. An empirical evaluation has shown that the algorithms perform well in practical scenarios with large-scale ontologies.

@thesis{ kne-diss-2010,
  address = {Dresden, Germany},
  author = {Martin {Knechtel}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Access Restrictions to and with Description Logic Web Ontologies},
  type = {Doctoral Thesis},
  year = {2010},
}

Description Logics (DLs) form a family of knowledge representation formalisms which can be used to represent and reason with conceptual knowledge about a domain of interest. The knowledge represented by DLs is mainly static. In many applications, the domain knowledge is dynamic. This observation motivates the research on how to update the knowledge when changes in the application domain take place. This thesis is dedicated to the study of updating knowledge, more precisely, assertional knowledge represented in DLs. We explore whether the updated knowledge can be expressed in several standard DLs and, if so, whether it is computable and what is its size.

@thesis{ Liu-PhD-10,
  address = {Dresden, Germany},
  author = {Hongkai {Liu}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Computing Updates in Description Logics},
  type = {Doctoral Thesis},
  year = {2010},
}

In recent years, the description logic EL has received a significant interest. The description logic EL is a knowledge representation formalism used e.g in natural language processing, configuration of technical systems, databases and biomedical ontologies. Unification is used there as a tool to recognize equivalent concepts. It has been proven that unification in EL is NP-complete. This result was based on a locality property of certain EL unifiers. Here we show that a similar local- ity holds for EL without top (EL-top), but decidability of EL-top unification does not follow immediately from locality as it does in the case of unification in EL. However, by restricting further the locality property, we prove that EL-top unifica- tion is decidable and construct an NExptime decision procedure for the problem. Furthermore, we show that unification in EL-top is PSPACE-hard by reducing the Finite State Automata Intersection problem to EL-top unification problem.

@thesis{ Ngu-Mas-10,
  address = {Dresden, Germany},
  author = {Nguyen Thanh {Binh}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Unification in Description Logic EL without Top Constructor},
  type = {Master's Thesis},
  year = {2010},
}

Automata over infinite trees are used in many areas of theoretical computer science, such as model checking or description logics. This is because deciding the satisfiability of many types of logical formulae can be reduced to checking the emptiness of the tree language defined by such an automaton. Weighted automata can be used to compute quantifiable properties of formulae. The language inclusion problem for certain types of automata over infinite trees is analyzed, as well as a generalization of this problem to weighted automata. Several constructions are presented and compared for different automata models.

@thesis{ Bor-Dip-10,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt}},
  school = {Technische Universit\"{a}t Dresden},
  title = {The Infimum Problem as a Generalization of the Inclusion Problem for Automata},
  type = {Diploma Thesis},
  year = {2010},
}

Fuzzy Description Logics are an extension of Description Logics (DL) which deal with fuzzy and vague concepts. Recently, several algorithms, based on tableau methods, have been developed for reasoning with t-norm fuzzy DLs, in particular the product and Lukasiewicz t-norms. In this work, we analyse these algorithms and show that they are not able to detect unsatisfiability of Knowledge Bases in all cases. We try to solve this problem by presenting several conditions that lead to unsatisfiability, which can be decided directly from the output of the existing fuzzy tableau algorithms.

@thesis{ Far-Mas-10,
  address = {Dresden, Germany},
  author = {M. {Farooque}},
  school = {Technische Universit\"{a}t Dresden},
  title = {A Study on Satisfiability in Fuzzy Description Logics},
  type = {Master's Thesis},
  year = {2010},
}

@thesis{ Kno-Mas-10,
  address = {Dresden, Germany},
  author = {C. {Knobloch}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Beschreibung formaler Sprachen mittels DNA-Rekombination in Ciliaten},
  type = {Master's Thesis},
  year = {2010},
}

In this thesis we investigate the problem of deciding query completeness over partially incomplete databases. Incomplete data is an ubiquitous problem in practical data management. Often however, knowledge about completeness of parts of the data exists. Then, the problem is to decide whether a query answer still is necessarily complete. Previous work on this problem reduced it to a generally undecidable problem. Also it considered only a special case of completeness reasoning in the presence of schema and extensional information. We present a better solution for the problem by reducing it to the problem of query containment. We study the effect of schema and extensional information on completeness reasoning and its complexity. We discuss relevant aspects of a prototypical implementation done in collaboration with the school IT department of the province of South Tyrol.

@thesis{ Raz-Dip-10,
  address = {Dresden, Germany},
  author = {Simon {Razniewski}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Completeness of Queries over Incomplete Databases},
  type = {Diploma Thesis},
  year = {2010},
}

Building and mantaining large-scale ontologies is an error-prone task. It is thus not uncommon to find unwanted or unexpected consequences that follow implicitely from the restrictions in the ontology. To understand and correct these consequences, it is helpful to find the specific portions of the ontology that are responsible for them. Axiom-pinpointing is the task of finding minimal subontologies that entail a given consequence, also called MinAs. In this work we look at the task of computing all the MinAs by means of modified decision procedures. We first show that tableaux- and automata-based decision procedures can be transformed into pinpointing algorithms that output a (compact) representation of the set of all MinAs. We then explore the complexity of the problem.

@thesis{ Pen-PhD-09,
  address = {Dresden, Germany},
  author = {Rafael Pe\~{n}aloza {Nyssen}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Axiom-Pinpointing in Description Logics and Beyond},
  type = {Doctoral Thesis},
  year = {2009},
}

Description Logics (DLs) belong to a successful family of knowledge representation formalisms with two key assets: formally well-defined semantics which allows to represent knowledge in an unambiguous way and automated reasoning which allows to infer implicit knowledge from the one given explicitly. This thesis investigates various reasoning techniques for tractable DLs in the EL family which have been implemented in the CEL system. It suggests that the use of the lightweight DLs, in which reasoning is tractable, is beneficial for ontology design and maintenance both in terms of expressivity and scalability. The claim is supported by a case study on the renown medical ontology SNOMED CT and extensive empirical evaluation on several large-scale biomedical ontologies.

@thesis{ Sun-PhD-09,
  address = {Dresden, Germany},
  author = {Boontawee {Suntisrivaraporn}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Polynomial-Time Reasoning Support for Design and Maintenance of Large-Scale Biomedical Ontologies},
  type = {Doctoral Thesis},
  year = {2009},
}

In many applications of description logics (DLs) it is no longer enough to describe the static aspects of the application domain. In particular, there is a need to formalize the temporal evolution of an application domain. This is the case, for example, if we want to use DLs as conceptual modeling languages for temporal databases. Another example are medical ontologies, where the representation of concepts often requires reference to temporal patterns. However, description logics have been designed and used as a formalism for knowledge representation and reasoning only in static application domains. Therefore, DLs are not able to express temporal aspects of knowledge. The previous observations have resulted in diverse proposals of temporal description logics (TDLs). In particular, one approach is to combine standard description logics, such as ALC and EL, with standard temporal logics, such as LTL, CTL and CTL*.

In this thesis, we follow the mentioned approach. More precisely, we use the description logics ALC and EL in the DL component and the temporal logic computation tree logic (CTL) in the temporal component. These combinations result in two TDLs, namely CTL-ALC from the combination of ALC and CTL, and CTL-EL from the combination of CTL and EL. In CTL-ALC and CTL-EL , we focus on temporal reasoning about concepts, i.e., we apply temporal operators only to concepts. After introducing CTL-ALC and CTL-EL, we determine the computational complexity for reasoning problems in the mentioned logics. More precisely, we show that satisfiability w.r.t. TBoxes with expanding domains in CTL-ALC is EXPTIME-complete. We show also that subsumption w.r.t. TBoxes with expanding domains in CTLEL is intractable, in particular, it is EXPTIME-complete.

@thesis{ Gut-Mas-09,
  address = {Dresden, Germany},
  author = {V\'{i}ctor Didier Guti\'{e}rrez {Basulto}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Branching Temporal Description Logics: Reasoning About CTL-ALC And CTL-EL Concepts},
  type = {Master's Thesis},
  year = {2009},
}

Ontologies play an increasingly important role in areas such as the life and clinical sciences and the Semantic Web. Domain experts, i.e. biologists and clinicians, build and re-use (parts of) ontologies, and make use of reasoners to explicate some of the knowledge captured in an ontology. Understanding this knowledge is a highly complex task for which some tool support has recently become available, yet it has also become clear that more support is needed.

The goal of this work was to investigate whether model exploration, i.e. the interactive generation and presentation of models of an ontology, can be used to help ontology engineers understand the knowledge captured in an ontology. In order to achieve this goal, a Protégé 4 plug-in supporting generation of and interaction with models was implemented. In addition, a pilot study was carried out to evaluate its effectiveness in supporting users in understanding an ontology.

@thesis{ Bau-Mas-09,
  address = {Dresden, Germany},
  author = {Johannes {Bauer}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Model Exploration to Support Understanding of Ontologies},
  type = {Master's Thesis},
  year = {2009},
}

Computergestützte Wissensrepräsentation ist seit der Prägung des Begriffs "Semantic Web" in mehrere W3C-Standards eingeflossen und hat damit den Weg für Ontologien in reale Informationssysteme geebnet. Die Mehrheit dieser Systeme basiert heutzutage auf einer verteilten Architektur, was sich jedoch in der theoretischen Basis der verbreiteten Ontologiesprachen nur unzureichend widerspiegelt.

Die Arbeit gibt einen Überblick über existierende Ansätze, die diese Unzulänglichkeit mittels der Einbettung in einen modularen Kontext zu lösen versuchen. Dabei sind E-Connections hervorzuheben, da sie ein robustes theoretisches Fundament besitzen, welches die Verknüpfung vieler modaler und beschreibender Logiken ermöglicht. Den betrachteten Formalismen fehlt es jedoch oft an einer gründlichen Analyse der Extraktion von Wissen mittels konjunktiver Abfragen, was zu deren mangelnder Eignung für einen praktischen Einsatz beiträgt.

Für allgemeine E-Connections wird die Frage nach der Berechenbarkeit solcher Abfragen mittels der Vorstellung eines korrekten und vollständigen Verfahrens und zweier daran geknüpfter Bedingungen ausführlich beantwortet. Dieses reduziert in mehreren Schritten die Beantwortung einer Abfrage auf eine Menge von Erfüllbarkeits-Prüfungen von E-Connection-Wissensbasen. Es wird erörtert, unter welchen Bedingungen die Beantwortung zudem verteilt erfolgen kann, und ein allgemeines Implementierungskonzept vorgestellt.

@thesis{ Eic-Dip-09,
  address = {Dresden, Germany},
  author = {J\"{o}rg {Eichhorn}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Untersuchung von konjunktiven Abfragen \"{u}ber verteilte Ontologien mit dem Fokus auf E-Connections},
  type = {Diploma Thesis},
  year = {2009},
}

Gene Assembly ist ein biologischer Prozess in Ciliaten, der aus den Operationen, loop, hairpin, und doubleloop besteht. Für Gene Assembly existieren zwei Modellrichtungen, deren Unterschied in der Anzahl an den Gene Assembly Operationen beteiligten Molekülen begründet ist. Das so genannte intermolekulare Gene Assembly Modell erlaubt, dass Operationen zwischen mehr als einem Molekül stattfinden können. Der zweite Modellansatz wird als intramolekulares Gene Assembly Modell bezeichnet. Dessen Operationen agieren auf verschiedenen Teilen desselben Moleküls. Neben dem ursprünglichen intramolekularen Gene Assembly Modell, welches heute als universelles Modell bezeichnet wird, entwickelten sich zwei weitere Modelle. Ein elementares Modell und ein so genanntes einfaches Modell. Beide beruhen auf einer Restriktion der Gene Assembly Operationen zu vereinfachten Operationen. Die teils geringen Abweichungen zwischen den drei intramolekularen Modellen haben starke Auswirkungen auf den Charakter der Modelle. Es wird ein Vergleich der drei Modelle hinsichtlich ausgewählter Eigenschaften vorgenommen. Für das einfache Modell wird für die vereinfachte doubleloop Operation (sd) eine Charakterisierung sd-sortierbarer Genmuster aufgestellt.

@thesis{ Hau-Dip-09,
  address = {Dresden, Germany},
  author = {Rainer {Hausdorf}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Intramolekulares Gene Assembly},
  type = {Diploma Thesis},
  year = {2009},
}

Daily life depends on complex hardware and software systems and the question whether a system satisfies its specification becomes more and more crucial. One way to verify such systems is runtime verification. This technique has been considered for specifications given in terms of a formula of some propositional temporal logic. For reasoning in the context of ontology-based applications, this approach was extended to the temporal description logic ALC-LTL where both rigid and flexible concept and role names are available. This talk presents some of the results of the underlying work, which also deals with reasoning with respect to incomplete knowledge, where the past behaviour of the system is not completely known.

@thesis{ Lip-Dip-09,
  address = {Dresden, Germany},
  author = {Marcel {Lippmann}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Runtime Verification Using Temporal Description Logics},
  type = {Diploma Thesis},
  year = {2009},
}

Description logics (DLs) provide expressiveness much beyond the expressiveness of propositional logic while still maintaining decidability of reasoning. This makes DLs a natural choice for formalizing actions. Besides DLs are also used in several application domains. However representing dynamic aspects of such application domains is not out of question. As a result, temporal extensions of DLs have been investigated in literature. In formalizing actions, sometimes we come across a situation, where we want to be sure of a property to hold at a certain time. Thus a suitable approach is of using temporalized DLs in describing such properties meanwhile formalizing actions in DLs. In this thesis, we present the integration of action formalisms in a temporalized DL.

We consider the "satisfiability problem" of an ALCO-LTL formula with respect to an acyclic TBox, an ABox and actions i.e., we check if there is a sequence of world states (interpretations) such that the formula is satisfied in this sequence whereas the semantics of the actions is also respected. We consider two different cases; a simple case in which we consider "unconditional actions" where all the changes imposed by an action hold trivially after the application of the action and a general case in which we consider "conditional actions". A conditional action requires certain conditions to hold in order to impose such changes. In the former case, we reduce the problem to the ABox consistency problem, whereas in the later case, we reduced it to the emptiness problem of a Büchi automaton and the ABox consistency problem.

@thesis{ Meh-Mas-09,
  address = {Dresden, Germany},
  author = {Anees ul {Mehdi}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Integrate Action Formalisms into Linear Temporal Description Logics},
  type = {Master's Thesis},
  year = {2009},
}

Description Logics (DLs) are a family of logic-based knowledge representation (KR) formalisms designed to represent and reason about static conceptual knowledge in a semantically well-understood way. On the other hand, standard action formalisms are KR formalisms based on classical logic designed to model and reason about dynamic systems. The largest part of the present work is dedicated to integrating DLs with action formalisms, with the main goal of obtaining decidable action formalisms with an expressiveness significantly beyond propositional. To this end, we offer DL-tailored solutions to the frame and ramification problem. The main technical result is that standard reasoning problems about actions (executability and projection), as well as the plan existence problem are decidable if one restricts the logic for describing action pre- and post-conditions and the state of the world to decidable Description Logics. Moreover, reasoning about DL actions is reducible to standard DL reasoning problems, with the nice consequence that already available DL reasoners can be employed to provide automated support for reasoning about a dynamically changing world. A smaller part of the work is related to the design of a tableau algorithm for decidable extensions of Description Logics with concrete datatypes, most importantly with those allowing to refer to the notions of space and time, and with powerful domain constraints (general concept inclusions).

@thesis{ MajaMilicicDiss,
  address = {Dresden, Germany},
  author = {Maja {Mili\v{c}i\'{c}}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Action, Time and Space in Description Logics},
  type = {Doctoral Thesis},
  year = {2008},
}

ABoxes in Description Logics are used to represent factual knowledge of the world. In many situations an ABox is not enough to represent the knowledge of the world under consideration, as there is just an implicit boolean AND operator between each ABox assertion in the ABox. A Boolean ABox allows us to state Boolean combination of ABox assertions. The present work deals with the consistency problem of Boolean ABoxes in Description Logics (DLs).

Five years ago, a reduction algorithm to check consistency of ALC Boolean ABoxes has been introduced, in which an ALC Boolean ABox is reduced to a satisfiability preserving knowledge base, possibly in a more expressive description logic. We also argue that the reduction algorithm can be extended to check consistency of ALCO Boolean ABoxes. Motivated by ongoing research in Satisfiability Modulo Theory (SMT), we applied the DPLL(T) approach of SMT to check consistency of Boolean ABoxes. We have implemented a SAT solver based on DPLL procedure with state-of-the-art performance enhancing techniques like backjumping and conflict-driven-lemma- learning. By interconnecting the SAT solver with a DL reasoner using a special communication strategy, we developed a DPLL(T) solver to check consistency of ALCO Boolean ABoxes.

We have also implemented a reasoner to check consistency of ALCO Boolean ABoxes based on the reduction algorithm on top of an existing DL reasoner having a reasoning service to check consistency of ALCO ABoxes. In both of the implementations for checking consistency of Boolean ABoxes, Java is used as the programming language. Both of the implementations are tested, compared, and analyzed on the input stemming from the ABox update problem.

@thesis{ Vir-Mas-08,
  address = {Dresden, Germany},
  author = {Jigneshkumar Ramjibhai {Viradia}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Reasoning with Boolean ABoxes},
  type = {Master's Thesis},
  year = {2008},
}

Die Erforschung der komplexen Organisationsprinzipien biologischer Zellen steht im Interesse des noch jungen Forschungsgebietes der Systembiologie. Die strukturierte Repräsentation vorhandenen Wissens und die Unterstützung des Erkenntnisgewinns durch Simulationen erfordert die Entwicklung formaler Modellierungssprachen und liefert insbesondere für die Theoretische Informatik eine neue Herausforderung. Ein vielversprechender Ansatz für diese Zielstellung sind die auf autonomen, kommunizierenden Agenten basierenden Prozesskalküle. Ausgehend vom π-Kalkül, deren bekanntestem Vertreter, wurden Adaptionen entwickelt, die durch die Spezialisierung auf einzelne Komponenten biologischer Zellen besonders direkte Modellierungen von Teilfunktionalitäten ermöglichen. Zwei solche Ansätze sind der auf die Modellierung von Membraninteraktionen spezialisierte Brane-Kalkül und der κ-Kalkül, der sich auf Proteininteraktionen konzentriert. Die beiden Prozesskalküle werden anhand eines Beispiels aus der Biologie vorgestellt und bezüglich ihrer Eignung für Modellierungen der Systembiologie diskutiert. Ausgehend vom Brane-Kalkül wird schließlich ein Ansatz entwickelt, der durch die Vereinigung der Vorteile beider Prozesskalküle einer breiteren Anwendung zur Verfügung steht.

@thesis{ Voi-Dip-08,
  address = {Dresden, Germany},
  author = {Sebastian {Voigt}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Modellierung zellbiologischer Prozesse mittels Brane- und $\kappa$-Kalk\"{u}l},
  type = {Diploma Thesis},
  year = {2008},
}

Description Logics are a family of knowledge representation formalisms for representing and reasoning about conceptual knowledge. Every DL system has reasoning services as an important component that infer implicit knowledge from the one explicitly given. Standard reasoning problems include concept satisability, concept subsumption, ABox consistency and the instance checking problem. This work considers the concept subsumption service, which is considered to be the most traditional service. Four years ago, a polynomial time algorithm for subsumption problem in the Description Logic EL was developed. After that, algorithms for dierent problems in tractable extensions of EL have been developing. These Description Logics are sucient to represent many knowledge bases; however, there are ontologies requiring more expressive extensions of EL. Specifically, GALEN, an important medical ontology, requires ELHIfR+, an intractable extension of EL that includes role hierarchies, inverse, functional and transitive roles. This motivates the extension of the polynomial time algorithm to ELHIfR+. This thesis proposes two solutions for the subsumption problem in ELHIfR+. The first solution is to reduce ELHIfR+ to the less expressive DL ELI, for which an algorithm is readily available. The second solution is to create an algorithm for the concept subsumption problem in ELHIfR+. This algorithm still runs in polynomial time in the simple case of ELHIfR+ that does not include inverse and functional roles.

@thesis{ Vu-Mas-08,
  address = {Dresden, Germany},
  author = {Quoc Huy {Vu}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Subsumption in the Description Logic in ELHIfR+ w.r.t. General TBoxes},
  type = {Master's Thesis},
  year = {2008},
}

Description Logics (DLs) are a family of knowledge representation languages with well-defined logic-based semantics and decidable inference problems, e.g. satisfiability. Two of the most widely used decision procedures for the satisfiability problem are tableau- and automata-based algorithms. Due to their different operation, these two classes have complementary properties: tableau algorithms are well-suited for implementation and for showing PSPACE and NEXPTIME complexity results, whereas automata algorithms are particularly useful for showing EXPTIME results. Additionally, they allow for an elegant handling of infinite structures, but they are not suited for implementation. The aim of this thesis is to analyse the reasons for these differences and to find ways of transferring properties between the two approaches in order to reconcile the positive properties of both.

In a first approach, we describe a method to translate automata into DL knowledge bases, which allows us to use tableau reasoners to decide the automata emptiness problem. Since empirical results show that this does not lead to acceptable performance in practice, we develop a way for transferring PSPACE complexity results from tableaus to automata by modifying the automata emptiness test with optimisation techniques known from tableaus, in particular by using a blocking condition. Finally, in order to transfer EXPTIME complexity results from the automata to the tableau paradigm, we develop Tableau Systems, a framework for tableau algorithms. From an algorithm formalised within this framework, it is possible to derive both an EXPTIME automata algorithm and a tableau algorithm that is useable in practice.

@thesis{ Hladik-Diss-2007,
  address = {Dresden, Germany},
  author = {Jan {Hladik}},
  school = {Technische Universit\"{a}t Dresden},
  title = {To and Fro Between Tableaus and Automata for Description Logics},
  type = {Doctoral Thesis},
  year = {2007},
}

Description Logics (DLs) are a class of logic based knowledge representation formalisms that are used to represent terminological knowledge of an application domain in a structured way. Formal Concept Analysis (FCA), on the other hand, is a field of applied mathematics that aims to formalize the notions of a concept and a conceptual hierarchy by means of mathematical tools. Although the notion of a concept as a collection of objects sharing certain properties, and the notion of a conceptual hierarchy are fundamental to both DLs and FCA, the ways concepts are described and obtained differ significantly between these two research areas.

In the present work we show that, despite these differences, DL research can benefit from FCA research for solving problems encountered in knowledge representation by employing FCA methods. Our contributions in this direction fall mainly under two topics: 1) supporting bottom-up construction of DL knowledge bases, 2) completing DL knowledge bases. In the first one we show how the attribute exploration method can be used for computing least common subsumers w.r.t. a background knowledge base. In the second one, we develop an extension of FCA for open-world semantics of DL knowledge bases, and show how the extended attribute exploration method can be used to detect missing axioms and individuals in a DL knowledge base. Moreover we also contribute to FCA research by investigating the computational complexity of several decision and counting problems related to minimal generators of closed sets.

@thesis{ Sertkaya-Diss-2007,
  address = {Dresden, Germany},
  author = {Bar\i{}\c{s} {Sertkaya}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Formal Concept Analysis Methods for Description Logics},
  type = {Doctoral Thesis},
  year = {2007},
}

Description logics (DL) knowledge bases are often build by users with expertise in the application domain, but little expertise in logic. To support this kind of users when building their knowledge bases a number of extension methods have been proposed to provide the user with concept descriptions as a starting point for new concept definitions. The inference service central to several of these approaches is the computation of (least) common subsumers of concept descriptions.

In case disjunction of concepts can be expressed in the DL under consideration, the least common subsumer (lcs) is just the disjunction of the input concepts. Such a trivial lcs is of little use as a starting point for a new concept definition to be edited by the user. To address this problem we propose two approaches to obtain "meaningful" common subsumers in the presence of disjunction tailored to two different methods to extend DL knowledge bases. More precisely, we devise computation methods for the approximation-based approach and the customization of DL knowledge bases, extend these methods to DLs with number restrictions and discuss their efficient implementation.

@thesis{ Turhan-PhD,
  address = {Dresden, Germany},
  author = {Anni-Yasmin {Turhan}},
  school = {Technische Universit\"{a}t Dresden},
  title = {On the Computation of Common Subsumers in Description Logics},
  type = {Doctoral Thesis},
  year = {2007},
}

A description logic ABox is a tool to represent a snapshot of the world. Since the world is dynamic, we need a mechanism to update Aboxes. In general, updates can be any kind of information about a change of the world. Here, we consider only basic updates, i.e., updates that are described using only simple ABoxes. There are several known results concerning this kind of update. One of the results is that the existence of nominals and @-constructor is needed to express the updated ABox. More precisely, the simplest DL that is propositionally closed that is able to express the updated ABox is ALCO@. We try to recover the existence of ABox updates in fragments of ALCO@ that are still propositionally closed, by weakening the definition of ABox updates from semantic updates to syntactic updates. It turns out that this weakening is not enough to recover the existence of ABox updates in these DLs. We then try again to further weaken the definition of ABox updates from syntactic updates to extended syntactic updates. With this additional weakening, we recover the existence of ABox updates in ALCO. Unfortunately, this is not the case for ALC. If we only allow ALC ABoxes as the result of updates, then, also this second weakening is still not enough to recover ABox updates in ALC. Then, we recover the existence of extended syntactic ABox updates in ALC by allowing a KB, i.e., a pair of a TBox and an ABox, as the result of the update.

@thesis{ Bon-Mas-07,
  address = {Dresden, Germany},
  author = {Yusri {Bong}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Description Logic ABox updates revisited},
  type = {Master's Thesis},
  year = {2007},
}

Ontologies are now ubiquitous and many of them are currently being ported into logical formalisms, most notably description logic (DL). It is inevitable that such migration might introduces inconsistencies—both in terms of logical and that of ontological—which could be far from obvious. This motivates the recent research topic of explanation of DL-based ontologies. Explanation comes in two flavors: pinpointing which addresses the source of inconsistencies found in the ontology and debugging which recovers the ontology into a consistent state. Since the latter often requires information from the former, we consider axiom pinpointing as essential for both flavors of the explanation problem. Much of the research in this area is focusing on expressive DLs, in which standard reasoning alone is already highly intractable. In this paper, we investigate this problem in a tractable extension of EL which is useful in life science applications. We have discovered that pinpointing is inherently intractable—despite the tractable logic considered—if all information is required. This is due to the combinatorial blow-up of possible sets of axioms. We develop a labelled algorithm for axiom pinpointing based on the EL subsumption algorithm and the known labelling technique used in tableau algorithm. For implementation purposes, we restrict this algorithm to computation of only partial information, for which polynomial-time algorithm can be obtained. We have experimented this approach on Galen and found that even partial information can already help ease the way an ontology is being debugged.

@thesis{ Hua-Mas-07,
  address = {Dresden, Germany},
  author = {Huang {Changsheng}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Non-standard inference for explaining subsumption in the description logic EL with general concept inclusions and complex role inclusions},
  type = {Master's Thesis},
  year = {2007},
}

During the last years, it has been shown that the description logic EL is well-suited for tractable reasoning. In particular, reasoning is even tractable w.r.t. general concept inclusion axioms, and various extensions of EL and their effects on the complexity of subsumption w.r.t. general concept inclusion axioms have been studied. In this thesis, we sharpen the border between tractability and intractability of subsumption in extensions of EL w.r.t. cyclic TBoxes. We provide two new extensions for which subsumption can be computed in polynomial time w.r.t. cyclic TBoxes. The first extends EL by role con- and disjunction in disjunctive normal form, primitive negation and p-admissible concrete domains, and the second by role con- and disjunction in disjunctive normal form and at-least restrictions. Moreover, we show that a combination of the two extensions leads to intractability of subsumption w.r.t. cyclic TBoxes, as well as EL extended by negation, disjunction, transitive closure over role names, functionality and concrete domains with abstract feature chains. This justifies the fact that—except for inverse roles which remain an open problem—both extensions are maximal in the sense that they cannot be further extended without losing tractability of subsumption w.r.t. cyclic TBoxes.

@thesis{ Haa-Mas-07,
  address = {Dresden, Germany},
  author = {Christoph {Haase}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Complexity of Subsumption in Extensions of EL},
  type = {Master's Thesis},
  year = {2007},
}

Instance checking is the basic problem of querying a description logic knowledge base comprising a TBox and an ABox. Most existing complexity results for instance checking concern combined complexity, which is measured in the size of the whole input consisting of a TBox, an ABox, a query concept and an individual name. However, in many applications, the size of the ABox is much larger than the size of the other parts of the input. Hence, it is more realistic to analyze data complexit, which is measured only in the size of the ABox. This thesis maps out the data complexity of instance checking in the EL family of DLs, a for which the tractability boundary of subsumption has been previously clarified. We identify members of the EL family for which data complexity is coNP-hard (and thus intractable) and members of the EL family for which data complexity is tractable. As an interesting note, these results show that the tractability boundary regarding combined complexity does not coincide with that of data complexity.

@thesis{ Kri-Mas-07,
  address = {Dresden, Germany},
  author = {Adila Alfa {Krisnadhi}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Data Complexity of Instance Checking in the EL Family of Description Logics},
  type = {Master's Thesis},
  year = {2007},
}

@thesis{ Lau-Mas-07,
  address = {Dresden, Germany},
  author = {T. {Lau}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Molekulares Self-Assembly},
  type = {Master's Thesis},
  year = {2007},
}

Description Logics (DLs) are logic-based formalisms for representing knowledge that provide a trade-off in expressivity and reasoning within a formalism. On one side of the spectrum, there is a light-weight description logic EL with top symbol, conjunction and existential restriction, whose expressivity, though very limited, is sufficient to describe some of the widely used ontologies of today. It has been shown that the subsumption problem in EL has polynomial complexity for terminologies with cyclic definitions w.r.t. greatest fixpoint, least fixpoint, and descriptive semantics, and for the general terminologies interpreted by de- scriptive semantics. Recently, the same was shown in these cases by devising sound and complete proof systems for these semantics.

Hybrid EL TBoxes have been proposed in order to combine the generality of cyclic definitions and general concept inclusions with certain desirable non- standard inference services. These terminologies combine two of the semantics, descriptive and greatest fixpoint semantics. A polynomial subsumption algo- rithm for theories with hybrid EL TBoxes and corresponding semantics was recently proposed.

Motivated by previous results, this thesis looks at the problem of subsumption w.r.t. hybrid EL TBoxes from a proof-theoretic point of view. A rule system is devised, and we show that polynomial proof search in the calculus yields a polynomial decision procedure for the subsumption problem in EL w.r.t. hybrid TBoxes.

In addition, we consider the problem of existence of least common subsumers of two EL concepts w.r.t. hybrid TBoxes. We give a positive answer to the existence problem by providing an algorithm for computing such concepts and showing its correctness in a proof-theoretic manner.

@thesis{ Nov-Mas-07,
  address = {Dresden, Germany},
  author = {Novak {Novakovi\'{c}}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Proof-theoretic Approach to Deciding Subsumption and Computing Least Common Subsumer in EL w.r.t. Hybrid TBoxes},
  type = {Master's Thesis},
  year = {2007},
}

In dem noch jungen Forschungsgebiet der Systembiologie werden lebende Zellen als komplexe Systeme mit einer Vielzahl autonomer, kommunizierender Komponenten aufgefasst. Die Verschiedenartigkeit dieser Komponenten, deren wichtigste Vertreter Gene, Proteine und Membranen sind, stellt besondere Anforderungen an geeignete Ansätze zur formalen Modellierung ihrer Interaktionen. Insbesondere Konzepte aus der theoretischen Informatik zur Beschreibung und Analyse komplexer Systeme können zur Realisierung dieser Zielstellung einen wesentlichen Beitrag leisten. Die Diplomarbeit untersucht Ansütze auf Prozesskalkül-Basis, die sich als vielversprechende Modellierungssprachen für biologische Prozesse erwiesen haben. Ausgehend vom -Kalkül, dem bekanntesten Vertreter dieser Gruppe, werden zwei Erweiterungen diskutiert, die sinnvolle Anpassungen an die Thematik der Zellbiologie darstellen. Die resultierenden Kalküle werden anhand von Beispielmodellierungen demonstriert und bezüglich biologisch relevanter Kriterien sowohl untereinander als auch mit anderen Ansätzen auf Prozesskalkül-Basis verglichen.

@thesis{ Ste-Dip-07,
  address = {Dresden, Germany},
  author = {Florian {Stenger}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Adaptionen von Prozesskalk\"{u}len f\"{u}r eine Anwendung in der Systembiologie},
  type = {Diploma Thesis},
  year = {2007},
}

Most commonly used Description Logic reasoning systems provide only limited support for debugging logically inconsistent knowledge bases. Attempts have been made to come up with algorithms that solve the debugging problem by suggesting possible resolutions. These algorithms use the method of pinpointing of the axioms in the knowledge bases that are the possible source of inconsistency. In this thesis, we analyze two of such pinpointing algorithms devised for the Description Logic ALC. These algorithms are extensions of the standard tableau-based reasoning algorithms for the consistency of the knowledge bases represented in ALC. These pinpointing algorithms calculate maximal satisfiable subsets of the original knowledge base by pinpointing minimal sets of the problematic axioms. We have shown in the thesis that although these algorithms appear to be working quite differently from each other but a close analysis reveals that they use the same idea of axiom pinpointing and execute it in a similar fashion. Both contain similar rules to expand the knowledge and the rule applications have similar results in both of the algorithms. But the two algorithms keep the information about the axioms, that generate a particular knowledge portion, in different ways.

@thesis{ Tay-Mas-07,
  address = {Dresden, Germany},
  author = {Muhammad {Tayyab}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Analysis of Pinpointing Algorithms for the Description Logic ALC},
  type = {Master's Thesis},
  year = {2007},
}

@thesis{ Tho-Mas-07,
  address = {Dresden, Germany},
  author = {J. {Thomas}},
  school = {Technische Universit\"{a}t Dresden},
  title = {\"{A}quivalenz von in-vivo- und in-vitro-Modellen im Natural-Computing},
  type = {Master's Thesis},
  year = {2007},
}

@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},
}

The present work deals with Description Logics (DLs), a class of knowledge representation formalisms used to represent and reason about classes of individuals and relations between such classes in a formally well-defined way. We provide novel results in three main directions. (1) Tractable reasoning revisited: in the 1990s, DL research has largely answered the question for practically relevant yet tractable DL formalisms in the negative. Due to novel application domains, especially the Life Sciences, and a surprising tractability result by Baader, we have re-visited this question, this time looking in a new direction: general terminologies (TBoxes) and extensions thereof defined over the DL EL and extensions thereof. As main positive result, we devise EL++(D)-CBoxes as a tractable DL formalism with optimal expressivity in the sense that every additional standard DL constructor, every extension of the TBox formalism, or every more powerful concrete domain, makes reasoning intractable. (2) Non-standard inferences for knowledge maintenance: non-standard inferences, such as matching, can support domain experts in maintaining DL knowledge bases in a structured and well-defined way. In order to extend their availability and promote their use, the present work extends the state of the art of non-standard inferences both w.r.t. theory and implementation. Our main results are implementations and performance evaluations of known matching algorithms for the DLs ALE and ALN, optimal non-deterministic polynomial time algorithms for matching under acyclic side conditions in ALN and sublanguages, and optimal algorithms for matching w.r.t. cyclic (and hybrid) EL-TBoxes. (3) Non-standard inferences over general concept inclusion (GCI) axioms: the utility of GCIs in modern DL knowledge bases and the relevance of non-standard inferences to knowledge maintenance naturally motivate the question for tractable DL formalism in which both can be provided. As main result, we propose hybrid EL-TBoxes as a solution to this hitherto open question.

@thesis{ Brandt-PhD-2006,
  address = {Dresden, Germany},
  author = {Sebastian-Philipp {Brandt}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Standard and Non-standard Reasoning in Description Logics},
  type = {Doctoral Thesis},
  year = {2006},
}

Description Logics (DLs) are a family of logic-based knowledge representation formalisms for representing and reasoning about conceptual knowledge. To represent and reason about concrete qualities of real-world entities such as size, duration, or amounts, DLs are equipped with concrete domains. Interestingly, DLs and DLs with concrete domains are useful in many applications, such as modelling database schemas and the semantic web. Recently, it has been suggested that the expressive power of DLs with concrete domains can be further extended by adding database-like key constraints. In database schemas, key constraints can be a source of additional inconsistencies, which DLs used in reasoning about database schemas should be able to capture. Up to now, two different types of key constraints, namely uniqueness constraints and funtional dependencies, have been considered in the context of DLs with concrete domains. Surprisingly, to the best of our knowledge the two types of key constraints have not been investigated in one single logic despite the fact that in some applications, both of them are needed. In this paper, we consider the first description logic with concrete domains, uniqueness constraints, and functional dependencies. It it obtained by extending the description logic ALC(D) (the basic propositional closed description logic ALC equipped with a concrete domain D) with key boxes consisting of key constraints. More precisely, we analyze the impact of the presence of both types of key constraints on decidability and complexity of reasoning. Following from previous results, uniqueness constraints and functional dependencies bring undecidability in the general case and in order to preserve decidability we need to consider a slightly restricted form of key constraints. In the restricted form, we are able to show that reasoning w.r.t. both types of key constraints is not harder than reasoning w.r.t. each of them individually. Furthermore, several extensions with acyclic TBoxes, general TBoxes, and inverse roles are also discussed.

@thesis{ Din-Mas-06,
  address = {Dresden, Germany},
  author = {D\~{u}ng {Dinh-Khac}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Two Types of Key Constraints in Description Logics with Concrete Domains},
  type = {Master's Thesis},
  year = {2006},
}

@thesis{ Hin-Dip-06,
  address = {Dresden, Germany},
  author = {Matthias {Hintzmann}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Verifikation von DNA-basierten Programmen},
  type = {Diploma Thesis},
  year = {2006},
}

Description Logics, these days, are becoming more and more of a standard use for the applications that are being developed in the field of Knowledge Representation and Reasoning, be it a medical terminology or a web ontology. There are also state-of-the-art reasoners like Racer, FaCT++ and Pellet etc. that are being developed based on a variety of algorithms from Description Logics. Here we discuss some expressive Description Logics, Knowledge Bases that are built based upon these logics, reasoners that can classify these knowledge bases, and finally the logical constructs that make the knowledge bases hard for the reasoners to classify them.

We basically try to investgate, using an empirical approach, the influence of the various parameters that are used for building knowledge bases. In other words, we shall try to find out which logical operators make a knowledge base hard, when one wants to reason them with the existing reasoners like Racer. For this, we first develop a random TBox generator that can generate TBoxes, based on the input parameters given by the user. The objective of this TBox generator is to generate random TBoxes that are very much similar to the real-world TBoxes, like Galen and Telecom Italia, in terms of characteristics and the classification time.

Once we figure out the basic parameteric set of input values, for this random TBox generator, which can generate a random TBox that resembles the real-world TBox, we then modify these basic parameteric set of input values to generate different random TBoxes. We shall then use each of these random TBoxes as inputs to Racer and try to find out the influence of those parameteric values on the TBoxes, for the reasoner to classify them.

@thesis{ Mud-Mas-06,
  address = {Dresden, Germany},
  author = {R. {Mudunuri}},
  school = {Technische Universit\"{a}t Dresden},
  title = {What Makes a Description Logic Knowledge Base Hard? A First Empirical Approach},
  type = {Master's Thesis},
  year = {2006},
}

Automata theory has proven to be a useful tool for solving decision problems, for example, the satisfiability problem in some logics. This approach consists basically in reducing the desired problem to the emptiness problem of automata. Unfortunately, this reduction leads in some cases to suboptimal methods. When this happens, it is usually possible to find properties in the specific automata that allow the emptiness test to be solved in an optimized manner. This path has been followed many times, but always done solely for the specific automata at the time. In this work general conditions are given, under which the emptiness test can be solved using only logarithmic space on the number of states. These conditions are later applied to prove that ALC-satisfiability with respect to empty and acyclic TBoxes is in PSpace.

@thesis{ Pen-Mas-06,
  address = {Dresden, Germany},
  author = {Rafael {Pe\~{n}aloza}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Optimization of emptiness test of B\"{u}chi automata on infinite trees},
  type = {Master's Thesis},
  year = {2006},
}

Motivated by a chemical process engineering application, we introduce a new concept constructor, namely the n-ary variant of the existential restriction, into the Description Logic (DL) EL. We refer to the resulting logic as EL(n) and to its fragment that matches the needs of the real world application as restricted EL(n). Although the new constructor can be expressed in the DL ALCQ, its translation is exponential and introduces many expensive constructors, thus making the translation-based approach impractical. In the present work, we design direct algorithms for deciding the main inference problem, namely subsumption, in restricted EL(n). We show that reasoning in restricted EL(n) is polynomial when we allow for acyclic TBoxes. Additionally, we examine the complexity of reasoning in (unrestricted) EL(n) with general TBoxes. In particular, we show that subsumption in EL(n) with GCIs is ExpTime-complete. In order to test the practical efficiency of our approach, we implement the polynomial algorithm for restricted EL(n) with acyclic TBoxes in a system called Eln. Comparison between Eln and the state-of-the-art DL reasoner RACER demonstrate a considerable advantage of the direct algorithm over the translation-based approach.

@thesis{ Kar-Mas-05,
  address = {Dresden, Germany},
  author = {Eldar {Karabaev}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Reasoning in the Description Logic EL extended with an n-ary existential quantifier},
  type = {Master's Thesis},
  year = {2005},
}

Matching of concepts against patterns is a so-called non-standard inference problem in Description Logics. For the small description language EL, matching problems without terminological cycles have been investigated. In the present thesis we introduce EL-matching problems allowing terminological cycles. Among the three different semantics defined by Nebel for the interpretation of cyclic TBoxes we will argue that gfp-semantics is the appropriate one to define matching problems. Based on deciding subsumption and computing the least common subsumers, a matching algorithm is provided whose soundness and completeness is shown. Moreover, the matching algorithm is implemented and tested in the programming language LISP.

@thesis{ Liu-Mas-05,
  address = {Dresden, Germany},
  author = {Hongkai {Liu}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Matching in Description Logics with Existential Restrictions and Terminological Cycles},
  type = {Master's Thesis},
  year = {2005},
}

Für die Beschreibungslogik EL ist gezeigt worden, dass das Subsumtionsproblem für zyklische TBoxen in polynomieller Laufzeit entscheidbar ist, sowohl mit gfp-Semantik, als auch mit deskriptiver Semantik. Auch das 'kleinste gemeinsame Oberkonzept' (lcs) von zwei Konzepten aus einer zyklischen EL-TBbox existiert immer und kann in polynomieller Zeit berechnet werden, wenn man die gfp-Semantik zugrunde legt. Ebenso wurde auch für generelle EL-TBoxen mit GCIs bezüglich deskriptiver Semantik ein polynomieller Subsumtionsalgorithmus angegeben. Da es beim Vorkommen von GCIs nicht sinnvoll ist, TBoxen mit gfp-Semantik zu interpretieren, andererseits nur die gfp-Semantik für zyklische EL-TBoxen die wünschenswerte Eigenschaft garantiert, dass das lcs immer existiert und in polynomieller Zeit berechnet werden kann, wurde eine eine neue Art von TBoxen konzipiert, in der sowohl zyklische Definitionen vorkommen, die mit gfp-Semantik interpretiert werden, als auch GCIs, die mit deskriptiver Semantik interpretiert werden. Wir zeigen, dass das Subsumtionsproblem für diese hybriden EL-TBoxen in polynomieller Zeit auf das Subsumtionsproblem für zyklische TBoxen mit gfp-Semantik reduziert werden kann und geben ein Verfahren dafür an. Außerdem wird eine prototypische Implementierung in LISP vorgestellt, die auf bestehenden Implementierungen für das Subsumtionsproblem von generellen TBoxen und zyklischen EL-TBoxen mit gfp-Semantik aufbaut.

@thesis{ Mod-Dip-05,
  address = {Dresden, Germany},
  author = {J\"{o}rg {Model}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Subsumtion in EL bez\"{u}glich hybrider TBoxen},
  type = {Diploma Thesis},
  year = {2005},
}

The subsumption problem in the description logic (DL) EL has been shown to be polynomial regardless of whether cyclic or acyclic TBoxes are used. Recently, it was shown that the problem remains tractable even when admitting general concept inclusion (GCI) axioms. Motivated by its nice complexity and sufficient expressiveness for some applications, we propose three decision procedures for computing subsumption in the DL EL whose run-time is bounded by a low-degree polynomial. The three decision procedures are for three terminological settings in EL: TBoxes with greatest fixpoint semantics (ELgfp), TBoxes with descriptive semantics (ELdes), and terminologies with GCIs (ELgci). For subsumption wrt TBoxes, i.e. ELgfp and ELdes, we use a characterization through simulations on so-called EL-description graphs—the syntactically normalized representation of EL-TBoxes. With an efficient algorithm for computing simulations on graphs, we show that ELgfp-subsumption can be decided in time cubic in the size of the input TBox. We decide ELdes-subsumption by reducing the simulation problem on graphs to the satisfiability problem of Horn formulae. Then, we apply a linear-time Horn-SAT algorithm to our Horn formulae. This approach yields a quartic-time decision procedure for ELdes-subsumption. Concerning terminologies with GCIs, we employ a different normalization and characterize subsumption through so-called implication sets. We show that ELgci-subsumption can be decided in time cubic in the size of the input terminology, by translating the implication sets into a Horn formula and exploiting the linear-time Horn-SAT algorithm similarly to ELdes. Besides, we implement these decision procedures in the Common LISP language and evaluate their efficiency using the Gene Ontology as a benchmark. The implementation can be used as terminological reasoners that classify ontologies represented in EL-TBoxes.

@thesis{ Sun-Mas-05,
  address = {Dresden, Germany},
  author = {Boontawee {Suntisrivaraporn}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Optimization and Implementation of Subsumption Algorithms for the Description Logic EL with cyclic TBoxes and General Concept Inclusion Axioms},
  type = {Master's Thesis},
  year = {2005},
}

Description Logics (DLs) are a family of logic-based knowledge representation formalisms designed to represent and reason about conceptual knowledge. Due to a nice compromise between expressivity and the complexity of reasoning, DLs have found applications in many areas such as, e.g., modelling database schemas and the semantic web. However, description logics represent knowledge in an abstract way and lack the power to describe more concrete (quantitative) qualities like size, duration, or amounts. The standard solution is to equip DLs with concrete domains, e.g., natural numbers with predicates =, <, + or strings with a string concatenation predicate. Moreover, recently it has been suggested that the expressive power of DLs with concrete domains can be further enhanced by providing them with database-like key constraints. Key constraints can be a source of additional inconsistencies in database schemas, and DLs applied in reasoning about database schemas are thus wanted to be able to capture such constraints. Up to now, only the integration of uniqueness key constraints into DLs with concrete domains has been investigated. In this thesis, we continue this investigation by considering another type of keys, called functional dependencies. Functional dependencies allow us to state that a property is uniquely determined by a set of properties, such as: ``all books with the same ISBN number have the same title''. We will focus on ALC (the basic propositionally closed DL) and ALC(D) (ALC equipped with an arbitrary concrete domain D). We show that functional dependencies, just like uniqueness constraints, dramatically increase the complexity of reasoning in the PSpace-complete ALC(D): reasoning in ALC(D)^FD (ALC(D) extended with functional dependencies) is undecidable in the general case, while NExpTime-complete in a slightly restricted version.

@thesis{ Mil-Mas-04,
  address = {Dresden, Germany},
  author = {Maja {Mili\v{c}i\'{c}}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Description Logics with Concrete Domains and Functional Dependencies},
  type = {Master's Thesis},
  year = {2004},
}

Propositional Dynamic Logic (PDL) is a very successful variant of modal logic. In the past, many extensions of PDL have been considered to make this logic even more suitable for applications. Unfortunately, the very interesting extension of PDL with negation of programs is undecidable. This work extends PDL with negati on on atomic programs only. The resulting logic is called PDL(neg) and has still an interesting expressive power. It is shown that the satisfiability problem of PDL(neg) is decidable and ExpTime-complete by using Büchi tree automata.

@thesis{ Wal-Mas-04,
  address = {Dresden, Germany},
  author = {Dirk {Walther}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Propositional Dynamic Logic with Negation on Atomic Programs},
  type = {Master's Thesis},
  year = {2004},
}

@thesis{ Tho-Bac-04,
  address = {Dresden, Germany},
  author = {J. {Thomas}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Conformon-P-Systeme},
  type = {Bachelor's Thesis},
  year = {2004},
}

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},
}

Die Arbeit beleuchtet das Forschungsgebiet des DNA-Computing vordergründig aus dem Blickwinkel der Berechenbarkeitstheorie. Universelle sowie platzbeschränkt universelle Modelle des DNA-Computing, deren DNA-basierte Daten auf der Abbildung linearer DNA beruhen, werden untersucht, klassifiziert und als Beschreibungssysteme für Algorithmen angewendet. Mit dem TT6-EH-System und dem Simulationssystem Sisyphus werden zwei universelle DNA-Computing-Modelle eingeführt, deren Modelleigenschaften labornah ausgerichtet sind. Das TT6-EH-System stellt ein endlichkomponentiges verteiltes Splicing-System dar, das sich durch einen statischen Systemaufbau, eine Minimierung der in die Verarbeitung einbezogenen Ressourcen und ein niedriges Abstraktionsniveau der Modelloperationen auszeichnet. Das Simulationssystem Sisyphus berücksichtigt Seiteneffekte der den Modelloperationen zugrundeliegenden molekularbiologischen Prozesse. Zusätzlich besitzt das Modell die Eigenschaften "restriktiv" und "multimengenbasiert". Anhand einer Probleminstanz des NP-vollständigen Rucksackproblems erfolgte eine laborpraktische Verifikation.

@phdthesis{ Hinze-TUD-02,
  address = {Dresden, Germany},
  author = {T. {Hinze}},
  school = {Technische Universit\"at Dresden},
  title = {Universelle Modelle und ausgew\"ahlte Algorithmen des DNA-Computing},
  type = {Doctoral Thesis},
  year = {2002},
}

Concrete domains are an extension of Description Logics (DLs) that allows to integrate reasoning about conceptual knowledge with reasoning about "concrete qualities" of real world entities such as their age, weight, shape, and temporal extension. In this thesis, we perform an in-depth analysis of the computational complexity of reasoning with DLs that are equipped with concrete domains.

The main results are that (i) reasoning with ALC(D), the basic DL ALC extended with a concrete domain D, is PSpace-complete if reasoning with D is in PSpace; (ii) for many seemingly "harmless" extensions of ALC(D), such as the extension with acyclic TBoxes, role conjunction, and inverse roles, the complexity of reasoning leaps from PSpace-completeness to NExpTime-completeness—at least for a large class of concrete domains; and (iii) although, in general, the combination of concrete domains and general TBoxes leads to undecidability of reasoning, there exists an interesting temporal concrete domain that can be combined with general TBoxes without sacrificing decidability. This concrete domain is used to devise a rather powerful interval-based temporal Description Logic.
As a side-track, we illuminate the connection between Description Logics equipped with concrete domains and DLs providing for so-called feature agreement and disagreement constructors. Indeed, this connection turns out to be quite close: in most cases, the complexity of reasoning with a DL providing for concrete domains is identical to the complexity of reasoning with the corresponding DL that offers feature (dis)agreements.

@thesis{ Lutz-PhD-2002,
  address = {Aachen, Germany},
  author = {Carsten {Lutz}},
  school = {Rheinisch-Westf\"{a}lische Technische Hochschule Aachen},
  title = {The Complexity of Description Logics with Concrete Domains},
  type = {Doctoral Thesis},
  year = {2002},
}

@thesis{ Sei-Dip-02,
  address = {Dresden, Germany},
  author = {J. {Seiffert}},
  school = {Technische Universit\"{a}t Dresden},
  title = {Experimentelle und theoretische Aspekte zum Membrane-Computing},
  type = {Diploma Thesis},
  year = {2002},
}

Description Logics (DLs) are used in knowledge-based systems to represent and reason about terminological knowledge of the application domain in a semantically well-defined manner. In this thesis, we establish a number of novel complexity results and give practical algorithms for expressive DLs that provide different forms of counting quantifiers.
We show that, in many cases, adding local counting in the form of qualifying number restrictions to DLs does not increase the complexity of the inference problems, even if binary coding of numbers in the input is assumed. On the other hand, we show that adding different forms of global counting restrictions to a logic may increase the complexity of the inference problems dramatically.

We provide exact complexity results and a practical, tableau based algorithm for the DL SHIQ, which forms the basis of the highly optimized DL system iFaCT.

Finally, we describe a tableau algorithm for the clique guarded fragment (CGF), which we hope will serve as the basis for an efficient implementation of a CGF reasoner.

@thesis{ Tobies-PhD-2001,
  address = {Aachen, Germany},
  author = {Stephan {Tobies}},
  school = {Rheinisch-Westf\"{a}lische Technische Hochschule Aachen},
  title = {Complexity Results and Practical Algorithms for Logics in Knowledge Representation},
  type = {Doctoral Thesis},
  year = {2001},
}

In this thesis we present SAGA, an optimized implementation of a tableau algorithm for the Guarded Fragment of first order predicate logic. The empirical evaluation of this program with different sets of benchmark formulae shows that backjumping and semantic branching are crucial for most formulae, and blocking is efficient even when it is not required by the logic of the corresponding formula. Compared with other systems, the performance of SAGA is similar to that of tableau algorithms for logics in a lower complexity class.

@mastersthesis{ Hladik-Diplom-01,
  address = {Germany},
  author = {J. {Hladik}},
  school = {RWTH Aachen},
  title = {Implementierung eines Entscheidungsverfahrens f{{\"u}}r das Bewachte Fragment der Pr{{\"a}}dikatenlogik},
  type = {Diploma thesis},
  year = {2001},
}

Description Logics denote a family of knowledge representation formalisms that can be used to represent the terminological knowledge of an application domain in a structured and well-defined way. The standard inferences in these logics, like subsumption and instance checking, have been investigated in detail during the last fifteen years, both from a theoretical and a practical point of view. In some applications it has turned out, however, that the optimal support of building and maintaining large knowledge bases requires additional (non-standard) inferences, such as least common subsumer, most specific concept, and matching of concept descriptions. Some systems contain ad hoc implementations of such inferences, mostly without having defined them formally or having investigated their computational complexity. In this work, a formal basis for these inferences is established by providing precise definitions, complete algorithms, and first complexity results.

@thesis{ Kuesters-Diss-2000,
  address = {Aachen, Germany},
  author = {Ralf {K\"{u}sters}},
  school = {Rheinisch-Westf\"{a}lische Technische Hochschule Aachen},
  title = {Non-Standard Inferences in Description Logics},
  type = {Doctoral Thesis},
  year = {2000},
}

In der Prozesstechnik ist, wie in vielen anderen Bereichen, eine strukturierte Darstellung und Speicherung des anwendungsspezifischen Wissens wünschenswert. Im Rahmen einer Kooperation zwischen dem Lehrstuhl für Prozesstechnik und dem Lehr- und Forschungsgebiet Theoretische Informatik wurde bereits nachgewiesen, dass sich Beschreibungslogiken aufgrund ihrer hohen Ausdrucksstärke und mächtigen Inferenzalgorithmen sehr gut für diese Aufgabe eignen. So ermöglichen die standardmäßig von Beschreibungslogik-Systemen bereitgestellten Inferenzdienste beispielsweise die automatische Berechnung der Spezialisierungshierarchie einer Wissensbasis. Es hat sich jedoch herausgestellt, dass sie für eine umfassende Unterstützung der Erstellung und Wartung der Wissensbasis nicht ausreichen.
In dieser Arbeit werden daher die Nicht-Standardinferenzen Least Common Subsumer, Most Specific Concept und Rewriting untersucht, die im Zusammenspiel die Definition neuer Konzepte und damit die Erweiterung und Pflege der Wissensbasis unterstützen. Die Resultate zur Existenz, Berechenbarkeit und Komplexität sowie die Entwicklung vollständiger Algorithmen zur Lösung dieser Inferenzprobleme konzentrieren sich dabei auf Beschreibungslogiken, die bereits erfolgreich in der Prozesstechnik eingesetzt werden.

@thesis{ Molitor-diss,
  address = {Aachen, Germany},
  author = {Ralf {Molitor}},
  school = {Rheinisch-Westf\"{a}lische Technische Hochschule Aachen},
  title = {Unterst\"{u}tzung der Modellierung verfahrenstechnischer Prozesse durch Nicht-Standardinferenzen in Beschreibungslogiken},
  type = {Doctoral Thesis},
  year = {2000},
}

Matching in Description Logics originally has been inroduced by Borgida and McGuinness in order to prune aspects of concept descriptions irrelevant under certain circumstances. In this context, side conditions have been proposed to avoid trivial solutions to matching problems. In this work the computational complexity of matching algorithms is discussed for four common description logics—ALN and three of its sublanguages. Three different problems are considered. Matching modulo equivalence without side conditions, the approach of eliminating acyclic subsumption conditions and the use of fixed point algorithms for solving matching problems under subsumption conditions. As a result, we prove that matching under subsumption conditions can be solved in polynomial time in ALN and its sublanguages.

@mastersthesis{ Brandt-DA-2000,
  address = {Germany},
  author = {S.\ {Brandt}},
  school = {RWTH Aachen},
  title = {Matching under Side Conditions in Description Logics},
  type = {Diploma thesis},
  year = {2000},
}

Im automatischen Beweisen ist der Einsatz von E-Unifikation eine Technik, um allgemein anwendbare Beweisverfahren wie Resolution oder Vervollständigung mit Spezialverfahren zu ergänzen. Diese können zwar nur sehr spezielle Probleme lösen, sind dabei aber besonders effizient. Durch den Einsatz von E-Unifikation wird die Behandlung einer Gleichungstheorie E von dem allgemeinen Beweisverfahren in ein spezielles Unifikationsverfahren verlagert.
Treten in einem Beweisproblem mehrere Gleichungstheorien E0, ... , En auf, so entsteht die Aufgabe, die einzelnen Unifikationsverfahren für diese Theorien zu einem Unifikationsverfahren für die Vereinigung der Theorien E0, ..., En zu kombinieren. Zu diesem Zweck wurden in der Literatur mehrere Kombinationsalgorithmen vorgestellt. Diese beschäftigen sich aber fast ausschließlich mit der Kombination von E-Unifikationsverfahren, die sogenannte vollständige Mengen von Unifikatoren, also Mengen von Lösungen, berechnen. In den letzten Jahren ist zusätzlich das Interesse an E-Unifikationsverfahren gestiegen, die als reine Entscheidungsverfahren arbeiten. Franz Baader und Klaus Schulz haben einen Kombinationsalgorithmus vorgestellt, der auch Entscheidungsverfahren zur E-Unifikation kombinieren kann. Dieser Algorithmus ist allerdings vornehmlich von theoretischem Interesse, da eine direkte Implementierung wegen des enorm großen Suchraums für praktische Probleme nicht geeignet ist.

In der vorliegenden Arbeit wird aufbauend auf dem Algorithmus von Baader und Schulz ein optimiertes Kombinationsverfahren für Entscheidungsverfahren zur E-Unifikation vorgestellt. Der grundlegende Gedanke dieser Optimierung ist, den Suchraum durch den Austausch von Informationen zwischen den Komponentenverfahren der beteiligten Theorien E0, ... , En zu beschränken. Um diesen Informationsaustausch spezifizieren und seine Korrektheit beweisen zu können, wird ein spezieller Formalismus, die sogenannten Constraints, eingeführt. Außerdem wird für drei ausgewählte Theorien vorgestellt, wie bekannte Entscheidungsverfahren für diese Theorien so erweitert werden können, dass sie sich an dem angesprochenen Informationsaustausch beteiligen können. Laufzeittests mit den implementieren Algorithmen zeigen, dass diese Optimierungen tatsächlich zu Unifikationsalgorithmen führen, welche für Probleme in der Praxis einsetzbar sind.

@thesis{ Richts-Diss-1999,
  address = {Aachen, Germany},
  author = {J\"{o}rn {Richts}},
  school = {Rheinisch-Westf\"{a}lische Technische Hochschule Aachen},
  title = {Effiziente Entscheidungsverfahren zur E-Unifikation},
  type = {Doctoral Thesis},
  year = {1999},
}

Im Anwendungsbereich Medizin wird der Einsatz traditioneller Wissensrepräsentationssysteme dadurch erschwert, dass Aussagen und Folgerungen häufig nicht exakt sind. Vielmehr liegen diese oft nur mit einem gewissen Grad an Unschärfe vor. Allerdings gibt es nichtsdestotrotz oft die Anforderung, das entsprechende Wissen geeignet zu formaliseren, um Anwendungssysteme zu entwickeln, die den Mediziner in seiner Ausbildung oder im Alltagsgeschäft unterstützen.
Zum Aufbau eines medizinischen Tutoringsystems im Bereich der Radiologie wird daher im Rahmen dieser Arbeit eine unendlichwertige (fuzzy) Beschreibungslogik entwickelt, welche speziell das in diesem Rahmen vorkommende unscharfe Wissen zu repräsentieren erlaubt.

Die Arbeit umfasst als einen Schwerpunkt die theoretischen Grundlagen der Beschreibungslogik und das darauf aufbauende Schlussfolgerungsverfahren, welches den Ausgangspunkt für ein Computersystem liefert. Über die an dieser Stelle gezeigten Eigenschaften lassen sich für die spätere Anwendung wichtige Aussagen treffen, welche beispielsweise die Korrektheit einer Inferenz in dieser Logik umfassen.

Zum anderen werden aber auch die praktischen Fragestellungen behandelt, die beim Entwurf eines medizinischen Anwendungssystems auftauchen. Ein wichtiger Punkt ist hier die Verarbeitung der medizinischen Fachsprache, die es im Kontext des Ausbildungssystems vollautomatisch in Konstrukte der Wissensrepräsentationssprache zu übersetzen gilt.

@thesis{ Tresp-Diss-1999,
  address = {Aachen, Germany},
  author = {Christopher B. {Tresp}},
  school = {Rheinisch-Westf\"{a}lische Technische Hochschule Aachen},
  title = {Beschreibungslogiken zur Behandlung von unscharfem Wissen im Kontext eines medizinischen Anwendungsszenarios},
  type = {Doctoral Thesis},
  year = {1999},
}

In der hier vorliegenden Arbeit werden verschiedene, aus der Literatur bekannte Klassen monadischer Programmschemata betrachtet. Monadische Programmschemata sind uninterpretierte Programme und stellen damit Programm über potentiell beliebigen Rechenbereichen mit beliebigen einstelligen Grundfunktionen dar. Im Gegensatz zum Äquivalenzbegriff für Programme, bei dem zwei Programme als äquivalent betrachtet werden, wenn sie die gleiche Funktion berechnen, fordert man beim Äquivalenzbegriff für Programmschemata, dass für alle Interpretationen der Grundfunktionen die entstehenden Programme die gleiche Funktion berechnen. Für die Klasse der Ianov-Schemata ist eine Charakterisierung äquivalenter Programmschemata bekannt. Hier wird eine solche Charakterisierung für die Klasse der Dijkstra-Schemata und die Klasse der Kosaraju-Schemata angegeben. Diese Charakterisierung erfolgt durch die Zuordnung von regulären Sprachen bzw. Vektoren von solchen Sprachen, wobei hervorzuheben ist, dass sich die charakterisierenden Sprachen am induktiven Aufbau der jeweiligen Klassen orientieren. Durch die Verwendung dieser Charakterisierungen kann beispielsweise das Äquivalenzproblem für Programmschemata dieser Klassen sehr effizient entschieden werden.
Darüber hinaus wird gezeigt, dass die Schachtelungstiefe von WHILE-Schleifen in Dijkstra-Schemata eine echte semantische Hierarchie von Funktionen, die sogenannte WHILE-Hierarchie, bildet. Dieses Hierarchieresultat zeigt, dass bei Betrachtung beliebiger Rechenbereiche und beliebigen Grundfunktionen der klassische Satz der Rekursionstheorie von S.C. Kleene nicht mehr gilt, der besagt, dass eine einzige WHILE-Schleife zur Programmierung beliebiger Funktionen auf natürlichen Zahlen ausreicht.

@thesis{ Albayrak-Diss-1998,
  address = {Aachen, Germany},
  author = {Can Adam {Albayrak}},
  school = {Rheinisch-Westf\"{a}lische Technische Hochschule Aachen},
  title = {Die WHILE-Hierarchie f\"{u}r Programmschemata},
  type = {Doctoral Thesis},
  year = {1998},
}

This work is concerned with the question of how far terminological knowledge representation systems can support the development of mathematical models of chemical processes. Terminological knowledge representation systems are based on Description Logics, a highly expressive formalism with well-defined semantics, and provide powerful inference services. These system services can be used to support the structuring of the application domain, namely the organised storage of parts of process models. However, the process systems engineering application asks for the extension of the expressive power of already existing Description Logics. These extensions are introduced and investigated with respect to the computational complexity of the corresponding inference problems.

@thesis{ Sattler-diss,
  address = {Aachen, Germany},
  author = {Ulrike {Sattler}},
  school = {Rheinisch-Westf\"{a}lische Technische Hochschule Aachen},
  title = {Terminological Knowledge Representation Systems in a Chemical Engineering Application},
  type = {Doctoral Thesis},
  year = {1998},
}

Formal Methods are becoming more an more important for the development of hardware and software systems. Verification tools support the employment of Formal Methods. This thesis gives an overview of the design and implementation of the verification tool Truth.

@mastersthesis{ Tobies-DA-98,
  address = {Germany},
  author = {Stephan {Tobies}},
  school = {RWTH Aachen},
  title = {Design und Implementierung einer Plattform zur Verifikation verteilter Systeme},
  type = {Diploma thesis},
  year = {1998},
}

The object-oriented data-model VeDa is designed to represent objects as well as steps relevant for the modeling of chemical plants and processes. The main objective of this thesis is to develop a relation which supports the organization of modeling-steps into an hierarchy. This hierarchy facilitates the search for and the reuse of existing steps. It also helps to decide whether a step can be exchanged in a given sequence of steps without loss of executability of that sequence. The first step in the definition of this hierarchy was the development of a language for the specification of classes of modeling-steps. Parallel to this a formalism was developed to formulate pre- and postconditions for individual steps. These conditions characterize the effects of the above named steps. Next, an algorithm is presented that decides interesting properties of these pre- and postconditions such as satisfiability. Finally, it is shown how the formalism developed is used as a basis for both the definition of the hierarchy and an algorithm to check whether a given sequence of steps is executable.

@mastersthesis{ Kr97,
  address = {Germany},
  author = {Claudia {Krobb}},
  school = {RWTH Aachen},
  title = {Entwicklung einer Spezialisierungshierarchie f{\"u}r Modellierungsschritte im objekt-orientierten Datenmodell VeDa},
  type = {Diploma thesis},
  year = {1997},
}

The representation of terminological knowledge may naturally lead to terminological cycles. In addition to descriptive semantics, the meaning of a (cyclic) terminology can also be captured by fixed-point semantics, which were first introduced by B. Nebel. These semantics were analyzed by F. Baader with the help of finite automata for the very small language FL₀, which allows for concept conjunctions and (universal) value-restrictions. This automata theoretic characterization helps deciding which semantic is to prefer in a specific representation task, and in addition, it yields decision procedures and complexity results for subsumption. Since FL₀ is not expressive enough for most practical representation problems, my diploma thesis extends FL₀ to ALN by adding primitive negation and number-restrictions. Beside the characterizations of cyclic ALN-terminologies, in this work the relationship between ALN-terminologies and SL_dis-schemata (which were introduced by M. Buchheit, F. M. Donini, W. Nutt and A. Schaerf) is analyzed. It turns out that SL_dis-schemata can be seen — w.r.t. inconsistency, validity, and subsumption — as special terminologies. Thus, inference problems involving schemata can be reduced to inference problems of the corresponding terminologies.

@mastersthesis{ Kuesters-DA-97,
  address = {Germany},
  author = {Ralf {K{\"u}sters}},
  school = {RWTH Aachen},
  title = {Charakterisierung der Semantik terminologischer Zyklen mit Hilfe endlicher Automaten},
  type = {Diploma thesis},
  year = {1997},
}

Im Rahmen dieser Arbeit werden Entscheidbarkeitsprobleme für Erweiterungen der Beschreibungslogik ALC um Konzeptkonstruktoren auf Rollenketten untersucht. Ausgehend von einem regelbasierten Vervollständigungsvefahren, das die Erfüllbarkeit von ALCN(o)-Konzepten entscheidet, wird zunächst versucht, die Konsistenz von ALCN(o)-ABoxen mit Hilfe geeigneter Erweiterungen des Verfahrens zu entscheiden. Die Untersuchungen liefern zum einen für eine spezielle Klasse von (zulässigen) ALCN(o)-ABoxen das gewünschte Entscheidbarkeitsresultat. Zum anderen werden anhand von Beipsielen die Probleme ausführlich diskutiert, die sich (im Beweis der Terminierung) für das Vervollständigungsverfahren und unzulässige ALCN(o)-ABoxen ergeben. Die Entscheidbarkeit des Konsistenzproblems für ALCN(o) bleibt dabei offen. Für das erste Entscheidbarkeitsresultat nutzt man die Levelstruktur-Eigenschaft von ALCN(o) aus. Da die Erweiterung von ALC um Role-Value-Maps auf Rollenketten gleicher Länge (ALC+rvm) ebenfalls die Levelstruktur-Eigenschaft besitzt, untersucht man nun das Erfüllbarkeits- und Subsumtionsproblem für ALC+rvm. Die Entscheidbarkeit dieser Probleme für ALC+rvm bleibt wiederum offen, allerdings gelingt der Nachweis der Endlich-Modell-Eigenschaft für einige Fragmente von ALC+rvm, so daß man für diese Fragmente entsprechende Entscheidbarkeitsresultate erhält.

@mastersthesis{ Molitor97,
  address = {Germany},
  author = {Ralf {Molitor}},
  school = {RWTH Aachen},
  title = {Konsistenz von Wissensbasen in Beschreibungslogiken mit Rollenoperatoren},
  type = {Diploma thesis},
  year = {1997},
}

In dieser Diplomarbeit geht es um die Berechnung einer erweiterten Subsumtionshierarchie mit Hilfe der Merkmalexploration. Die Berechnung einer einfachen Subsumtionshierarchie (Klassifikation) ist häufig als ein Systemdienst in heutigen KR-Systemen realisiert. Die Klassifikation vereinfacht das Schlußfolgerungsproblem während der Laufzeit. Die Informationen, die aus dieser einfachen Hierarchie gewonnen werden können, sind aber sehr beschränkt, da diese Hierarchie keine Auskunft über die Subsumtionsrelationen zwischen den Konjunktionen von Konzeptnamen gibt. Solche Konjunktionen stellen einen großen Teil der zusammengesetzten Eigenschaften dar. Es ist wünschenswert, eine erweiterte Subsumtionshierarchie zu berechnen, die alle Konjunktionen zwischen den definierten Konzeptnamen repräsentiert. Zur Berechnung einer solchen Hierarchie möchte man natürlich so wenig wie möglich den teuren Subsumtionsalgorithmus aufrufen müssen.<p> Das Ziel dieser Arbeit war, diese Aufgabe zu lösen. Hierzu wurden die Resultate aus der Welt der Formalen Begriffsanalyse herangezogen. In diesem Gebiet werden Objekte, Eigenschaften (Merkmale) und die Objekt-Eigenschafts-Beziehung durch formale Kontexte und formale Begriffe dargestellt. Begriffsanalytische Methoden, die von Ganter und Wille entwickelt wurden, ermöglichen die Berechnung der Begriffshierarchie eines gegebenen Kontextes, die als ein vollständiger Verband dargestellt werden kann. <p> Durch die Definition eines geeigneten Kontextes zu einer gegebenen Tbox wurde der Zusammenhang zwischen der Begriffsanalyse und terminologischen Tboxen hergestellt, in der Hoffnung, daß dadurch die Berechnung einer erweiterten Subsumtionshierarchie im oben definierten Sinne ermöglicht wird. In diesem Kontext entsprechen die Merkmale den in der Tbox definierten Konzeptnamen. Entsprechend ist jeder Begriffsinhalt eine Konjunktion zwischen Konzeptnamen. <p> Ganter und Wille haben eine Methode angegeben (Merkmalexploration), durch die man eine minimale Implikationsbasis für einen gegebenen Kontext berechnen kann, auch wenn der Kontext unendlich ist. Diese Basis repräsentiert dann den ganzen Begriffsverband des Kontextes. Die durch die Merkmalexploration berechnete Basis <em>L</em> besteht aus einer minimalen Anzahl von Implikationen, die im Kontext gelten. Die Menge aller im Kontext gültigen Implikationen ist dann genau die Menge aller Implikationen, die aus <em>L</em> folgen. Man berechnet diese Basis für einen gegebenen Kontext, indem man alle sogenannten Pseudoinhalte des Kontextes mit Hilfe einer auf der Potenzmenge der Menge aller Merkmale definierten Ordnung (lektische Ordnung) berechnet. <p> In dem zu einer Tbox geeignet definierten Kontext entspricht diese Basis einer minimalen Repräsentation aller Subsumtionen zwischen den Konjunktionen der definierten Konzeptnamen. Um diese Basis zu berechnen, hat der ,,Gantersche`` Algorithmus einen menschlichen Experten vorausgesetzt, der sich in dem Anwendungsgebiet auskennt und zu jeder Implikation zwischen Merkmalen entscheiden kann, ob sie im Kontext gilt oder nicht. Im Zusammenhang mit Tboxen wird diese Rolle von einem Subsumtionsalgorithmus übernommen. Hierzu wurde ein bekannter, optimierter und regelbasierter Erfüllbarkeitsalgorithmus (funktionaler Algorithmus) zu dem gewünschten Experten erweitert, der eingesetzt im ,,Ganterschen`` Algorithmus die Berechnung der gewünschten Implikationsbasis ermöglicht.

@mastersthesis{ Nassiri97,
  address = {Germany},
  author = {Madjid {Nassiri}},
  school = {RWTH Aachen},
  title = {Berechnung einer erweiterten Subsumtionshierarchie},
  type = {Diploma thesis},
  year = {1997},
}

Bei dem Kombinationsproblem in der Unifikationstheorie geht es darum, Unifikationsalgorithmen für Gleichungstheorien über disjunkten Signaturen zu einem Unifikationsalgorithmus zu kombinieren, der Unifikationsprobleme über der gemischten Signatur, d.h. Unifikationsprobleme in denen Symbole aus verschiedenen Gleichungstheorien vorkommen können, behandeln kann. Eine Erweiterung dieses Problems besteht darin, Termrelationen zu betrachten, die allgemeiner sind, als die Gleichheit modulo einer Gleichungstheorie. Die Klasse der Knuth-Bendix Reduktionsordnungen, die z.B. bei der Vervollständigung von Termersetzungssystemen Verwendung findet, ist ein wichtiges Beispiel solcher Termrelationen.<p> Dazu muß man aber zuerst festlegen, wie diese Relationen auf den gemischten Termen zu interpretieren sind. Dazu existieren zwei Definitionen. Die Definition von Baader und Schulz ist eine algebraische Definition, die auf einer geeigneten Kombination von freien Strukturen basiert. Die Definition von Kirchner und Ringeissen ist hingegen syntaktisch. Sie verwendet Termreduktion und Termabstraktion. In dieser Arbeit wird im wesentlichen gezeigt, daß beide Definitionen äquivalent sind. Anschließend wird gezeigt, wie man ausgehend von einer Modifikation der syntaktischen Definition Entscheidungsverfahren für die Gültigkeit von reinen atomaren Formeln zu einem Entscheidungsverfahren für die Gültigkeit von atomaren Formeln über der gemischten Signatur kombinieren kann.

@mastersthesis{ Ben-Khalifa-DA-96,
  address = {Germany},
  author = {Kamel {Ben-Khalifa}},
  month = {November},
  school = {RWTH Aachen},
  title = {Kombination freier Strukturen},
  type = {Diploma thesis},
  year = {1996},
}

This thesis compares the two most prominent semantic approaches to unification in equational theories. We can show that unification in primal algebras is not a direct instance of unification in monoidal theories. However, it is possible to reduce unification in a given primal algebra to unification in a corresponding monoidal theory. As by-products of this work we have shown that unification in algebras is an instance of unification modulo equational theories, and we have introduced a new notion of equivalence for equational theories.

@mastersthesis{ Leucker-DA-96,
  author = {Martin {Leucker}},
  note = {In German},
  school = {RWTH Aachen, Germany},
  title = {Comparison of Two Semantic Approaches to Unification},
  type = {Diploma Thesis},
  year = {1996},
}

This work investigates general <em>AC</em>-unification, i.e. unification in the combination of free function symbols and free Abelian semigroups, whose function symbols fulfill associativity and commutativity.<p> The three necessary parts of general <em>AC</em>-unification are presented: a combination algorithm, a procedure for elementary <em>AC</em>-unification, and methods for solving systems of diophantine equations. Starting with A. Boudet's unification algorithm for the combination of regular and collapse-free theories, an efficient algorithm for general <em>AC</em>-unification is developed, setting out conditions that must be fulfilled by the solutions of elementary <em>AC</em>-unification. These conditions are used by the procedure for elementary <em>AC</em>-unification whereby further conditions are set out that must be fulfilled by the solutions of the diophantine equations. Then three methods (those of E. Contejean and H. Devie, E. Domenjoud, L. Pottier) for solving systems of diophantine equations are presented. The three methods are compared and evaluated, trying to use the conditions efficiently.<p> Finally some problems which arise from the reuse of <em>AC</em>-unifiers in unification, such as merging, are presented. It is shown that reusing <em>AC</em>-unifiers for partial problems is often worse than solving the entire problem from the beginning.

@thesis{ Ric-Dip-1992,
  address = {Postfach 3049, D--67663 Kaiserslautern, Germany},
  author = {J{\"o}rn {Richts}},
  school = {Fachbereich Informatik, Universit{\"a}t Kaiserslautern},
  title = {Allgemeine {$AC$}-{U}nifikation durch {V}ariablenabstraktion mit {F}remdtermbedingungen},
  type = {Diploma Thesis},
  year = {1992},
}