Chair of Automata Theory at the Institute of Theoretical Computer Science of the Faculty of Computer Science of the Technische Universität Dresden

# Master Theses, Diplomarbeiten, and Bachelor Theses supervised by Prof. Franz Baader

## Master Theses and Diplomarbeiten

### 2016

M.Z. Zia### 2015

T.A. Saisree, P. Lätsch, M. Pensel### 2014

S. Pester, A. Abdrakhmanov### 2013

D. Merz , I. Ceylan , J. Leyva Galano , X. Wu, W. Wang### 2012

O. Fernández Gil, B. Zarrieß, M. Voigt, K. Lehmann### 2011

W. Fu, P. Nutakki, J. A. Mendez, D. Schröder, Eldora### 2010

S. Razniewski, S. Borgwardt, M. Farooque, T. B. Nguyen, C. Knobloch### 2009

A. Mehdi, R. Hausdorf, J. Bauer, M. Lippmann, J. Eichhorn, V. Gutierrez### 2008

J. Viradia, Q. H. Vu, S. Voigt### 2007

N. Novakovic, Y. Bong, C. Huang, C. Haase, F. Stenger, A. Krisnadhi, M. Tayyab, J. Thomas, T. Lau### 2006

D. Dinh-Khac, R. Peñaloza, R. Mudunuri, M. Hintzmann### 2005

E. Karabaev, H. Liu, J. Model, B. Suntisrivaraporn### 2004

M. Milicic, D. Walther### 2002

J. Seiffert

## Bachelor Theses

### 2015

A. Püschel, T. Schick### 2012

P. Nitzsche, M. Roth### 2009

S. Gothan### 2004

J. Thomas

## Master Theses and Diplomarbeiten

## 2016

#### M. Zahid Zia: Finite Herbrand Models for Monadic Clauses with Unary Function Symbols

**Abstract:**
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.

**Download:**
PDF (0.4 MB)

## 2015

#### T. Aparna Saisree: Iterative Ontology Update with Minimum Change

**Abstract:**
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.

**Download:**
PDF (0.5 MB)

#### Paul Lätsch: Simi-Framework for Concept-Similarity-Measures: property analysis and expansion to more powerful Description Logics

**Abstract:** 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.

**Download:**
PDF (0.5 MB)

#### Maximilian Pensel: An Automata Based Approach for Subsumption w.r.t. General Concept Inclusions in the Description Logic FL0

**Abstract:**
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.

**Download:**
PDF (0.56 MB)

## 2014

#### Stephanie Pester: Investigations on an Action Formalism based on the Description Logic ALCQIO

**Abstract:**
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.

**Download:**
PDF (0.71 MB)

#### Adilzhan Abdrakhmanov: Conditions for the Existence of the lcs of EL-concepts w.r.t. General Horn-ALC TBoxes

**Abstract:** 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.

**Download:**
PDF (0.25 MB)

## 2013

#### Dorian Merz: Decidability of Reasoning in ALC with Fuzzy Concrete Domains

**Abstract:**
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.

**Download:**
PDF (1 MB)

#### Ismail Ceylan: Context-Sensitive Bayesian Description Logics

**Abstract:**
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.

**Download:**
PDF (0.6 MB)

#### J. Leyva Galano: The Subsumption Problem for FL0 with Greatest Fixed-point Semantics

**Abstract:**
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.

**Download:**
PDF (0.5 MB)

#### X. Wu: Enhancing Ontology Matching Using Logic-based Reasoning

**Abstract:**
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.

**Download:**
PDF (1.1 MB)

#### W. Wang: Error-Tolerant Direct Bases

**Abstract:**
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%.

**Download:**
PDF (0.4 MB)

## 2012

#### O. Fernández Gil: Hybrid Unification in the Description Logic EL

**Abstract:**
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.

**Download:**
PDF (0.5 MB)

#### B. Zarrieß: Existenz des Least Common Subsumers in der Beschreibungslogik EL bezüglich genereller Terminologien

**Abstract:**
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.

**Download:**
PDF (0.5 MB)

#### M. Voigt: On Polymorphic Types with Enforceable Linearity for A Quantum Lambda Calculus

**Abstract:**
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.

**Download:**
PDF (1.2 MB)

#### K. Lehmann: A Framework for Semantic Invariant Similarity Measures for ELH Concept Descriptions

**Abstract:**
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.

**Download:**
PDF (0.5 MB)

## 2011

#### W. Fu: Labeling-extensions of General Tableaux with Many Values

**Abstract:**
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.

#### P. Nutakki: Specializing conjunctive queries in the EL-family for better comprehension of result sets.

**Abstract:**
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.

**Download:**
PDF (2.1 MB)

#### J. A. Mendez: A Classification Algorithm For ELHIfR+

**Abstract:**
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 here.

**Download:**
PDF (0.36 MB)

#### D. Schröder: About Expanding Spiking Neural P Systems

**Abstract:**
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.

**Download:**
PDF (0.87 MB)

#### Eldora: Correcting Access Restrictions: a Range-based Approach

**Abstract:**
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].

**Download:**
PDF (1.0 MB)

## 2010

#### S. Razniewski: Completeness of Queries over Incomplete Databases

**Abstract**
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.

**Download:**
PDF (0.68 MB)

#### S. Borgwardt: The Infimum Problem as a Generalization of the Inclusion Problem for Automata

**Abstract:**
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.

**Download:**
PDF (0.66 MB)

#### M. Farooque: A Study on Satisfiability in Fuzzy Description Logics

**Abstract:**
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.

#### T. B. Nguyen: Unification in Description Logic EL without Top Constructor

**Abstract:**
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.

**Download:**
PDF (0.41 MB)

#### C. Knobloch: Beschreibung formaler Sprachen mittels DNA-Rekombination in Ciliaten

## 2009

#### A. Mehdi: Integrate Action Formalisms into Linear Temporal Description Logics

**Abstract:**
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.

**Download:**
PDF (0.32 MB)

#### R. Hausdorf: Intramolekulares Gene Assembly

**Abstract:**
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.

**Download:**
PDF (2.10 MB)

#### J. Bauer: Model Exploration to Support Understanding of Ontologies

**Abstract:**
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.

**Download:**
PDF (0.7 MB)

#### M. Lippmann: Runtime Verification Using Temporal Description Logics

**Abstract:**
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.

**Download:**
PDF (0.46 MB)

#### J. Eichhorn: Untersuchung von konjunktiven Abfragen über verteilte Ontologien mit dem Fokus auf E-Connections

**Abstract:**
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.

**Download:**
PDF (1.0 MB)

#### V. Gutierrez: Branching Temporal Description Logics: Reasoning About CTL-ALC And CTL-EL Concepts

**Abstract:**
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.

**Download:**
PDF (0.38 MB)

## 2008

#### J. Viradia: Reasoning with Boolean ABoxes

**Abstract:**
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.

**Download:**
PDF (0.28 MB)

#### Q. H. Vu: Subsumption in the Description Logic in ELHIf_{R+} w.r.t. General TBoxes.

**Abstract:**
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.

**Download:**
PDF (0.36 MB)

#### S. Voigt: Modellierung zellbiologischer Prozesse mittels Brane- und κ-Kalkül

**Abstract:**
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.

**Download:**
PDF (0.64 MB)

## 2007

#### N. Novakovic: Proof-theoretic Approach to Deciding Subsumption and Computing Least Common Subsumer in EL w.r.t. Hybrid TBoxes

**Abstract:**
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.

**Download:**
PDF (0.32 MB)

#### Y. Bong: Description Logic ABox updates revisited

**Abstract:**
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.

**Download:**
PDF (0.39 MB)

#### C. Huang: Non-standard inference for explaining subsumption in the description logic EL with general concept inclusions and complex role inclusions.

**Abstract:**
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.

**Download:**
PDF (0.42 MB)

#### C. Haase: Complexity of Subsumption in Extensions of EL

**Abstract:**
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.

**Download:**
PDF (0.72 MB)

#### F. Stenger: Adaptionen von Prozesskalkülen für eine Anwendung in der Systembiologie

**Abstract:**
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.

**Download:**
PDF (0.62 MB)

#### A. Krisnadhi: Data Complexity of Instance Checking in the EL Family of Description Logics

**Abstract:**
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.

**Download:**
PDF (0.88 MB)

#### M. Tayyab: Analysis of Pinpointing Algorithms for the Description Logic ALC

**Abstract:**
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.

**Download:**
PDF (0.25 MB)

#### J. Thomas: Äquivalenz von in-vivo- und in-vitro-Modellen im Natural-Computing

#### T. Lau: Molekulares Self-Assembly

## 2006

#### D. Dinh-Khac: Two Types of Key Constraints in Description Logics with Concrete Domains

**Abstract:**
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.

**Download:**
PDF (0.54 MB)

#### R. Peñaloza: Optimization of emptiness test of Büchi automata on infinite trees

**Abstract:**
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.

**Download:**
PDF (0.24 MB)

#### R. Mudunuri: What Makes a Description Logic Knowledge Base Hard? A First Empirical Approach

**Abstract:**
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.

#### M. Hintzmann: Verifikation von DNA-basierten Programmen

## 2005

#### E. Karabaev: Reasoning in the Description Logic EL extended with an n-ary existential quantifier

**Abstract:**
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.

**Download:**
PDF (0.4 MB)

#### H. Liu: Matching in Description Logics with Existential Restrictions and Terminological Cycles

**Abstract:**
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.

**Download:**
PS (0.49 MB)

#### J. Model: Subsumtion in EL bezüglich hybrider TBoxen

**Abstract:**
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.

**Download:**
PS (1.2 MB)

#### B. Suntisrivaraporn: Optimization and Implementation of Subsumption Algorithms for the Description Logic EL with cyclic TBoxes and General Concept Inclusion Axioms

**Abstract:**
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.

**Download:**
PDF (0.43 MB)

## 2004

#### M. Milicic: Description Logics with Concrete Domains and Functional Dependencies

**Abstract:**
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.

**Download:**
PS (0.7 MB)

#### D. Walther: Propositional Dynamic Logic with Negation on Atomic Programs

**Abstract:**
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 stil l 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.

**Download:**
PDF (0.29 MB)

## 2002

#### J. Seiffert: Experimentelle und theoretische Aspekte zum Membrane-Computing

## Bachelor Theses

## 2015

#### A. Püschel: Spiking Neural P-Systeme

#### T. Schick: Hybrides Membrane-Quantum Computing

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

**Download:**
PDF (0.58 MB)

## 2012

#### P. Nitzsche: Universalitätsresultate für Watson-Crick-Automaten

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

**Download:**
PDF (0.69 MB)

#### M. Roth: Untersuchung der Berechnungsstärke eines gewichteten Insertion-Deletion-Systems

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

**Download:**
PDF (1.1 MB)

## 2009

#### S. Gothan: Spiking Neural P-Systeme

**Abstract:**
Natural Computing, das Rechnen mit Molekülen, ist ein Teilgebiet des
Unconventional Computing, in dem alternative Rechnermodelle konstruiert
werden, mit deren Hilfe schwere Probleme der Informatik effizient gelöst
werden sollen. Ein Vertreter des Molekularen Rechnens in-vivo, das Prozesse
untersucht, die in der Natur ablaufen, sind die P-Systeme. Sie beschreiben
Stofftransport in einem hierarchischen System von Membranen. Auf der
Grundlage dieser P-Systeme wurden die Spiking Neural P-Systeme entwickelt,
die die Ausbreitung elektrischer Impulse in einem Netz von Neuronen
modellieren und auf diese Weise Zahlenmengen berechnen. In der Arbeit werden
P-Systeme beschrieben und darauf aufbauend eine formale Definition der
Spiking Neural P-Systeme erarbeitet. Für dieses Modell wird die
Turing-Vollständigkeit bewiesen und gezeigt, wie mit Spiking Neural
P-Systemen des SAT-Problems in konstanter Zeit gelöst werden kann.

**Download:**
PDF (0.42 MB)

## 2004

#### J. Thomas: Conformon-P-Systeme

Back to the hompage of the Chair of Automata Theory.