Diploma Theses and Master's Theses

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

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

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

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

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

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

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

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

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

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

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

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

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

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