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

Bachelor Theses


Master Theses and Diplomarbeiten


2016

Adrian Nuradiansyah: Algorithms for Computing Least Common Subsumers w.r.t. General FL0-TBoxes

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

Download:
PDF


Maximilian Marx: Universality Results for Spiking Neural P Systems with Cooperating Rules

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

Download:
PDF


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 ELHIfR+ 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

Download: PDF (0.74 MB)


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


2016

B. Range: Splicing-P-Systeme

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

Download:
PDF


2015

A. Püschel: Spiking Neural P-Systeme

Download: PDF (0.33 MB)


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.