Master and bachelor Theses (including Diplomarbeiten) supervised by Prof. Franz Baader

Master Theses (including Diplomarbeiten)

• 2009

  A. Mehdi

  R. Hausdorf

  J. Bauer

  M. Lippmann

  J. Eichhorn

  V. Gutierrez

• 2008

  J. Viradia

  Q. Vu

  S. Voigt

• 2007

  Y. Bong

  C. Huang

  C. Haase

  F. Stenger

  A. Krisnadhi

  M. Tayyab

  J. Thomas

  T. Lau

• 2006

  D. Dinh-Khac

  R. Penaloza

  R. Mudunuri

  M. Hintzmann

• 2005

  E. Karabaev

  H. Liu

  J. Model

  B. Suntisrivaraporn

• 2004

  M. Milicic

  D. Walther

• 2002

  J. Seiffert

Bachelor Theses

• 2009

  S. Gothan

• 2004

  J. Thomas

There are also lists of our papers and technical reports.

Integrate Action Formalisms into Linear Temporal Description Logics

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 (0.32MB, PDF)

R. Hausdorf

Intramolekulares Gene Assembly

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 (2.10MB, PDF)

J. Bauer

Model Exploration to Support Understanding of Ontologies

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 (0.70MB, PDF)

M. Lippmann

Runtime Verification Using Temporal Description Logics

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 (0.46MB, PDF)

Untersuchung von konjunktiven Abfragen über verteilte Ontologien mit dem Fokus auf E-Connections

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 (1.00MB, PDF)

Branching Temporal Description Logics: Reasoning About CTL-ALC And CTL-EL Concepts

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 CTLALC and CTLEL , 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 CTLALC 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 (0.38MB, PDF)

J. Viradia

Reasoning with Boolean ABoxes

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 (0.28MB, PDF)

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 rst 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 algorithmstill runs in polynomial time in the simple case of ELHIfR+ that does not include inverse and functional roles.

Download (0.36MB, PDF)

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 pi-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 $\kappa$-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 (0.64MB, PDF)

Y. Bong

Description Logic ABox updates revisited

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 (0.39MB, PDF)

C. Huang

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

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 (0.42MB, PDF)

C. Haase

Complexity of Subsumption in Extensions of EL

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 (0.72MB, PDF)

F. Stenger

Adaptionen von Prozesskalkülen für eine Anwendung in der Systembiologie

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 (0.62MB, PDF)

A. Krisnadhi

Data Complexity of Instance Checking in the EL Family of Description Logics

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 (0.88MB, PDF)

M. Tayyab

Analysis of Pinpointing Algorithms for the Description Logic ALC

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 (0.25MB, PDF)

J. Thomas

Äquivalenz von in-vivo- und in-vitro-Modellen im Natural-Computing

T. Lau

Molekulares Self-Assembly

D. Dinh-Khac

Two Types of Key Constraints in Description Logics with Concrete Domains

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 (0.54MB, PDF)

R. Penaloza

Optimization of emptiness test of Buchi automata on infinite trees

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 $\mathcal{ALC}$-satisfiability with respect to empty and acyclic TBoxes is in PSpace.

Download (0.24MB, PDF)

R. Mudunuri

What Makes a Description Logic Knowledge Base Hard? A First Empirical Approach

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

Download (0.74MB, PDF)

E. Karabaev

Reasoning in the Description Logic EL extended with an n-ary existential quantifier

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 (0.40MB, PDF)

Matching in Description Logics with Existential Restrictions and Terminological Cycles

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 (0.49MB, PS)

Subsumtion in EL bezüglich hybrider TBoxen

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 (1.2MB, PS)

Optimization and Implementation of Subsumption Algorithms for the Description Logic EL with cyclic TBoxes and General Concept Inclusion Axioms

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 (0.43MB, PDF)

M. Milicic

Description Logics with Concrete Domains and Functional Dependencies

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 (0.70MB, PS)

Propositional Dynamic Logic with Negation on Atomic Programs

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 Buechi tree automata.

Download (0.29MB, PDF)

J. Seiffert

Experimentelle und theoretische Aspekte zum Membrane--Computing

S. Gothan

Spiking Neural P-Systeme

Download (0.42MB, PDF)

J.Thomas

Conformon-P-Systeme