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

Technical Reports

The list of technical reports is also available as PDF document. There is also a list of our publications and theses.

2017

Maximilian Pensel and Anni-Yasmin Turhan: Making Quantification Relevant again—the case of Defeasible ELbot. 17-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017. See http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

Defeasible Description Logics (DDLs) extend Description Logics with defeasible concept inclusions. Reasoning in DDLs often employs rational or relevant closure according to the (propositional) KLM postulates. If in DDLs with quantification a defeasible subsumption relationship holds between concepts, this relationship might also hold if these concepts appear in existential restrictions. Such nested defeasible subsumption relationships were not detected by earlier reasoning algorithms—neither for rational nor relevant closure. In this report, we present a new approach for ELbot that alleviates this problem for relevant closure (the strongest form of preferential reasoning currently investigated) by the use of typicality models that extend classical canonical models by domain elements that individually satisfy any amount of consistent defeasible knowledge. We also show that a certain restriction on the domain of the typicality models in this approach yields inference results that correspond to the (weaker) more commonly known rational closure.



Franz Baader: Concept Descriptions with Set Constraints and Cardinality Constraints. 17-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017. See http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

We introduce a new description logic that extends the well-known logic ALCQ by allowing the statement of constraints on role successors that are more general than the qualified number restrictions of ALCQ. To formulate these constraints, we use the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA), in which one can express Boolean combinations of set constraints and numerical constraints on the cardinalities of sets. Though our new logic is considerably more expressive than ALCQ, we are able to show that the complexity of reasoning in it is the same as in ALCQ, both without and with TBoxes.



Franz Baader, Stefan Borgwardt, Patrick Koopmann, Ana Ozaki, and Veronika Thost: Metric Temporal Description Logics with Interval-Rigid Names (Extended Version). 17-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017. see https://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

In contrast to qualitative linear temporal logics, which can be used to state that some property will eventually be satisfied, metric temporal logics allow to formulate constraints on how long it may take until the property is satisfied. While most of the work on combining Description Logics (DLs) with temporal logics has concentrated on qualitative temporal logics, there has recently been a growing interest in extending this work to the quantitative case. In this paper, we complement existing results on the combination of DLs with metric temporal logics over the natural numbers by introducing interval-rigid names. This allows to state that elements in the extension of certain names stay in this extension for at least some specified amount of time.



Franz Baader, Stefan Borgwardt, and Marcel Lippmann: Query Rewriting for DL-Lite with n-ary Concrete Domains (Extended Version). 17-04, Chair for Automata Theory, Technische Universität Dresden, Germany, 2017. see https://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

We investigate ontology-based query answering (OBQA) in a setting where both the ontology and the query can refer to concrete values such as numbers and strings. In contrast to previous work on this topic, the built-in predicates used to compare values are not restricted to being unary. We introduce restrictions on these predicates and on the ontology language that allow us to reduce OBQA to query answering in databases using the so-called combined rewriting approach. Though at first sight our restrictions are different from the ones used in previous work, we show that our results strictly subsume some of the existing first-order rewritability results for unary predicates.



Franz Baader, Patrick Koopmann, and Anni-Yasmin Turhan: Using Ontologies to Query Probabilistic Numerical Data (Extended Version). 17-05, Chair for Automata Theory, Technische Universität Dresden, Germany, 2017. See https://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

We consider ontology-based query answering in a setting where some of the data are numerical and of a probabilistic nature, such as data obtained from uncertain sensor readings. The uncertainty for such numerical values can be more precisely represented by continuous probability distributions than by discrete probabilities for numerical facts concerning exact values. For this reason, we extend existing approaches using discrete probability distributions over facts by continuous probability distributions over numerical values. We determine the exact (data and combined) complexity of query answering in extensions of the well-known description logics EL and ALC with numerical comparison operators in this probabilistic setting.



Camille Bourgaux and Anni-Yasmin Turhan: Temporal Query Answering in DL-Lite over Inconsistent Data. 17-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017. see http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

In ontology-based systems that process data stemming from different sources and that is received over time, as in context-aware systems, reasoning needs to cope with the temporal dimension and should be resilient against inconsistencies in the data. Motivated by such settings, this paper addresses the problem of handling inconsistent data in a temporal version of ontology-based query answering. We consider a recently proposed temporal query language that combines conjunctive queries with operators of propositional linear temporal logic and extend to this setting three inconsistency-tolerant semantics that have been introduced for querying inconsistent description logic knowledge bases. We investigate their complexity for DL-LiteR temporal knowledge bases, and furthermore complete the picture for the consistent case.




2016

Claudia Carapelle and Anni-Yasmin Turhan: Decidability of ALCP(D) for concrete domains with the EHD-property. 16-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016.
BibTeX entry  Paper (PDF) 

Abstract:

Reasoning for Description Logics with concrete domains and w.r.t. general TBoxes easily becomes undecidable. However, with some restriction on the concrete domain, decidability can be regained. We introduce a novel way to integrate a concrete domain D into the well known description logic ALC, we call the resulting logic ALCP(D). We then identify sufficient conditions on D that guarantee decidability of the satisfiability problem, even in the presence of general TBoxes. In particular, we show decidability of ALCP(D) for several domains over the integers, for which decidability was open. More generally, this result holds for all negation-closed concrete domains with the EHD-property, which stands for `the existence of a homomorphism is definable'. Such technique has recently been used to show decidability of CTL* with local constraints over the integers.



Franz Baader and Oliver Fernández Gil: Extending Description Logic tEL(deg) with Acyclic TBoxes. 16-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016. See http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

In a previous paper, we have introduced an extension of the lightweight Description Logic EL that allows us to define concepts in an approximate way. For this purpose, we have defined a graded membership function deg, which for each individual and concept yields a number in the interval [0,1] expressing the degree to which the individual belongs to the concept. Threshold concepts C t for   in <, <=, >, >= then collect all the individuals that belong to C with degree  t. We have then investigated the complexity of reasoning in the Description Logic tEL(deg), which is obtained from EL by adding such threshold concepts. In the present paper, we extend these results, which were obtained for reasoning without TBoxes, to the case of reasoning w.r.t. acyclic TBoxes. Surprisingly, this is not as easy as might have been expected. On the one hand, one must be quite careful to define acyclic TBoxes such that they still just introduce abbreviations for complex concepts, and thus can be unfolded. On the other hand, it turns out that, in contrast to the case of EL, adding acyclic TBoxes to tEL(deg) increases the complexity of reasoning by at least on level of the polynomial hierarchy.



Franz Baader, Pavlos Marantidis, and Alexander Okhotin: Approximately Solving Set Equations. 16-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016. See http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

Unification with constants modulo the theory of an associative (A), commutative (C) and idempotent (I) binary function symbol with a unit (U) corresponds to solving a very simple type of set equations. It is well-known that solvability of systems of such equations can be decided in polynomial time by reducing it to satisfiability of propositional Horn formulae. Here we introduce a modified version of this problem by no longer requiring all equations to be completely solved, but allowing for a certain number of violations of the equations. We introduce three different ways of counting the number of violations, and investigate the complexity of the respective decision problem, i.e., the problem of deciding whether there is an assignment that solves the system with at most violations for a given threshold value .



Franz Baader, Pavlos Marantidis, and Alexander Okhotin: Approximate Unification in the Description Logic FL0. 16-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016. See http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

Unification in description logics (DLs) has been introduced as a novel inference service that can be used to detect redundancies in ontologies, by finding different concepts that may potentially stand for the same intuitive notion. It was first investigated in detail for the DL FL0, where unification can be reduced to solving certain language equations. In order to increase the recall of this method for finding redundancies, we introduce and investigate the notion of approximate unification, which basically finds pairs of concepts that ``almost'' unify. The meaning of ``almost'' is formalized using distance measures between concepts. We show that approximate unification in FL0 can be reduced to approximately solving language equations, and devise algorithms for solving the latter problem for two particular distance measures.



Franz Baader and Oliver Fernández Gil: Decidability and Complexity of Threshold Description Logics Induced by Concept Similarity Measures. 16-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016. See http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

In a recent research paper, we have proposed an extension of the light-weight Description Logic (DL) EL in which concepts can be defined in an approximate way. To this purpose, the notion of a graded membership function m, which instead of a Boolean membership value 0 or 1 yields a membership degree from the interval [0,1], was introduced. Threshold concepts can then, for example, require that an individual belongs to a concept C with degree at least 0.8. Reasoning in the threshold DL tel(m) obtained this way of course depends on the employed graded membership function m. The paper defines a specific such function, called deg, and determines the exact complexity of reasoning in tel(deg). In addition, it shows how concept similarity measures (CSMs)   satisfying certain properties can be used to define graded membership functions m , but it does not investigate the complexity of reasoning in the induced threshold DLs tel(m ). In the present paper, we start filling this gap. In particular, we show that computability of   implies decidability of tel(m ), and we introduce a class of CSMs for which reasoning in the induced threshold DLs has the same complexity as in tel(deg).



Franz Baader, Oliver Fernández Gil, and Pavlos Marantidis: Approximation in Description Logics: How Weighted Tree Automata Can Help to Define the Required Concept Comparison Measures in FL0. 16-08, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016. See http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

Recently introduced approaches for relaxed query answering, approximately defining concepts, and approximately solving unification problems in Description Logics have in common that they are based on the use of concept comparison measures together with a threshold construction. In this paper, we will briefly review these approaches, and then show how weighted automata working on infinite trees can be used to construct computable concept comparison measures for FL0 that are equivalence invariant w.r.t. general TBoxes. This is a first step towards employing such measures in the mentioned approximation approaches.




2015

Francesco Kriegel: NextClosures – Parallel Exploration of Constrained Closure Operators. 15-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry 

Abstract:

It is well-known that the canonical implicational base of all implications valid w.r.t. a closure operator can be obtained from the set of all pseudo-closures. NextClosures is a parallel algorithm to compute all closures and pseudo-closures of a closure operator in a graded lattice, e.g., in a powerset. Furthermore, the closures and pseudo-closures can be constrained; partially known closure operators can be explored.



Francesco Kriegel: Model-Based Most-Specific Concept Descriptions and Least Common Subsumers in ALEQN(Self). 15-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry 

Abstract:

Model-based most-specific concept descriptions are a useful means to compactly represent all knowledge on a certain individual of an interpretation that is expressible in the underlying description logic. Existing approaches only cover their construction in the case of EL and FLE w.r.t. greatest fixpoint semantics, and the case of EL w.r.t. a role-depth bound, respectively. This document extends the results towards the more expressive description logic ALEQN(Self) w.r.t. role-depth bounds and also gives a method for the computation of least common subsumers.



Franz Baader, Stefan Borgwardt, and Barbara Morawska: Dismatching and Local Disunification in EL. 15-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic EL to disunification since negative constraints on unifiers can be used to avoid unwanted unifiers. While decidability of the solvability of general EL-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint must be ground, and local solvability of disunification problems, where we restrict the attention to solutions that are built from so-called atoms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of (general) disunification problems.



Stephan Böhme and Marcel Lippmann: Description Logics of Context with Rigid Roles Revisited. 15-04, Chair of Automata Theory, TU Dresden, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

To represent and reason about contextualized knowledge often two-dimensional Description Logics (DLs) are employed, where one DL is used to describe contexts (or possible worlds) and the other DL is used to describe the objects, i.e. the relational structure of the specific contexts. Previous approaches for DLs of context that combined pairs of DLs resulted in undecidability in those cases where so-called rigid roles are admitted, i.e. if parts of the relational structure are the same in all contexts. In this paper, we present a novel combination of pairs of DLs and show that reasoning stays decidable even in the presence of rigid roles. We give complexity results for various combinations of DLs involving ALC, SHOQ, and EL.



Stefan Borgwardt, Marco Cerami, and Rafael Peñaloza: Subsumption in Finitely Valued Fuzzy EL. 15-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Fuzzy Description Logics (DLs) are used to represent and reason about vague and imprecise knowledge that is inherent to many application domains. It was recently shown that the complexity of reasoning in finitely-valued fuzzy DLs is often not higher than that of the underlying classical DL. We show that this does not hold for fuzzy extensions of the light-weight DL EL, which is used in many biomedical ontologies, under the Lukasiewicz semantics. The complexity of reasoning increases from PTime to ExpTime, even if only one additional truth value is introduced. The same lower bound holds also for infinitely-valued Lukasiewicz extensions of EL.



Stefan Borgwardt and Veronika Thost: LTL over EL Axioms. 15-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

We investigate a combination of EL-axioms with operators of the linear-temporal logic LTL. The complexity of deciding satisfiability is reduced when compared to ALC-LTL, but we also identify one setting where it remains the same. We additionally investigate the setting where GCIs are restricted to hold globally (at all time points), in which case the problem is PSpace-complete.



Stefan Borgwardt and Veronika Thost: Temporal Query Answering in EL. 15-08, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Context-aware systems use data about their environment for adaptation at runtime, e.g., for optimization of power consumption or user experience. Ontology-based data access (OBDA) can be used to support the interpretation of the usually large amounts of data. OBDA augments query answering in databases by dropping the closed-world assumption (i.e., the data is not assumed to be complete any more) and by including domain knowledge provided by an ontology. We focus on a recently proposed temporalized query language that allows to combine conjunctive queries with the operators of the well-known propositional temporal logic LTL. In particular, we investigate temporalized OBDA w.r.t. ontologies in the DL EL, which allows for efficient reasoning and has been successfully applied in practice. We study both data and combined complexity of the query entailment problem.



Franz Baader, Gerhard Brewka, and Oliver Fernández Gil: Adding Threshold Concepts to the Description Logic EL. 15-09, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

We introduce an extension of the lightweight Description Logic EL that allows us to define concepts in an approximate way. For this purpose, we use a graded membership function, which for each individual and concept yields a number in the interval [0,1] expressing the degree to which the individual belongs to the concept. Threshold concepts C  t for   in <,<=,>,>= then collect all the individuals that belong to C with degree   t. We generalize a well-known characterization of membership in EL concepts to construct a specific graded membership function deg, and investigate the complexity of reasoning in the Description Logic tel(deg), which extends EL by threshold concepts defined using deg. We also compare the instance problem for threshold concepts of the form C> t in tel(deg) with the relaxed instance queries of Ecke et al.



Benjamin Zarrieß and Jens Claßen: Verification of Knowledge-Based Programs over Description Logic Actions. 15-10, Chair of Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html
BibTeX entry  Paper (PDF) 

Abstract:

A knowledge-based program defines the behavior of an agent by combining primitive actions, programming constructs and test conditions that make explicit reference to the agent's knowledge. In this paper we consider a setting where an agent is equipped with a Description Logic (DL) knowledge base providing general domain knowledge and an incomplete description of the initial situation. We introduce a corresponding new DL-based action language that allows for representing both physical and sensing actions, and that we then use to build knowledge-based programs with test conditions expressed in the epistemic DL. After proving undecidability for the general case, we then discuss a restricted fragment where verification becomes decidable. The provided proof is constructive and comes with an upper bound on the procedure's complexity.



Stefan Borgwardt and Rafael Peñaloza: Infinitely Valued Gödel Semantics for Expressive Description Logics. 15-11, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Fuzzy Description Logics (FDLs) combine classical Description Logics with the semantics of Fuzzy Logics in order to represent and reason with vague knowledge. Most FDLs using truth values from the interval [0,1] have been shown to be undecidable in the presence of a negation constructor and general concept inclusions. One exception are those FDLs whose semantics is based on the infinitely valued Gödel t-norm (G). We extend previous decidability results for the FDL G-ALC to deal with complex role inclusions, nominals, inverse roles, and qualified number restrictions. Our novel approach is based on a combination of the known crispification technique for finitely valued FDLs and an automata-based procedure for reasoning in G-ALC.



Veronika Thost, Jan Holste, and Özgür Özçep: On Implementing Temporal Query Answering in DL-Lite. 15-12, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2015.
BibTeX entry  Paper (PDF) 

Abstract:

Ontology-based data access augments classical query answering over fact bases by adopting the open-world assumption and by including domain know-ledge provided by an ontology. We implemented temporal query answering w.r.t. ontologies formulated in the Description Logic DL-Lite. Focusing on temporal conjunctive queries (TCQs), which combine conjunctive queries via the operators of propositional linear temporal logic, we regard three approaches for answering them: an iterative algorithm that considers all data available; a window-based algorithm; and a rewriting approach, which translates the TCQs to be answered into SQL queries. Since the relevant ontological knowledge is already encoded into the latter queries, they can be answered by a standard database system. Our evaluation especially shows that implementations of both the iterative and the window-based algorithm answer TCQs within a few milliseconds, and that the former achieves a constant performance, even if data is growing over time.



Daniel Borchmann, Felix Distel, and Francesco Kriegel: Axiomatization of General Concept Inclusions from Finite Interpretations. 15-13, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Description logic knowledge bases can be used to represent knowledge about a particular domain in a formal and unambiguous manner. Their practical relevance has been shown in many research areas, especially in biology and the semantic web. However, the tasks of constructing knowledge bases itself, often performed by human experts, is difficult, time-consuming and expensive. In particular the synthesis of terminological knowledge is a challenge every expert has to face. Because human experts cannot be omitted completely from the construction of knowledge bases, it would therefore be desirable to at least get some support from machines during this process. To this end, we shall investigate in this work an approach which shall allow us to extract terminological knowledge in the form of general concept inclusions from factual data, where the data is given in the form of vertex and edge labeled graphs. As such graphs appear naturally within the scope of the Semantic Web in the form of sets of RDF triples, the presented approach opens up the possibility to extract terminological knowledge from the Linked Open Data Cloud. We shall also present first experimental results showing that our approach has the potential to be useful for practical applications.



Francesco Kriegel: Learning General Concept Inclusions in Probabilistic Description Logics. 15-14, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Probabilistic interpretations consist of a set of interpretations with a shared domain and a measure assigning a probability to each interpretation. Such structures can be obtained as results of repeated experiments, e.g., in biology, psychology, medicine, etc. A translation between probabilistic and crisp description logics is introduced and then utilised to reduce the construction of a base of general concept inclusions of a probabilistic interpretation to the crisp case for which a method for the axiomatisation of a base of GCIs is well-known.



Stefan Borgwardt and Veronika Thost: Temporal Query Answering in DL-Lite with Negation. 15-16, Chair for Automata Theory, Technische Universität Dresden, Germany, 2015.
BibTeX entry  Paper (PDF) 

Abstract:

Ontology-based query answering augments classical query answering in databases by adopting the open-world assumption and by including domain knowledge provided by an ontology. We investigate temporal query answering w.r.t. ontologies formulated in DL-Lite, a family of description logics that captures the conceptual features of relational databases and was tailored for efficient query answering. We consider a recently proposed temporal query language that combines conjunctive queries with the operators of propositional linear temporal logic (LTL). In particular, we consider negation in the ontology and query language, and study both data and combined complexity of query entailment.



Franz Baader, Stefan Borgwardt, and Marcel Lippmann: Temporal Conjunctive Queries in Expressive DLs with Non-simple Roles. 15-17, Chair for Automata Theory, Technische Universität Dresden, Germany, 2015.
BibTeX entry  Paper (PDF) 

Abstract:

In Ontology-Based Data Access (OBDA), user queries are evaluated over a set of facts under the open world assumption, while taking into account background knowledge given in the form of a Description Logic (DL) ontology. In order to deal with dynamically changing data sources, temporal conjunctive queries (TCQs) have recently been proposed as a useful extension of OBDA to support the processing of temporal information. We extend the existing complexity analysis of TCQ entailment to very expressive DLs underlying the OWL 2 standard, and in contrast to previous work also allow for queries containing transitive roles.



Stefan Borgwardt and Rafael Peñaloza: A Tableau Algorithm for SROIQ under Infinitely Valued Gödel Semantics. 15-18, Chair for Automata Theory, Technische Universität Dresden, Germany, 2015.
BibTeX entry  Paper (PDF) 

Abstract:

Fuzzy description logics (FDLs) are knowledge representation formalisms capable of dealing with imprecise knowledge by allowing intermediate membership degrees in the interpretation of concepts and roles. One option for dealing with these intermediate degrees is to use the so-called Gödel semantics. Despite its apparent simplicity, developing reasoning techniques for expressive FDLs under this semantics is a hard task. We present a tableau algorithm for deciding consistency of a SROIQ ontology under Gödel semantics. This is the first algorithm that can handle the full expressivity of SROIQ as well as the full Gödel semantics.



Benjamin Zarrieß and Jens Claßen: Decidable Verification of Golog Programs over Non-Local Effect Actions. 15-19, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2015. Extended version. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

The Golog action programming language is a powerful means to express high-level behaviours in terms of programs over actions defined in a Situation Calculus theory. In particular for physical systems, verifying that the program satisfies certain desired temporal properties is often crucial, but undecidable in general, the latter being due to the language's high expressiveness in terms of first-order quantification and program constructs. So far, approaches to achieve decidability involved restrictions where action effects either had to be context-free (i.e. not depend on the current state), local (i.e. only affect objects mentioned in the action's parameters), or at least bounded (i.e. only affect a finite number of objects). In this paper, we present a new, more general class of action theories (called acyclic) that allows for context-sensitive, non-local, unbounded effects, i.e. actions that may affect an unbounded number of possibly unnamed objects in a state-dependent fashion. We contribute to the further exploration of the boundary between decidability and undecidability for Golog, showing that for acyclic theories in the two-variable fragment of first-order logic, verification of CTL* properties of programs over ground actions is decidable.




2014

Franz Baader and Marcel Lippmann: Runtime Verification Using a Temporal Description Logic Revisited. 14-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Formulae of linear temporal logic (LTL) can be used to specify (wanted or unwanted) properties of a dynamical system. In model checking, the system's behaviour is described by a transition system, and one needs to check whether all possible traces of this transition system satisfy the formula. In runtime verification, one observes the actual system behaviour, which at any point in time yields a finite prefix of a trace. The task is then to check whether all continuations of this prefix to a trace satisfy (violate) the formula. More precisely, one wants to construct a monitor, i.e., a finite automaton that receives the finite prefix as input and then gives the right answer based on the state currently reached. In this paper, we extend the known approaches to LTL runtime verification in two directions. First, instead of propositional LTL we use the more expressive temporal logic ALC-LTL, which can use axioms of the Description Logic (DL) ALC instead of propositional variables to describe properties of single states of the system. Second, instead of assuming that the observed system behaviour provides us with complete information about the states of the system, we assume that states are described in an incomplete way by ALC-knowledge bases. We show that also in this setting monitors can effectively be constructed. The (double-exponential) size of the constructed monitors is in fact optimal, and not higher than in the propositional case. As an auxiliary result, we show how to construct Büchi automata for ALC-LTL-formulae, which yields alternative proofs for the known upper bounds of deciding satisfiability in ALC-LTL.



Stefan Borgwardt: The Complexity of Fuzzy Description Logics over Finite Lattices with Nominals. 14-02, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

The complexity of reasoning in fuzzy description logics (DLs) over finite lattices usually does not exceed that of the underlying classical DLs. This has recently been shown for the logics between L-IALC and L-ISCHI using a combination of automata- and tableau-based techniques. In this report, this approach is modified to deal with nominals and constants in L-ISCHOI. Reasoning w.r.t. general TBoxes is ExpTime-complete, and PSpace-completeness is shown under the restriction to acyclic terminologies in two sublogics. The latter implies two previously unknown complexity results for the classical DLs ALCHO and SO.



Franz Baader and Barbara Morawska: Matching with respect to general concept inclusions in the Description Logic EL. 14-03, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics (DLs) almost 20 years ago, motivated by applications in the Classic system. For the DL EL, it was shown in 2000 that the matching problem is NP-complete. It then took almost 10 years before this NP-completeness result could be extended from matching to unification in EL. The next big challenge was then to further extend these results from matching and unification without a TBox to matching and unification w.r.t. a general TBox, i.e., a finite set of general concept inclusions. For unification, we could show some partial results for general TBoxes that satisfy a certain restriction on cyclic dependencies between concepts, but the general case is still open. For matching, we solve the general case in this paper: we show that matching in EL w.r.t. general TBoxes is NP-complete by introducing a goal-oriented matching algorithm that uses non-deterministic rules to transform a given matching problem into a solved form by a polynomial number of rule applications. We also investigate some tractable variants of the matching problem.



Rafael Peñaloza, Veronika Thost, and Anni-Yasmin Turhan: Conjunctive Query Answering in Rough EL. 14-04, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Rough Description Logics have recently been studied as a means for representing and reasoning with imprecise knowledge. Real-world applications need to exploit reasoning over such knowledge in an efficient way. We describe how the combined approach to query answering can be extended to the rough setting. In particular, we extend both the canonical model and the rewriting procedure such that rough queries over rough EL ontologies can be answered by considering this information alone.



Yue Ma and Rafael Peñaloza: Towards Parallel Repair Using Decompositions. 14-05, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Ontology repair remains one of the main bottlenecks for the development of ontologies for practical use. Many automated methods have been developed for suggesting potential repairs, but ultimately human intervention is required for selecting the adequate one, and the human expert might be overwhelmed by the amount of information delivered to her. We propose a decomposition of ontologies into smaller components that can be repaired in parallel. We show the utility of our approach for ontology repair, provide algorithms for computing this decomposition through standard reasoning, and study the complexity of several associated problems.



Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Reasoning with Temporal Properties over Axioms of DL-Lite. 14-06, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2014. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Recently, a lot of research has combined description logics (DLs) of the DL-Lite family with temporal formalisms. Such logics are proposed to be used for situation recognition and temporalized ontology-based data access. In this report, we consider DL-Lite-LTL, in which axioms formulated in a member of the DL-Lite family are combined using the operators of propositional linear-time temporal logic (LTL). We consider the satisfiability problem of this logic in the presence of so-called rigid symbols whose interpretation does not change over time. In contrast to more expressive temporalized DLs, the computational complexity of this problem is the same as for LTL, even w.r.t. rigid symbols.



Michel Ludwig and Rafael Peñaloza: Error-Tolerant Reasoning in the Description Logic EL. 14-11, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Developing and maintaining ontologies is an expensive and error-prone task. After an error is detected, users may have to wait for a long time before a corrected version of the ontology is available. In the meantime, one might still want to derive meaningful knowledge from the ontology, while avoiding the known errors. We study error-tolerant reasoning tasks in the description logic . While these problems are intractable, we propose methods for improving the reasoning times by precompiling information about the known errors and using proof-theoretic techniques for computing justifications. A prototypical implementation shows that our approach is feasible for large ontologies used in practice.




2013

Franz Baader, Stefan Borgwardt, and Marcel Lippmann: On the Complexity of Temporal Query Answering. 13-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Ontology-based data access (OBDA) generalizes query answering in databases towards deduction since (i) the fact base is not assumed to contain complete knowledge (i.e., there is no closed world assumption), and (ii) the interpretation of the predicates occurring in the queries is constrained by axioms of an ontology. OBDA has been investigated in detail for the case where the ontology is expressed by an appropriate Description Logic (DL) and the queries are conjunctive queries. Motivated by situation awareness applications, we investigate an extension of OBDA to the temporal case. As query language we consider an extension of the well-known propositional temporal logic LTL where conjunctive queries can occur in place of propositional variables, and as ontology language we use the prototypical expressive DL ALC. For the resulting instance of temporalized OBDA, we investigate both data complexity and combined complexity of the query entailment problem.



Daniel Borchmann: A General Form of Attribute Exploration. 13-02, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

We present a general form of attribute exploration, a knowledge completion algorithm from formal concept analysis. The aim of this generalization is to extend the applicability of attribute exploration by a general description. Additionally, this may also allow for viewing different existing variants of attribute exploration as instances of a general form, as for example exploration on partial contexts.



Yue Ma and Felix Distel: Learning Formal Definitions for Snomed CT from Text. 13-03, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Snomed CT is a widely used medical ontology which is formally expressed in a fragment of the Description Logic EL++. The underlying logics allow for expressive querying, yet make it costly to maintain and extend the ontology. Existing approaches for ontology generation mostly focus on learning superclass or subclass relations and therefore fail to be used to generate Snomed CT definitions. In this paper, we present an approach for the extraction of Snomed CT definitions from natural language texts, based on the distance relation extraction approach. By benefiting from a relatively large amount of textual data for the medical domain and the rich content of Snomed CT, such an approach comes with the benefit that no manually labelled corpus is required. We also show that the type information for Snomed CT concept is an important feature to be examined for such a system. We test and evaluate the approach using two types of texts. Experimental results show that the proposed approach is promising to assist Snomed CT development.



Daniel Borchmann: Exploration by Confidence. 13-04, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Within formal concept analysis, attribute exploration is a powerful tool to semi-automatically check data for completeness with respect to a given domain. However, the classical formulation of attribute exploration does not take into account possible errors which are present in the initial data. We present in this work a generalization of attribute exploration based on the notion of confidence, which will allow for the exploration of implications which are not necessarily valid in the initial data, but instead enjoy a minimal confidence therein.



Stefan Borgwardt, Marcel Lippmann, and Veronika Thost: Temporal Query Answering w.r.t. DL-Lite-Ontologies. 13-05, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2013. Revised version. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Ontology-based data access (OBDA) generalizes query answering in relational databases. It allows to query a database by using the language of an ontology, abstracting from the actual relations of the database. For ontologies formulated in Description Logics of the DL-Lite family, OBDA can be realized by rewriting the query into a classical first-order query, e.g. an SQL query, by compiling the information of the ontology into the query. The query is then answered using classical database techniques. In this report, we consider a temporal version of OBDA. We propose a temporal query language that combines a linear temporal logic with queries over DL-Lite-core-ontologies. This language is well-suited for expressing temporal properties of dynamical systems and is useful in context-aware applications that need to detect specific situations. Using a first-order rewriting approach, we transform our temporal queries into queries over a temporal database. We then present three approaches to answering the resulting queries, all having different advantages and drawbacks.



Benjamin Zarrieß and Anni-Yasmin Turhan: Most Specific Generalizations w.r.t. General EL-TBoxes. 13-06, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

In the area of Description Logics the least common subsumer (lcs) and the most specific concept (msc) are inferences that generalize a set of concepts or an individual, respectively, into a single concept. If computed w.r.t. a general -TBox neither the lcs nor the msc need to exist. So far in this setting no exact conditions for the existence of lcs- or msc-concepts are known. This paper provides necessary and suffcient conditions for the existence of these two kinds of concepts. For the lcs of a fixed number of concepts and the msc we show decidability of the existence in PTime and polynomial bounds on the maximal role-depth of the lcs- and msc-concepts. The latter allows to compute the lcs and the msc, respectively.



Franz Baader, Oliver Fernández Gil, and Barbara Morawska: Hybrid Unification in the Description Logic EL. 13-07, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NP-complete. However, the unification algorithms for EL developed until recently could not deal with ontologies containing general concept inclusions (GCIs). In a series of recent papers we have made some progress towards addressing this problem, but the ontologies the developed unification algorithms can deal with need to satisfy a certain cycle restriction. In the present paper, we follow a different approach. Instead of restricting the input ontologies, we generalize the notion of unifiers to so-called hybrid unifiers. Whereas classical unifiers can be viewed as acyclic TBoxes, hybrid unifiers are cyclic TBoxes, which are interpreted together with the ontology of the input using a hybrid semantics that combines fixpoint and declarative semantics. We show that hybrid unification in EL is NP-complete and introduce a goal-oriented algorithm for computing hybrid unifiers.



Franz Baader and Benjamin Zarrieß: Verification of Golog Programs over Description Logic Actions. 13-08, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 



Stefan Borgwardt, Felix Distel, and Rafael Peñaloza: Goedel Description Logics: Decidability in the Absence of the Finitely-Valued Model Property. 13-09, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

In the last few years there has been a large effort for analysing the computational properties of reasoning in fuzzy Description Logics. This has led to a number of papers studying the complexity of these logics, depending on their chosen semantics. Surprisingly, despite being arguably the simplest form of fuzzy semantics, not much is known about the complexity of reasoning in fuzzy DLs w.r.t. witnessed models over the Goedel t-norm. We show that in the logic G-IALC, reasoning cannot be restricted to finitely-valued models in general. Despite this negative result, we also show that all the standard reasoning problems can be solved in this logic in exponential time, matching the complexity of reasoning in classical ALC.



Benjamin Zarrieß and Jens Claßen: On the Decidability of Verifying LTL Properties of Golog Programs. 13-10, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2013. Extended version. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Golog is a high-level action programming language for controlling autonomous agents such as mobile robots. It is defined on top of a logic-based action theory expressed in the Situation Calculus. Before a program is deployed onto an actual robot and executed in the physical world, it is desirable, if not crucial, to verify that it meets certain requirements (typically expressed through temporal formulas) and thus indeed exhibits the desired behaviour. However, due to the high (first-order) expressiveness of the language, the corresponding verification problem is in general undecidable. In this paper, we extend earlier results to identify a large, non-trivial fragment of the formalism where verification is decidable. In particular, we consider properties expressed in a first-order variant of the branching-time temporal logic CTL*. Decidability is obtained by (1) resorting to the decidable first-order fragment C2 as underlying base logic, (2) using a fragment of Golog with ground actions only, and (3) requiring the action theory to only admit local effects.



Daniel Borchmann: Model Exploration by Confidence with Completely Specified Counterexamples. 13-11, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

We present an extensions of our previous work on axiomatizing confident general concept inclusions in given finite interpretations. Within this extension we allow external experts to interactively provide counterexamples to general concept inclusions with otherwise enough confidence in the given data. This extensions allows us to distinguish between erroneous counterexamples in the data and rare, but valid counterexamples.



Andreas Ecke and Anni-Yasmin Turhan: Similarity Measures for Computing Relaxed Instances w.r.t. General EL-TBoxes. 13-12, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

The notion of concept similarity is central to several ontology tasks and can be employed to realize relaxed versions of classical reasoning services. In this paper we investigate the reasoning service of answering instance queries in a relaxed fashion, where the query concept is relaxed by means of a concept similarity measure (CSM). To this end we investigate CSMs that assess the similarity of EL-concepts defined w.r.t. a general EL-TBox. We derive such a family of CSMs from a family of similarity measures for finite interpretations and show in both cases that the resulting measures enjoy a collection of formal properties. These properties allow us to devise an algorithm for computing relaxed instances w.r.t. general EL-TBoxes, where users can specify the `appropriate' notion of similarity by instanciating our CSM appropriately.




2012

Franz Baader and Alexander Okhotin: Solving Language Equations and Disequations Using Looping Tree Automata with Colors. 12-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

We extend previous results on the complexity of solving language equations with one-sided concatenation and all Boolean operations to the case where also disequations (i.e., negated equations) may occur. To show that solvability of systems of equations and disequations is still in ExpTime, we introduce a new type of automata working on infinite trees, which we call looping automata with colors. As applications of these results, we show new complexity results for disunification in the description logic FL0 and for monadic set constraints with negation. We believe that looping automata with colors may also turn out to be useful in other applications.



Franz Baader, Stefan Borgwardt, and Barbara Morawska: SAT Encoding of Unification in ELHR+ w.r.t. Cycle-Restricted Ontologies. 12-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Unification in Description Logics has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the Description Logic EL, which is used to define several large biomedical ontologies, unification is NP-complete. An NP unification algorithm for EL based on a translation into propositional satisfiability (SAT) has recently been presented. In this report, we extend this SAT encoding in two directions: on the one hand, we add general concept inclusion axioms, and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the translation to be complete, however, the ontology needs to satisfy a certain cycle restriction. The SAT translation depends on a new rewriting-based characterization of subsumption w.r.t. ELHR+-ontologies.



Franz Baader, Stefan Borgwardt, and Barbara Morawska: Computing Minimal EL-Unifiers is Hard. 12-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Unification has been investigated both in modal logics and in description logics, albeit with different motivations. In description logics, unification can be used to detect redundancies in ontologies. In this context, it is not sufficient to decide unifiability, one must also compute appropriate unifiers and present them to the user. For the description logic EL, which is used to define several large biomedical ontologies, deciding unifiability is an NP-complete problem. It is known that every solvable EL-unification problem has a minimal unifier, and that every minimal unifier is a local unifier. Existing unification algorithms for EL compute all minimal unifiers, but additionally (all or some) non-minimal local unifiers. Computing only the minimal unifiers would be better since there are considerably less minimal unifiers than local ones, and their size is usually also quite small. In this paper we investigate the question whether the known algorithms for EL-unification can be modified such that they compute exactly the minimal unifiers without changing the complexity and the basic nature of the algorithms. Basically, the answer we give to this question is negative.



Stefan Borgwardt and Rafael Peñaloza: Consistency in Fuzzy Description Logics over Residuated De Morgan Lattices. 12-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Fuzzy description logics can be used to model vague knowledge in application domains. This paper analyses the consistency and satisfiability problems in the description logic SHI with semantics based on a complete residuated De Morgan lattice. The problems are undecidable in the general case, but can be decided by a tableau algorithm when restricted to finite lattices. For some sublogics of SHI, we provide upper complexity bounds that match the complexity of crisp reasoning.



Franz Baader, Stefan Borgwardt, and Barbara Morawska: A Goal-Oriented Algorithm for Unification in ELHR+ w.r.t. Cycle-Restricted Ontologies. 12-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NP-complete. A goal-oriented NP unification algorithm for EL that uses nondeterministic rules to transform a given unification problem into solved form has recently been presented. In this report, we extend this goal-oriented algorithm in two directions: on the one hand, we add general concept inclusion axioms (GCIs), and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the algorithm to be complete, however, the ontology consisting of the GCIs and role axioms needs to satisfy a certain cycle restriction.



Daniel Borchmann: On Confident GCIs of Finite Interpretations. 12-06, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

In the work of Baader and Distel, a method has been proposed to axiomatize all general concept inclusions (GCIs) expressible in the description logic ELbot and valid in a given interpretation I. This provides us with an effective method to learn ELbot ontologies from interpretations, which itself can be seen as a different representation of linked data. In another report, we have extended this approach to handle errors in the data. This has been done by not only considering valid GCIs but also those whose confidence is above a certain threshold c. In the present work, we shall extend the results by describing another way to compute bases of confident GCIs. We furthermore provide experimental evidence that this approach can be useful for practical applications. We finally show that the technique of unravelling can also be used to effectively turn confident ELgfpbot bases into ELbot bases.




2011

Franz Baader, Nguyen Thanh Binh, Stefan Borgwardt, and Barbara Morawska: Unification in the Description Logic EL Without the Top Concept. 11-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of considerably lower complexity than unification in other DLs of similarly restricted expressive power. However, EL allows the use of the top concept, which represents the whole interpretation domain, whereas the large medical ontology SNOMED CT makes no use of this feature. Surprisingly, removing the top concept from EL makes the unification problem considerably harder. More precisely, we will show in this paper that unification in EL without the top concept is PSpace-complete.



Stefan Borgwardt and Rafael Peñaloza: Complementation and Inclusion of Weighted Automata on Infinite Trees: Revised Version. 11-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Weighted automata can be seen as a natural generalization of finite state automata to more complex algebraic structures. The standard reasoning tasks for unweighted automata can also be generalized to the weighted setting. In this report we study the problems of intersection, complementation, and inclusion for weighted automata on infinite trees and show that they are not harder than reasoning with unweighted automata. We also present explicit methods for solving these problems optimally.



Rafael Peñaloza: Towards a Tableau Algorithm for Fuzzy ALC with Product T-norm. 11-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Very recently, the tableau-based algorithm for deciding consistency of general fuzzy DL ontologies over the product t-norm was shown to be incorrect, due to a very weak blocking condition. In this report we take the first steps towards a correct algorithm by modifying the blocking condition, such that the (finite) structure obtained through the algorithm uniquely describes an infinite system of quadratic constraints. We show that this procedure terminates, and is sound and complete in the sense that the input is consistent iff the corresponding infinite system of constraints is satisfiable.



Stefan Borgwardt and Barbara Morawska: Finding Finite Herbrand Models. 11-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

We show that finding finite Herbrand models for a restricted class of first-order clauses is ExpTime-complete. A Herbrand model is called finite if it interprets all predicates by finite subsets of the Herbrand universe. The restricted class of clauses consists of anti-Horn clauses with monadic predicates and terms constructed over unary function symbols and constants. The decision procedure can be used as a new goal-oriented algorithm to solve linear language equations and unification problems in the description logic FL0. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.



Franz Baader, Stefan Borgwardt, and Barbara Morawska: Unification in the Description Logic EL w.r.t. Cycle-Restricted TBoxes. 11-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. The inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of significantly lower complexity than unification in other DLs of similarly restricted expressive power. However, the unification algorithms for EL developed so far cannot deal with general concept inclusion axioms (GCIs). This paper makes a considerable step towards addressing this problem, but the GCIs our new unification algorithm can deal with still need to satisfy a certain cycle restriction.



Stefan Borgwardt and Rafael Peñaloza: Undecidability of Fuzzy Description Logics. 11-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Fuzzy description logics (DLs) have been investigated for over two decades, due to their capacity to formalize and reason with imprecise concepts. Very recently, it has been shown that for several fuzzy DLs, reasoning becomes undecidable. Although the proofs of these results differ in the details of each specific logic considered, they are all based on the same basic idea. In this report, we formalize this idea and provide sufficient conditions for proving undecidability of a fuzzy DL. We demonstrate the effectiveness of our approach by strengthening all previously-known undecidability results and providing new ones. In particular, we show that undecidability may arise even if only crisp axioms are considered.




2010

Franz Baader, Marcel Lippmann, and Hongkai Liu: Adding Causal Relationships to DL-based Action Formalisms. 10-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2010. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

In the reasoning about actions community, causal relationships have been proposed as a possible approach for solving the ramification problem, i.e., the problem of how to deal with indirect effects of actions. In this paper, we show that causal relationships can be added to action formalisms based on Description Logics without destroying the decidability of the consistency and the projection problem.



Franz Baader and Barbara Morawska: SAT Encoding of Unification in EL. 10-04, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2010. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

The Description Logic EL is an inexpressive knowledge representation language, which nevertheless has recently drawn considerable attention in the knowledge representation and the ontology community since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, EL is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in EL is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power. In this paper, we introduce a new NP-algorithm for solving unification problem in EL, which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state of the art SAT solvers when implementing an EL-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that EL-unification is in NP that is much simpler than the one given in our previous paper on EL-unification.



Rafael Peñaloza and Anni-Yasmin Turhan: Completion-based computation of least common subsumers with limited role-depth for EL and Prob-EL01. LTCS-10-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2010. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

The least common subsumer (lcs) w.r.t general EL-TBoxes does not need to exists in general due to cyclic axioms. In this report we present an algorithm for computing role-depth bounded EL-lcs based on the completion algorithm for EL. We extend this computation algorithm to a recently introduced probabilistic variant of EL: Prob-EL-01.



Rafael Peñaloza and Anni-Yasmin Turhan: Completion-based computation of most specific concepts with limited role-depth for EL and Prob-EL01. LTCS-10-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2010. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

In Description Logics the reasoning service most specific concept (msc) constructs a concept description that generalizes an ABox individual into a concept description. For the Description Logic EL the msc may not exist, if computed with respect to general EL-TBoxes or cyclic ABoxes. However, it is still possible to find a concept description that is the msc up to a fixed role-depth, i.e. with respect to a maximal nesting of quantifiers. In this report we present a practical approach for computing the role-depth bounded msc, based on the polynomial-time completion algorithm for EL. We extend these methods to ProbEL-01, which is a probabilistic variant of EL. Together with the companion report LTCS-10-02 this report devises computation methods for the bottom-up construction of knowledge bases for EL and ProbEL-01.



Stefan Borgwardt and Rafael Peñaloza: Complementation and Inclusion of Weighted Automata on Infinite Trees. LTCS-10-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2010. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Weighted automata can be seen as a natural generalization of finite state automata to more complex algebraic structures. The standard reasoning tasks for unweighted automata can also be generalized to the weighted setting. In this report we study the problems of intersection, complementation and inclusion for weighted automata on infinite trees and show that they are not harder than reasoning with unweighted automata. We also present explicit methods for solving these problems optimally.




2009

Conrad Drescher, Hongkai Liu, Franz Baader, Steffen Guhlemann, Uwe Petersohn, Peter Steinke, and Michael Thielscher: Putting ABox Updates into Action. 09-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2009. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

When trying to apply recently developed approaches for updating Description Logic ABoxes in the context of an action programming language, one encounters two problems. First, updates generate so-called Boolean ABoxes, which cannot be handled by traditional Description Logic reasoners. Second, iterated update operations result in very large Boolean ABoxes, which, however, contain a huge amount of redundant information. In this paper, we address both issues from a practical point of view.



Franz Baader, Martin Knechtel, and Rafael Peñaloza: Computing Boundaries for Reasoning in Sub-Ontologies. 09-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2009. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Consider an ontology O where every axiom is labeled with an element of a lattice L. Then every element l of L determines a sub-ontology Ol, which consists of the axioms of O whose labels are greater or equal to l. These labels may be interpreted as required access rights, in which case Ol is the sub-ontology that a user with access right l is allowed to see, or as trust levels, in which case Ol consists of those axioms that we trust with level at least l. Given a consequence C (such as a subsumption relationship between concepts) that follows from the whole ontology O, we want to know from which of the sub-ontologies Ol, determined by lattice elements l, C still follows. However, instead of reasoning with Ol in the deployment phase of the ontology, we want to pre-compute this information during the development phase. More precisely, we want to compute what we call a boundary for C, i.e., an element mC of L such that C follows from Ol iff l is smaller or equal to mC. In this paper we show that, under certain restrictions on the elements l used to define the sub-ontologies, such a boundary always exists, and we describe black-box approaches for computing it that are generalizations of approaches for axiom pinpointing in description logics. We also present first experimental results that compare the efficiency of these approaches on real-world ontologies.



Rafael Peñaloza and Barış Sertkaya: On the Complexity of Axiom Pinpointing in Description Logics. 09-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2009. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

We investigate the computational complexity of axiom pinpointing in Description Logics, which is the task of finding minimal subsets of a knowledge base that have a given consequence. We consider the problems of enumerating such subsets with and without order, and show hardness results that already hold for the propositional Horn fragment, or for the Description Logic . We show complexity results for several other related decision and enumeration problems for these fragments that extend to more expressive logics. In particular we show that hardness of these problems depends not only on expressivity of the fragment but also on the shape of the axioms used.



Franz Baader, Hongkai Liu, and Anees ul Mehdi: Integrate Action Formalisms into Linear Temporal Description Logics. LTCS-09-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2009. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

The verification problem for action logic programs with non-terminating behaviour is in general undecidable. In this paper, we consider a restricted setting in which the problem becomes decidable. On the one hand, we abstract from the actual execution sequences of a non-terminating program by considering infinite sequences of actions defined by a Büchi automaton. On the other hand, we assume that the logic underlying our action formalism is a decidable description logic rather than full first-order predicate logic.




2008

Franz Baader, Silvio Ghilardi, and Carsten Lutz: LTL over Description Logic Axioms. 08-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2008. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can occur within DL concept descriptions. In this setting, reasoning usually becomes quite hard if rigid roles, i.e., roles whose interpretation does not change over time, are available. In this paper, we consider the case where temporal operators are allowed to occur only in front of DL axioms (i.e., ABox assertions and general concept inclusion axioms), but not inside of concepts descriptions. As the temporal component, we use linear temporal logic (LTL) and in the DL component we consider the basic DL ALC. We show that reasoning in the presence of rigid roles becomes considerably simpler in this setting.



Felix Distel: Model-based Most Specific Concepts in Description Logics with Value Restrictions. 08-04, Institute for theoretical computer science, TU Dresden, Dresden, Germany, 2008. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Non-standard inferences are particularly useful in the bottom-up construction of ontologies in Description Logics. One of the more common non-standard reasoning tasks is the most specific concept (msc) for an ABox-individual. In this paper we present similar non-standard reasoning task: model-based most specific concepts (model-mscs). We show that, although they look similar to ABox-mscs their computational behaviour can be different. We present constructions for model-mscs in the logics FLO and FLE with cyclic TBoxes and for ALC with acyclic TBoxes. Since subsumption in FLE with cyclic TBoxes has not been examined previously, we present a characterization of subsumption and give a construction for the least common subsumer in this setting.



Franz Baader and Felix Distel: Exploring finite models in the Description Logic EL\mathrmgfp. 08-05, Institute for Theoretical Computer Science, TU Dresden, Dresden, 2008. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

In a previous ICFCA paper we have shown that, in the Description Logics EL and ELgfp, the set of general concept inclusions holding in a finite model always has a finite basis. In this paper, we address the problem of how to compute this basis efficiently, by adapting methods from formal concept analysis.



Franz Baader and Rafael Peñaloza: Blocking and Pinpointing in Forest Tableaux. LTCS-08-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2008. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Axiom pinpointing has been introduced in Description Logics (DLs) to help the used understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in consideration. Several pinpointing algorithms have been described as extensions of the standard tableau-based reasoning algorithms for deciding consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL, using specific traits of them. In the past, we have developed a general approach for extending tableau-based algorithms into pinpointing algorithms. In this paper we explore some issues of termination of general tableaux and their pinpointing extensions. We also define a subclass of tableaux that allows the use of so-called blocking conditions, which stop the execution of the algorithm once a pattern is found, and adapt the pinpointing extensions accordingly, guaranteeing its correctness and termination.



Franz Baader and Rafael Peñaloza: Pinpointing in Terminating Forest Tableaux. LTCS-08-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2008. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of ``tableau algorithms,'' which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.



Barış Sertkaya: Some Computational Problems Related to Pseudo-intents. LTCS-08-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2008. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

We investigate the computational complexity of several decision, enumeration and counting problems related to pseudo-intents. We show that given a formal context and a set of its pseudo-intents, checking whether this context has an additional pseudo-intent is in coNP and it is at least as hard as checking whether a given simple hypergraph is saturated. We also show that recognizing the set of pseudo-intents is also in coNP and it is at least as hard as checking whether a given hypergraph is the transversal hypergraph of another given hypergraph. Moreover, we show that if any of these two problems turns out to be coNP-hard, then unless P = NP, pseudo-intents cannot be enumerated in output polynomial time. We also investigate the complexity of finding subsets of a given Duquenne-Guigues Base from which a given implication follows. We show that checking the existence of such a subset within a specified cardinality bound is NP-complete, and counting all such minimal subsets is #P-complete.




2007

Franz Baader and Felix Distel: A finite basis for the set of EL-implications holding in a finite model. 07-02, Inst. für Theoretische Informatik, TU Dresden, Dresden, Germany, 2007.
BibTeX entry  Paper (PDF) 

Abstract:

Formal Concept Analysis (FCA) can be used to analyze data given in the form of a formal context. In particular, FCA provides efficient algorithms for computing a minimal basis of the implications holding in the context. In this paper, we extend classical FCA by considering data that are represented by relational structures rather than formal contexts, and by replacing atomic attributes by complex formulae defined in some logic. After generalizing some of the FCA theory to this more general form of contexts, we instantiate the general framework with attributes defined in the Description Logic (DL) EL, and with relational structures over a signature of unary and binary predicates, i.e., models for EL. In this setting, an implication corresponds to a so-called general concept inclusion axiom (GCI) in EL. The main technical result of this report is that, in EL, for any finite model there is a finite set of implications (GCIs) holding in this model from which all implications (GCIs) holding in the model follow.



Boontawee Suntisrivaraporn: Module Extraction and Incremental Classification: A Pragmatic Approach for EL+ Ontologies. LTCS-07-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2007. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

The description logic EL+ has recently proved practically useful in the life science domain with presence of several large-scale biomedical ontologies such as SNOMED CT. To deal with ontologies of this scale, standard reasoning of classification is essential but not sufficient. The ability to extract relevant fragments from a large ontology and to incrementally classify it has become more crucial to support ontology design, maintenance and re-use. In this paper, we propose a pragmatic approach to module extraction and incremental classification for EL+ ontologies and report on empirical evaluations of our algorithms which have been implemented as an extension of the CEL reasoner.




2006

Franz Baader and Alexander Okhotin: On Language Equations with One-sided Concatenation. LTCS-06-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Language equations are equations where both the constants occurring in the equations and the solutions are formal languages. They have first been introduced in formal language theory, but are now also considered in other areas of computer science. In the present paper, we restrict the attention to language equations with one-sided concatenation, but in contrast to previous work on these equations, we allow not just union but all Boolean operations to be used when formulating them. In addition, we are not just interested in deciding solvability of such equations, but also in deciding other properties of the set of solutions, like its cardinality (finite, infinite, uncountable) and whether it contains least/greatest solutions. We show that all these decision problems are ExpTime-complete.



Franz Baader, Bernhard Ganter, Ulrike Sattler, and Baris Sertkaya: Completing Description Logic Knowledge Bases using Formal Concept Analysis. LTCS-06-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

We propose an approach for extending both the terminological and the assertional part of a Description Logic knowledge base by using information provided by the assertional part and by a domain expert. The use of techniques from Formal Concept Analysis ensures that, on the one hand, the interaction with the expert is kept to a minimum, and, on the other hand, we can show that the extended knowledge base is complete in a certain sense.



H. Liu, C. Lutz, M. Milicic, and F. Wolter: Description Logic Actions with general TBoxes: a Pragmatic Approach. LTCS-06-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Action formalisms based on description logics (DLs) have recently been introduced as decidable fragments of well-established action theories such as the Situation Calculus and the Fluent Calculus. However, existing DL action formalisms fail to include general TBoxes as provided by almost all state-of-the-art description logics. We define a DL action formalism that admits general TBoxes, propose a pragmatic approach to addressing the ramification problem that is introduced in this way, show that our formalim is decidable and perform a detailed investigation of its computational complexity.



F. Baader, J. Hladik, and R. Penaloza: PSPACE Automata with Blocking for Description Logics. LTCS-06-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

In Description Logics (DLs), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as satisfiability of concepts. Whereas tableau-based algorithms usually yield worst-case optimal algorithms in the case of PSPACE-complete logics, it is often very hard to design optimal tableau-based algorithms for EXPTIME-complete DLs. In contrast, the automata-based approach is usually well-suited to prove EXPTIME upper-bounds, but its direct application will usually also yield an EXPTIME-algorithm for a PSPACE-complete logic since the (tree) automaton constructed for a given concept is usually exponentially large. In the present paper, we formulate conditions under which an on-the-fly construction of such an exponentially large automaton can be used to obtain a PSPACE-algorithm. We illustrate the usefulness of this approach by proving a new PSPACE upper-bound for satisfiability of concepts w.r.t. acyclic terminologies in the DL SI, which extends the basic DL ALC with transitive and inverse roles.



Rafael Penaloza: Pinpointing in Tableaus. LTCS-06-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Tableau-based decision procedures have been successfully used for solving a wide variety of problems. For some applications, nonetheless, it is desirable not only to obtain a Boolean answer, but also to detect the causes for such a result. In this report, a method for finding explanations on tableau-based procedures is explored, generalizing previous results on the field. The importance and use of the method is shown by means of examples.



Franz Baader and Rafael Penaloza: Axiom Pinpointing in General Tableaux. LTCS-07-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of ``tableaux algorithms,'' which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.




2005

F. Baader, S. Brandt, and C. Lutz: Pushing the EL Envelope. LTCS-05-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Recently, it has been shown that the small DL EL, which allows for conjunction and existential restrictions, has better algorithmic properties than its counterpart FL0, which allows for conjunction and value restrictions. Whereas the subsumption problem in FL0 becomes already intractable in the presence of acyclic TBoxes, it remains tractable in EL even w.r.t. general concept inclusion axioms (GCIs). On the one hand, we will extend the positive result for EL by identifying a set of expressive means that can be added to EL without sacrificing tractability. On the other hand, we will show that basically all other additions of typical DL constructors to EL with GCIs make subsumption intractable, and in most cases even ExpTime-complete. In addition, we will show that subsumption in FL0 with GCIs is ExpTime complete.



F. Baader, M. Milicic, C. Lutz, U. Sattler, and F. Wolter: Integrating Description Logics and Action Formalisms for Reasoning about Web Services. LTCS-05-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Motivated by the need for semantically well-founded and algorithmically managable formalisms for describing the functionality of Web services, we introduce an action formalism that is based on description logics (DLs), but is also firmly grounded on research in the reasoning about action community. Our main contribution is an analysis of how the choice of the DL influences the complexity of standard reasoning tasks such as projection and executability, which are important for Web service discovery and composition.



C. Lutz, D. Walther, and F. Wolter: Quantitative Temporal Logics: PSpace and below. LTCS-05-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

The addition of metric operators to qualitative temporal logics often leads to an increase of the complexity of satisfiability by at least one exponential. In this paper, we exhibit a number of metric extensions of qualitative temporal logics of the real line that do not lead to an increase in computational complexity. The main result states that the language obtained by extending since/until logic of the real line with the operators "sometime within n time units", n coded in binary, is PSpace-complete even without the finite variability assumption. Without qualitative temporal operators the complexity of this language turns out to depend on whether binary or unary coding of parameters is assumed: it is still PSpace-hard under binary coding but in NP under unary coding.



Franz Baader and Silvio Ghilardi: Connecting Many-Sorted Theories. LTCS-05-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions under which decidability of the validity of universal formulae in the component theories transfers to their connection. In addition, we consider variants of the basic connection scheme.



C. Lutz: PDL with Intersection and Converse is Decidable. LTCS-05-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

In its many guises and variations, propositional dynamic logic (PDL) plays an important role in various areas of computer science such as databases, artificial intelligence, and computer linguistics. One relevant and powerful variation is ICPDL, the extension of PDL with intersection and converse. However, although ICPDL has several interesting applications, its computational properties have never been investigated. In this paper, we prove that ICPDL is decidable by developing a translation to the monadic second order logic of infinite trees. Our result has applications in information logic, description logic, and epistemic logic. In particular, we solve a long-standing open problem in information logic. Another virtue of our approach is that it provides a decidability proof that is more transparent than existing ones for PDL with intersection (but without converse).



P. Bonatti, C. Lutz, and F. Wolter: Expressive Non-Monotonic Description Logics Based on Circumscription. LTCS-05-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Recent applications of description logics (DLs) strongly suggest the integration of non-monotonic features into DLs, with particular attention to defeasible inheritance. However, the existing non-monotonic extensions of DLs are usually based on default logic or autoepistemic logic, and have to be seriously restricted in expressive power to preserve decidability of reasoning. In particular, such DLs allow the modelling of defeasible inheritance only in a very restricted form, where non-monotonic reasoning is limited to individuals that are explicitly identified by constants in the knowledge base. In this paper, we consider non-monotonic extensions of expressive DLs based on circumscription. We prove that reasoning in such DLs is decidable even without the usual, strong restrictions in expressive power. We pinpoint the exact computational complexity of reasoning as complete for NPNExp and NExpNP, depending on whether or not the number of minimized and fixed predicates is assumed to be bounded by a constant. These results assume that only concept names, but not role names can be minimized and fixed during minimization. On the other hand, we show that fixing role names during minimization leads to undecidability of reasoning.



C. Lutz and M. Milicic: A Tableau Algorithm for DLs with Concrete Domains and GCIs. LTCS-05-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

We identify a general property of concrete domains that is sufficient for proving decidability of DLs equipped with them and GCIs. We show that some useful concrete domains, such as a temporal one based on the Allen relations and a spatial one based on the RCC-8 relations, have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with such concrete domains.



Franz Baader, Carsten Lutz, Eldar Karabaev, and Manfred Theißen: A New n-ary Existential Quantifier in Description Logics. LTCS-05-08, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Motivated by a chemical process engineering application, we introduce a new concept constructor in Description Logics (DLs), an n-ary variant of the existential restriction constructor, which generalizes both the usual existential restrictions and so-called qualified number restrictions. We show that the new constructor can be expressed in ALCQ, the extension of the basic DL ALC by qualified number restrictions. However, this representation results in an exponential blow-up. By giving direct algorithms for ALC extended with the new constructor, we can show that the complexity of reasoning in this new DL is actually not harder than the one of reasoning in ALCQ. Moreover, in our chemical process engineering application, a restricted DL that provides only the new constructor together with conjunction, and satisfies an additional restriction on the occurrence of roles names, is sufficient. For this DL, the subsumption problem is polynomial.



C. Lutz: Complexity and Succinctness of Public Announcement Logic. LTCS-05-09, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

There is a recent trend of extending epistemic logic (EL) with dynamic operators that allow to express the evolution of knowledge and belief induced by knowledge-changing actions. The most basic such extension is public announcement logic (PAL), which is obtained from EL by adding an operator for truthful public announcements. In this paper, we consider the computational complexity of PAL and show that it coincides with that of EL. This holds in the single- and multi-agent case, and also in the presence of common knowledge operators. We also prove that there are properties that can be expressed exponentially more succinct in PAL than in EL. This shows that, despite the known fact that PAL and EL have the same expressive power, there is a benefit in adding the public announcement operator to EL: it exponentially increases the succinctness of formulas without having negative effects on computational complexity.



H. Liu, C. Lutz, M. Milicic, and F. Wolter: Updating Description Logic ABoxes. LTCS-05-10, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Description logic (DL) ABoxes are a tool for describing the states of affairs in an application domain. In this paper, we consider the problem of updating ABoxes when the state changes. We assume that changes are described at an atomic level, i.e., in terms of possibly negated ABox assertions that involve only atomic concepts and roles. We analyze such basic ABox updates in several standard DLs by investigating whether the updated ABox can be expressed in these DLs and, if so, whether it is computable and what is its size. It turns out that DLs have to include nominals and the ``@'' constructor of hybrid logic (or, equivalently, admit Boolean ABoxes) for updated ABoxes to be expressible. We give algorithms to compute updated ABoxes in several expressive DLs and exhibit ways to avoid an exponential blowup in the size of the original ABox. We also show that an exponential blowup in the size of the update information cannot be avoided (unless every PTime problem is LogTime-parallelizable).




2004

B. Morawska: A nice Cycle Rule for Goal-Directed E-Unification. LTCS-04-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

In this paper we improve a goal-directed E-unification procedure by introducing a new rule, Cycle, for the case of collapsing equations, i.e. equations of the type x = v where x appears in v. In the case of these equations some obviously unnecessary infinite paths of inferences were possible, because it was not known if the inference system is still complete if the inferences were not allowed into positions of x in v. Cycle does not allow such inferences and we prove that the system is complete. Hence we prove that as in other approaches, inferences into variable positions in our goal-directed procedure are not needed.



F. Baader: A Graph-Theoretic Generalization of the Least Common Subsumer and the Most Specific Concept in the Description Logic EL. LTCS-04-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

In two previous papers we have investigates the problem of computing the least common subsumer (lcs) and the most specific concept (msc) for the description logic EL in the presence of terminological cycles that are interpreted with descriptive semantics, which is the usual first-order semantics for description logics. In this setting, neither the lcs nor the msc needs to exist. We were able to characterize the cases in which the lcs/msc exists, but it was not clear whether this characterization yields decidability of the existence problem. In the present paper, we develop a common graph-theoretic generalization of these characterizations, and show that the resulting property is indeed decidable, thus yielding decidability of the existence of the lcs and the msc. This is achieved by expressing the property in monadic second-order logic on infinite trees. We also show that, if it exists, then the lcs/msc can be computed in polynomial time.



S. Brandt: Reasoning in ELH w.r.t. General Concept Inclusion Axioms. LTCS-04-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

In the area of Description Logic (DL) based knowledge representation, research on reasoning w.r.t. general terminologies has mainly focused on very expressive DLs. Recently, though, it was shown for the DL EL, providing only the constructors conjunction and existential restriction, that the subsumption problem w.r.t. cyclic terminologies can be decided in polynomial time, a surprisingly low upper bound. In this paper, we show that even admitting general concept inclusion (GCI) axioms and role hierarchies in EL terminologies preserves the polynomial time upper bound for subsumption. We also show that subsumption becomes co-NP hard when adding one of the constructors number restriction, disjunction, and `allsome', an operator used in the DL K-Rep. An interesting implication of the first result is that reasoning over the widely used medical terminology SNOMED is possible in polynomial time.



S. Brandt: Subsumption and Instance Problem in ELH w.r.t. General TBoxes. LTCS-04-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF) 

Abstract:

Recently, it was shown for the DL EL that subsumption and instance problem w.r.t. cyclic terminologies can be decided in polynomial time. In this paper, we show that both problems remain tractable even when admitting general concept inclusion axioms and simple role inclusion axioms.



C. Lutz and F. Wolter: Modal Logics of Topological Relations. LTCS-04-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

The eight topological RCC8 (or Egenhofer-Franzosa)-relations between spatial regions play a fundamental role in spatial reasoning, spatial and constraint databases, and geographical information systems. In analogy with Halpern and Shoham's modal logic of time intervals based on the Allen relations, we introduce a family of modal logics equipped with eight modal operators that are interpreted by the RCC8-relations. The semantics is based on region spaces induced by standard topological spaces, in particular the real plane. We investigate the expressive power and computational complexity of the logics obtained in this way. It turns our that, similar to Halpern and Shoham's logic, the expressive power is rather natural, but the computational behavior is problematic: topological modal logics are usually undecidable and often not even recursively enumerable. This even holds if we restrict ourselves to classes of finite region spaces or to substructures of region spaces induced by topological spaces. We also analyze modal logics based on the set of RCC5-relations, with similar results.



C. Lutz and M. Milicic: Description Logics with Concrete Domains and Functional Dependencies. LTCS-04-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PDF)  Paper (PS) 

Abstract:

Description Logics (DLs) with concrete domains are a useful tool in many applications. To further enhance the expressive power of such DLs, it has been proposed to add database-style key constraints. Up to now, however, only uniqueness constraints have been considered in this context, thus neglecting the second fundamental family of key constraints: functional dependencies. In this paper, we consider the basic DL with concrete domains , extend it with functional dependencies, and analyze the impact of this extension on the decidability and complexity of reasoning. Though intuitively the expressivity of functional dependencies seems weaker than that of uniqueness constraints, we are able to show that the former have a similarly severe impact on the computational properties: reasoning is undecidable in the general case, and -complete in some slightly restricted variants of our logic.




2003

S. Brandt, A.-Y. Turhan, and R. Küsters: Foundations of non-standard Inferences for Description Logics with transitive Roles and Role Hierarchies. 03-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003.
BibTeX entry  Paper (PS) 

Abstract:

Description Logics (DLs) are a family of knowledge representation formalisms used for terminological reasoning. They have a wide range of applications such as medical knowledge-bases, or the semantic web. Research on DLs has been focused on the development of sound and complete inference algorithms to decide satisfiability and subsumption for increasingly expressive DLs. Non-standard inferences are a group of relatively new inference services which provide reasoning support for the building, maintaining, and deployment of DL knowledge-bases. So far, non-standard inferences are not available for very expressive DLs. In this paper we present first results on non-standard inferences for DLs with transitive roles. As a basis, we give a structural characterization of subsumption for DLs where existential and value restrictions can be imposed on transitive roles. We propose sound and complete algorithms to compute the least common subsumer (lcs).



F. Baader: The Instance Problem and the Most Specific Concept in the Description Logic EL w.r.t. Terminological Cycles with Descriptive Semantics. LTCS-03-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

and non-standard inferences in the presence of terminological cycles for the description logic EL, which allows for conjunctions, existential restrictions, and the top concept. Regarding standard inference problems, it was shown there that the subsumption problem remains polynomial for all three types of semantics usually considered for cyclic definitions in description logics, and that the instance problem remains polynomial for greatest fixpoint semantics. Regarding non-standard inference problems, it was shown that, w.r.t. greatest fixpoint semantics, the least common subsumer and the most specific concept always exist and can be computed in polynomial time, and that, w.r.t. descriptive semantics, the least common subsumer need not exist. The present report is concerned with two problems left open by this previous work, namely the instance problem and the problem of computing most specific concepts w.r.t. descriptive semantics, which is the usual first-order semantics for description logics. We will show that the instance problem is polynomial also in this context. Similar to the case of the least common subsumer, the most specific concept w.r.t. descriptive semantics need not exist, but we are able to characterize the cases in which it exists and give a decidable sufficient condition for the existence of the most specific concept. Under this condition, it can be computed in polynomial time.



B. Morawska: Completness of E-unification with eager Variable Elimination. LTCS-03-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

The report contains a proof of completeness of a goal-directed inference system for general E-unification with eager Variable Elimination. The proof is based on an analysis of a concept of ground, equational proof. The theory of equational proofs is developed in the first part. Solving variables in a goal is then shown to be reflected in defined transformations of an equational proof. The termination of these transformations proves termination of inferences with eager Variable Elimination.



C. Lutz and D. Walther: PDL with Negation of Atomic Programs. LTCS-03-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Propositional dynamic logic (PDL) is one of the most successful variants of modal logic. To make it even more useful for applications, many extensions of PDL have been considered in the literature. A very natural and useful such extension is with negation of programs. Unfortunately, it is long-known that reasoning with the resulting logic is undecidable. In this paper, we consider the extension of PDL with negation of atomic programs, only. We argue that this logic is still useful, e.g. in the context of description logics, and prove that satisfiability is decidable and ExpTime-complete using an approach based on Buechi tree automata.



F. Baader, Silvio Ghilardi, and Cesare Tinelli: A New Combination Procedure for the Word Problem that Generalizes Fusion Decidability Results in Modal Logics. LTCS-03-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics—whose combination is not disjoint since they share the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.




2002

S. Brandt and A.-Y. Turhan: An Approach for Optimizing ALE-Approximation of ALC-Concepts. 02-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

An approximation of an ALC-concept by an ALE-concept can be computed in double exponential time. Consequently, one needs powerful optimization techniques for approximating an entire unfoldable TBox. Addressing this issue we identify a special form of ALC-concepts, which can be divided into parts s.t. each part can be approximated independently. This independent approximation in turn facilitates caching during the computation of approximation.



C. Lutz: Reasoning about Entity Relationship Diagrams with Complex Attribute Dependencies. LTCS-02-01, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2002. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Entity Relationship (ER) diagrams are among the most popular formalisms for the support of database design. To aid database designers in building (extended) ER schemas, Description Logics (DLs) have been proposed and successfully used as a tool for reasoning about such schemas. In this paper, we propose the extension of ER diagrams with dependencies on attributes and show how such dependencies can be translated into DLs with concrete domains. The result is an integrated approach to reasoning with conceptual models and attribute dependencies.



F. Baader: Terminological Cycles in a Description Logic with Existential Restrictions. LTCS-02-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Cyclic definitions in description logics have until now been investigated only for description logics allowing for value restrictions. Even for the most basic language FL0, which allows for conjunction and value restrictions only, deciding subsumption in the presence of terminological cycles is a PSPACE-complete problem. This report investigates subsumption in the presence of terminological cycles for the language EL, which allows for conjunction and existential restrictions. In contrast to the results for FL0, subsumption in EL remains polynomial, independent of whether we use least fixpoint semantics, greatest fixpoint semantics, or descriptive semantics. These results are shown via a characterization of subsumption through the existence of certain simulation relations between nodes of the description graph associated with a given cyclic terminology.



C. Lutz, C. Areces, I. Horrocks, and U. Sattler: Keys, Nominals, and Concrete Domains. LTCS-02-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Many description logics (DLs) combine knowledge representation on an abstract, logical level with an interface to "concrete" domains such as numbers and strings with built-in predicates such as <, +, and prefix-of. These hybrid DLs have turned out to be quite useful for reasoning about conceptual models of information systems, and as the basis for expressive ontology languages. We propose to further extend such DLs with key constraints that allow the expression of statements like "US citizens are uniquely identified by their social security number". Based on this idea, we introduce a number of natural description logics and perform a detailed analysis of their decidability and computational complexity. It turns out that naive extensions with key constraints easily lead to undecidability, whereas more careful extensions yield NExpTime-complete DLs for a variety of useful concrete domains.



C. Lutz, U. Sattler, and L. Tendera: The Complexity of Finite Model Reasoning in Description Logics. LTCS-02-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

We analyze the complexity of finite model reasoning in the description logic ALCQI, i.e. ALC augmented with qualifying number restrictions, inverse roles, and general TBoxes. It turns out that all relevant reasoning tasks such as concept satisfiability and ABox consistency are ExpTime-complete, regardless of whether the numbers in number restrictions are coded unarily or binarily. Thus, finite model reasoning with ALCQI is not harder than standard reasoning with ALCQI.



I. Horrocks and U. Sattler: Decidability of SHIQ with Complex Role Inclusion Axioms. LTCS-02-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Motivated by medical terminology applications, we investigate the decidability of an expressive and prominent DL, SHIQ, extended with role inclusion axioms of the form R o S => T (where "o" denotes composition of binary relations). It is well-known that a naive such extension leads to undecidability, and thus we restrict our attention to axioms of the form R o S => R or S o R => R, which is the most important form of axioms in the applications that motivated this extension. Surprisingly, this extension is still undecidable. However, it turns out that restricting our attention further to acyclic sets of such axioms, we regain decidability. We present a tableau-based decision procedure for this DL and report on its implementation, which behaves well in practise and provides important additional functionality in a medical terminology application.



F. Baader: Least Common Subsumers, Most Specific Concepts, and Role-Value-Maps in a Description Logic with Existential Restrictions and Terminological Cycles. LTCS-02-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002. See http://lat.inf.tu-dresden.de/research/reports.html.
BibTeX entry  Paper (PS) 

Abstract:

In a previous report we have investigates subsumption in the presence of terminological cycles for the description logic EL, which allows conjunctions, existential restrictions, and the top concept, and have shown that the subsumption problem remains polynomial for all three types of semantics usually considered for cyclic definitions in description logics. This result depends on a characterization of subsumption through the existence of certain simulation relations on the graph associated with a terminology. In the present report we will use this characterization to show how the most specific concept and the least common subsumer can be computed in EL with cyclic definitions. In addition, we show that subsumption in EL (with or without cyclic definitions) remains polynomial even if one adds a certain restricted form of global role-value-maps to EL. In particular, this kind of role-value-maps can express transitivity of roles.




2001

F. Baader, S. Brandt, and R. Küsters: Matching under Side Conditions in Description Logics. 01-02, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Whereas matching in Description Logics is now relatively well-investigated, there are only very few formal results on matching under additional side conditions, though these side conditions were already present in the original paper by Borgida and McGuinness introducing matching in DLs. The present paper closes this gap for the DL and its sublanguages.



F. Baader and S. Tobies: The Inverse Method Implements the Automata Approach for Modal Satisfiability. 01-03, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Tableaux-based decision procedures for satisfiability of modal and description logics behave quite well in practice, but it is sometimes hard to obtain exact worst-case complexity results using these approaches, especially for EXPTIME-complete logics.In contrast, automata-based approaches often yield algorithms for which optimal worst-case complexity can easily be proved. However, the algorithms obtained this way are usually not only worst-case, but also best-case exponential: they first construct an automaton that is always exponential in the size of the input, and then apply the (polynomial) emptiness test to this large automaton. To overcome this problem, one must try to construct the automaton ``on-the-fly'' while performing the emptiness test. In this paper we will show that Voronkov's inverse method for the modal logic K can be seen as an on-the-fly realization of the emptiness test done by the automata approach for K. The benefits of this result are two-fold. First, it shows that Voronkov's implementation of the inverse method, which behaves quite well in practice, is an optimized on-the-fly implementation of the automata-based satisfiability procedure for K. Second, it can be used to give a simpler proof of the fact that Voronkov's optimizations do not destroy completeness of the procedure. We will also show that the inverse method can easily be extended to handle global axioms, and that the correspondence to the automata approach still holds in this setting. In particular, the inverse method yields an EXPTIME-algorithm for satisfiability in K w.r.t. global axioms.



F. Baader and R. Küsters: Unification in a Description Logic with Transitive Closure of Roles. 01-05, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Unification of concept descriptions was introduced by Baader and Narendran as a tool for detecting redundancies in knowledge bases. It was shown that unification in the small description logic FL0, which allows for conjunction, value restriction, and the top concept only, is already ExpTime-complete. The present paper shows that the complexity does not increase if one additionally allows for composition, union, and transitive closure of roles. It also shows that matching (which is polynomial in FL0) is PSpace-complete in the extended description logic. These results are proved via a reduction to linear equations over regular languages, which are then solved using automata. The obtained results are also of interest in formal language theory.



S. Brandt, R. Küsters, and A.-Y. Turhan: Approximation and Difference in Description Logics. 01-06, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.
BibTeX entry  Paper (PS) 

Abstract:

Approximation is a new inference service in Description Logics first mentioned by Baader, K&uuml;sters, and Molitor. Approximating a concept, defined in one Description Logic, means to translate this concept to another concept, defined in a second typically less expressive Description Logic, such that both concepts are as closely related as possible with respect to subsumption. The present paper provides the first in-depth investigation of this inference task. We prove that approximations from the Description Logic ALC to ALE always exist and propose an algorithm computing them. As a measure for the accuracy of the approximation, we introduce a syntax-oriented difference operator, which yields a concept description that contains all aspects of the approximated concept that are not present in the approximation. It is also argued that a purely semantical difference operator, as introduced by Teege, is less suited for this purpose. Finally, for the logics under consideration, we propose an algorithm computing the difference.



C. Lutz, H. Sturm, F. Wolter, and M. Zakharyaschev: A Tableau Calculus for Temporal Description Logic: The Constant Domain Case. LTCS-01-01, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

We show how to combine the standard tableau system for the basic description logic ALC with Wolper's tableau calculus for propositional temporal logic PTL in order to design a terminating sound and complete tableau-based satisfiability-checking algorithm for the temporal description logic PTLALC interpreted in models with constant domains. We use the method of quasimodels to represent models with infinite domains, and the technique of minimal types to maintain these domains constant. The combination is flexible and can be extended to more expressive description logics or even to decidable fragments of first-order temporal logics.



C. Lutz, U. Sattler, and F. Wolter: Modal Logic and the two-variable fragment. LTCS-01-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

We introduce a modal language L which is obtained from standard modal logic by adding the difference operator and modal operators interpreted by boolean combinations and the converse of accessibility relations. It is proved that L has the same expressive power as the two-variable fragment FO2 of first-order logic but speaks less succinctly about relational structures: if the number of relations is bounded, then L-satisfiability is ExpTime-complete but FO2 satisfiability is NExpTime-complete. We indicate that the relation between L and FO2 provides a general framework for comparing modal and temporal languages with first-order languages.



C. Lutz: Adding Numbers to the SHIQ Description Logic—First Results. LTCS-01-07, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Recently, the Description Logic (DL) SHIQ has found a large number of applications. This success is due to the fact that SHIQ combines a rich expressivity with efficient reasoning, as is demonstrated by its implementation in DL systems such as FaCT and RACER. One weakness of SHIQ, however, limits its usability in several application areas: numerical knowledge such as knowledge about the age, weight, or temperature of real-world entities cannot be adequately represented. In this paper, we propose an extension of SHIQ that aims at closing this gap. The new Description Logic Q-SHIQ, which augments SHIQ by additional, ``concrete domain'' style concept constructors, allows to refer to rational numbers in concept descriptions, and also to define concepts based on the comparison of numbers via predicates such as ``<'' or ``=''. We argue that this kind of expressivity is needed in many application areas such as reasoning about the semantic web. We prove reasoning with Q-SHIQ to be ExpTime-complete (thus not harder than reasoning with SHIQ) by devising an automata-based decision procedure.



I. Horrocks and U. Sattler: Optimised Reasoning for SHIQ. LTCS-01-08, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

The tableau algorithm implemented in the FaCT knowledge representation system decides satisfiability and subsumption in SHIQ, a very expressive description logic providing, e.g., inverse and transitive roles, number restrictions, and general axioms. Intuitively, the algorithm searches for a tree-shaped abstraction of a model. To ensure termination of this algorithm without compromising correctness, it stops expanding paths in the search tree using a so-called ``double-blocking'' condition.

This condition was clearly more exacting than was strictly necessary, but it was assumed that more precisely defined blocking conditions would, on the one hand, make the proof of the algorithm's correctness far more difficult and, on the other hand (and more importantly), be so costly to check as to outweigh any benefit that might be derived.

However, FaCT's failure to solve UML derived knowledge bases led us to reconsider this conjecture and to formulate more precisely defined blocking conditions. We prove that the revised algorithm is still sound and complete, and demonstrate that it greatly improves FaCT's performance - in some cases by more than two orders of magnitude.




2000

F. Baader, R. Küsters, and R. Molitor: Rewriting Concepts Using Terminologies – Revisited. 00-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

The problem of rewriting a concept given a terminology can informally be stated as follows: given a terminology T (i.e., a set of concept definitions) and a concept description C that does not contain concept names defined in T, can this description be rewritten into a "related better" description E by using (some of) the names defined in T? In this paper, we first introduce a general framework for the rewriting problem in description logics, and then concentrate on one specific instance of the framework, namely the minimal rewriting problem (where "better" means shorter, and "related" means equivalent). We investigate the complexity of the decision problem induced by the minimal rewriting problem for the languages FL0, ALN, ALE, and ALC, and then introduce an algorithm for computing (minimal) rewritings for the languages ALE and ALN. Finally, we sketch other interesting instances of the framework. Our interest for the minimal rewriting problem stems from the fact that algorithms for non-standard inferences, such as computing least common subsumers and matchers, usually produce concept descriptions not containing defined names. Consequently, these descriptions are rather large and hard to read and comprehend. First experiments in a chemical process engineering application show that rewriting can reduce the size of concept descriptions obtained as least common subsumers by almost two orders of magnitude.



R. Küsters and R. Molitor: Computing Most Specific Concepts in Description Logics with Existential Restrictions. 00-05, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.
BibTeX entry  Paper (PS) 

Abstract:

Computing the most specific concept (msc) is an inference task that allows to abstract from individuals defined in description logic (DL) knowledge bases. For DLs that allow for number restrictions or existential restrictions, however, the msc need not exist unless one allows for cyclic concepts interpreted with the greatest fixed-point semantics. Since such concepts cannot be handled by current DL-systems, we propose to approximate the msc. We show that for the DL ALE, which has concept conjunction, a restricted form of negation, existential restrictions, and value restrictions as constructors, approximations of the msc always exist and can effectively be computed.



R. Küsters and R. Molitor: Computing Least Common Subsumers in ALEN. 00-07, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Computing the least common subsumer (lcs) in description logics is an inference task first introduced for sublanguages of CLASSIC. Roughly speaking, the lcs of a set of concept descriptions is the most specific concept description that subsumes all of the input descriptions. As such, the lcs allows to extract the commonalities from given concept descriptions, a task essential for several applications like, e.g., inductive learning, information retrieval, or the bottom-up construction of KR-knowledge bases. Previous work on the lcs has concentrated on description logics that either allow for number restrictions or for existential restrictions. Many applications, however, require to combine these constructors. In this work, we present an lcs algorithm for the description logic ALEN, which allows for both constructors (as well as concept conjunction, primitive negation, and value restrictions). The proof of correctness of our lcs algorithm is based on an appropriate structural characterization of subsumption in ALEN also introduced in this paper.



C. Lutz: NExpTime-complete Description Logics with Concrete Domains. LTCS-00-01, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Description Logics (DLs) are well-suited for the representation of abstract conceptual knowledge. Concrete knowledge such as knowledge about numbers, time intervals, and spatial regions can be incorporated into DLs by using so-called concrete domains. The basic Description Logics providing concrete domains is ALC(D) which was introduced by Baader and Hanschke. Reasoning with ALC(D) concepts is known to be PSpace-complete if reasoning with the concrete domain D is in PSpace. In this paper, we consider the following three extensions of ALC(D) and examine the computational complexity of the resulting formalism: As lower bounds, we show that there exists a concrete domain P for which reasoning is in PTime such that reasoning with ALC(P) and any of the above extensions (separately) is NExpTime-hard. This is rather surprising since acyclic TBoxes and inverse roles are known to ``usually'' not increase the complexity of reasoning. As a corresponding upper bound, we show that reasoning with ALC(D) and all of the above extensions (together) is in NExpTime if reasoning with the concrete domain D is in NP. For proving the lower bound, we introduce a NExpTime-complete variant of the Post Correspondence Problem and reduce it to the three logics under consideration. The upper bound is proved by giving a tableau algorithm.



C. Lutz and U. Sattler: The Complexity of Reasoning with Boolean Modal Logics (Extended Version). LTCS-00-02, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Boolean Modal Logics extend multi-modal K by allowing the use of boolean operators to define complex relation terms. In this paper, we investigate the complexity of reasoning with various such logics. The main results are that (1) adding negation of modal parameters to K makes reasoning ExpTime-complete, which is shown by using an automata-theoretic approach, and that (2) adding atomic negation and conjunction to K even yields a NExpTime- complete logic, which is shown by a reduction of a variant of the domino problem. The last result is relativized by the fact that it depends on an infinite number of modal parameters to be available. If the number of modal parameters is bounded, full Boolean Modal Logic becomes ExpTime-complete. This is shown by a reduction to K enriched with the universal modality.



C. Hirsch and S. Tobies: A Tableaux Algorithm for the Clique Guarded Fragment, Preliminary Version. LTCS-00-03, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 



C. Lutz: Interval-based Temporal Reasoning with General TBoxes. LTCS-00-06, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Until now, interval-based temporal Description Logics (DLs) did—if at all—only admit TBoxes of a very restricted form, namely acyclic macro definitions. In this paper, we present a temporal DL that overcomes this deficieny and combines interval-based temporal reasoning with general TBoxes. We argue that this combination is very interesting for many application domains. An automata-based decision procedure is devised and a tight ExpTime-complexity bound is obtained. Since the presented logic can be viewed as being equipped with a concrete domain, our results can be seen from a different perspective: We show that there exist interesting concrete domains for which reasoning with general TBoxes in decidable.




1999

F. Baader, R. Küsters, and R. Molitor: Rewriting Concepts Using Terminologies – Revisited. 99-12, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. Please refer to the revised version LTCS-Report 00-04.
BibTeX entry  Paper (PS) 

Abstract:

The problem of rewriting a concept given a terminology can informally be stated as follows: given a terminology T (i.e., a set of concept definitions) and a concept description C that does not contain concept names defined in T, can this description be rewritten into a "related better" description E by using (some of) the names defined in T? In this paper, we first introduce a general framework for the rewriting problem in description logics, and then concentrate on one specific instance of the framework, namely the minimal rewriting problem (where "better" means shorter, and "related" means equivalent). We investigate the complexity of the decision problem induced by the minimal rewriting problem for the languages FL0, ALN, ALE, and ALC, and then introduce an algorithm for computing (minimal) rewritings for the languages ALE and ALN. Finally, we sketch other interesting instances of the framework. Our interest for the minimal rewriting problem stems from the fact that algorithms for non-standard inferences, such as computing least common subsumers and matchers, usually produce concept descriptions not containing defined names. Consequently, these descriptions are rather large and hard to read and comprehend. First experiments in a chemical process engineering application show that rewriting can reduce the size of concept descriptions obtained as least common subsumers by almost two orders of magnitude.



C. Lutz: The Complexity of Reasoning with Concrete Domains (Revised Version). LTCS-99-01, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.
BibTeX entry  Paper (PS) 

Abstract:

Description logics are knowledge representation and reasoning formalisms which represent conceptual knowledge on an abstract logical level. Concrete domains are a theoretically well-founded approach to the integration of description logic reasoning with reasoning about concrete objects such as numbers, time intervals or spatial regions. In this paper, the complexity of combined reasoning with description logics and concrete domains is investigated. We extend ALC(D), which is the basic description logic for reasoning with concrete domains, by the operators "feature agreement" and "feature disagreement". For the extended logic, called ALCF(D), an algorithm for deciding the ABox consistency problem is devised. The strategy employed by this algorithm is vital for the efficient implementation of reasoners for description logics incorporating concrete domains. Based on the algorithm, it is proved that the standard reasoning problems for both logics ALC(D) and (D) are PSpace-complete - provided that the satisfiability test of the concrete domain used is in PSpace.



M.-S.  Hacid and C. Rigotti: Representing and Reasoning on Conceptual Queries Over Image Databases. LTCS-99-02, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html
BibTeX entry  Paper (PS) 

Abstract:

The problem of content management of multimedia data types (e.g., image, video, graphics) is becoming increasingly important with the development of advanced multimedia applications. Traditional database management systems are inadequate for the handling of such data types. They require new techniques for query formulation, retrieval, evaluation, and navigation. In this paper we develop a knowledge-based framework for modeling and retrieving image data by content. To represent the various aspects of an image object's characteristics, we propose a model which consists of three layers: (1) Feature and Content Layer, intended to contain image visual features such as contours, shapes, etc.; (2) Object Layer, which provides the (conceptual) content dimension of images; and (3) Schema Layer, which contains the structured abstractions of images, i.e., a general schema about the classes of objects represented in the object layer. We propose two abstract languages on the basis of description logics: one for describing knowledge of the object and schema layers, and the other, more expressive, for making queries. Queries can refer to the form dimension (i.e., information of the Feature and Content Layer) or to the content dimension (i.e., information of the Object Layer). These languages employ a variable free notation, and they are well suited for the design, verification and complexity analysis of algorithms. As the amount of information contained in the previous layers may be huge and operations performed at the Feature and Content Layer are time-consuming, resorting to the use of materialized views to process and optimize queries may be extremely useful. For that, we propose a formal framework for testing containment of a query in a view expressed in our query language. The algorithm we propose is sound and complete and relatively efficient.



C. Decleir, M.-S. Hacid, and J. Kouloumdjian: A Database Approach for Modeling and Querying Video Data. LTCS-99-03, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html
BibTeX entry  Paper (PS) 

Abstract:

Indexing video data is essential for providing content based access. In this paper, we consider how database technology can offer an integrated framework for modeling and querying video data. As many concerns in video (e.g., modeling and querying) are also found in databases, databases provide an interesting angle to attack many of the problems. From a video applications perspective, database systems provide a nice basis for future video systems. More generally, database research will provide solutions to many video issues even if these are partial or fragmented. From a database perspective, video applications provide beautiful challenges. Next generation database systems will need to provide support for multimedia data (e.g., image, video, audio). These data types require new techniques for their management (i.e., storing, modeling, querying, etc.). Hence new solutions are significant. This paper develops a data model and a rule-based query language for video content based indexing and retrieval. The data model is designed around the object and constraint paradigms. A video sequence is split into a set of fragments. Each fragment can be analyzed to extract the information (symbolic descriptions) of interest that can be put into a database. This database can then be searched to find information of interest. Two types of information are considered: (1) the entities (objects) of interest in the domain of a video sequence, (2) video frames which contain these entities. To represent these information, our data model allows facts as well as objects and constraints. We present a declarative, rule-based, constraint query language that can be used to infer relationships about information represented in the model. The language has a clear declarative and operational semantics.



C. Lutz: On the Complexity of Terminological Reasoning. LTCS-99-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. This report is superceded by the LTCS-00-01 technical report and my LPAR'99 paper.
BibTeX entry 

Abstract:

TBoxes are an important component of knowledge representation systems based on description logics DLs since they allow for a natural representation of terminological knowledge. Largely due to a classical result given by Nebel, complexity analyses for DLs have, until now, mostly focused on reasoning without (acyclic) TBoxes. In this paper, we concentrate on DLs, for which reasoning without TBoxes is PSpace-complete, and show that there exist logics for which the complexity of reasoning remains in PSpace if acyclic TBoxes are added and also logics for which the complexity increases. An example for a logic of the former type is ALC while examples for logics of the latter kind include ALC(D) and ALCF. This demonstrates that it is necessary to take TBoxes into account for complexity analyses. Furthermore, we show that reasoning with the description logic ALCRP(D) is NExpTime-complete regardless of whether TBoxes are admitted or not.



S. Tobies: A NEXPTIME-complete Description Logic Strictly Contained in C2. LTCS-99-05, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. An abriged version appeared at CSL-99.
BibTeX entry  Paper (PS) 

Abstract:

We examine the complexity and expressivity of the combination of the Description Logic ALCQI with a terminological formalism based on cardinality restrictions on concepts. This combination can naturally be embedded into C2, the two variable fragment of predicate logic with counting quantifiers. We prove that ALCQI has the same complexity as C2 but does not reach its expressive power.



F. Baader and R. Molitor: Rewriting Concepts using Terminologies. LTCS-99-06, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html
BibTeX entry  Paper (PS) 

Abstract:

In this work we consider the inference problem of computing (minimal) rewritings of concept descriptions using defined concepts from a terminology. We introduce a general framework for this problem. For the small description logic FLo, which provides us with conjunction and value restrictions, we show that the decision problem induced by the minimal rewriting problem is NP-complete.



F. Baader and R. Küsters: Matching in Description Logics with Existential Restrictions. LTCS-99-07, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html
BibTeX entry  Paper (PS) 

Abstract:

Matching of concepts with variables (concept patterns) is a relatively new operation that has been introduced in the context of description logics, originally to help filter out unimportant aspects of large concepts appearing in industrial-strength knowledge bases. Previous work has concentrated on (sub-)languages of CLASSIC, which in particular do not allow for existential restrictions. In this work, we present sound and complete decision algorithms for the solvability of matching problems and for computing sets of matchers for matching problems in description logics with existential restrictions.



I. Horrocks, U. Sattler, and S. Tobies: A Description Logic with Transitive and Converse Roles, Role Hierarchies and Qualifying Number Restrictions. LTCS-99-08, LuFG Theoretical Computer Science, RWTH Aachen, 1999. Revised version. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html
BibTeX entry  Paper (PS) 

Abstract:

Description Logics (DLs) are a family of knowledge representation formalisms mainly characterised by constructors to build complex concepts and roles from atomic ones. Expressive role constructors are important in many applications, but can be computationally problematical. We successively present algorithms that decides satisfiability of the DL extended with transitive and inverse roles, role hierarchies, and qualifying number restrictions. Early experiments indicate that this algorithm is well-suited for implementation.



S. Tobies: A PSpace-algorithm for ALCQI-satisfiability. LTCS-99-09, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.
BibTeX entry  Paper (PS) 

Abstract:

The description logic ALCQI extends the ``standard'' description logic ALC by qualifying number restrictions and converse roles. We show that concept satisfiability for this DL is still decidable in polynomial space. The presented algorithm combines techniques from A PSPACE Algorithm for Graded Modal Logic to deal with qualifying number restrictions and from Practical Reasoning for Description Logics with Functional Restrictions, Inverse and Transitive Roles, and Role Hierarchies to deal with converse roles.



S. Tobies: PSpace Reasoning for DLs with Qualifying Number Restrictions. LTCS-99-11, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.
BibTeX entry  Paper (PS) 

Abstract:

The description logic ALCQI extends the ``standard'' description logic ALC by qualifying number restrictions and converse roles. We show that concept satisfiability for this DL is still decidable in polynomial space. The presented algorithm combines techniques from A PSPACE Algorithm for Graded Modal Logic to deal with qualifying number restrictions and from Practical Reasoning for Description Logics with Functional Restrictions, Inverse and Transitive Roles, and Role Hierarchies to deal with converse roles. Additionally, we extend the result to ALCQIR which extends ALCQI by role intersections.



F. Baader and R. Küsters: Matching Concept Descriptions with Existential Restrictions Revisited. LTCS-99-13, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Matching of concepts against patterns is a new inference task in Description Logics, which was originally motivated by applications of the Classic system. Consequently, the work on this problem was until now mostly concerned with sublanguages of the Classic language, which does not allow for existential restrictions. Motivated by an application in chemical process engineering, which requires a description language with existential restrictions, this paper investigates the matching problem in Description Logics with existential restrictions. It turns out that existential restrictions make matching more complex in two respects. First, whereas matching in sublanguages of Classic is polynomial, deciding the existence of matchers is an NP-complete problem in the presence of existential restrictions. Second, whereas in sublanguages of Classic solvable matching problems have a unique least matcher, this is not the case for languages with existential restrictions. Thus, it is not a priori clear which of the (possibly infinitely many) matchers should be returned by a matching algorithm. After determining the complexity of the decision problem, the present paper first investigates the question of what are "interesting" sets of matchers, and then describes algorithms for computing these sets for the languages EL (which allows for conjunction and existential restrictions) and ALE.



I. Horrocks and S. Tobies: Optimisation of Terminological Reasoning. LTCS-99-14, LuFG Theoretical Computer Science, RWTH Aachen, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html
BibTeX entry  Paper (PS) 

Abstract:

When reasoning in description, modal or temporal logics it is often useful to consider axioms representing universal truths in the domain of discourse. Reasoning with respect to an arbitrary set of axioms is hard, even for relatively inexpressive logics, and it is essential to deal with such axioms in an efficient manner if implemented systems are to be effective in real applications. This is particularly relevant to Description Logics, where subsumption reasoning with respect to a terminology is a fundamental problem. Two optimisation techniques that have proved to be particularly effective in dealing with terminologies are lazy unfolding and absorption. In this paper we seek to improve our theoretical understanding of these important techniques. We define a formal framework that allows the techniques to be precisely described, establish conditions under which they can be safely applied, and prove that, provided these conditions are respected, subsumption testing algorithms will still function correctly. These results are used to show that the procedures used in the FaCT system are correct and, moreover, to show how efficiency can be significantly improved, while still retaining the guarantee of correctness, by relaxing the safety conditions for absorption.



I. Horrocks, U. Sattler, S. Tessaris, and S. Tobies: Query Containment Using a DLR ABox. LTCS-99-15, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 

Abstract:

Query containment under constraints is the problem of determining whether the result of one query is contained in the result of another query for every database satisfying a given set of constraints. This problem is of particular importance in information integration and warehousing where, in addition to the constraints derived from the source schemas and the global schema, inter-schema constraints can be used to specify relationships between objects in different schemas. A theoretical framework for tackling this problem using the DLR logic has been established, and in this paper we show how the framework can be extended to a practical decision procedure. The proposed technique is to extend DLR with an Abox (a set of assertions about named individuals and tuples), and to transform query subsumption problems into DLR Abox satisfiability problems. We then show how such problems can be decided, via a reification transformation, using a highly optimised reasoner for the SHI description logic.




1998

C.B. Tresp and R. Molitor: A Description Logic for Vague Knowledge. LTCS-98-01, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html
BibTeX entry  Paper (PS) 

Abstract:

This work introduces the concept language ALC(FM) which is an extension of ALC to many-valued logics. ALC(FM) allows to express vague concepts, e.g. `more or less enlarged' or `very small'. To realize this extension to many-valued logics, the classical notions of satisfiability and subsumption had to be modified appropriately. For example, ALC(FM)-concepts are no longer either satisfiable or unsatisfiable, but they are satisfiable to a certain degree. The main contribution of this paper is a sound and complete method for computing the degree of subsumption between two ALC(FM)-concepts.



F. Baader and U. Sattler: Description Logics with Aggregates and Concrete Domains, Part II (extended). LTCS-98-02, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.
BibTeX entry  Paper (PS) 



R. Molitor: Structural Subsumption for ALN. LTCS-98-03, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998.
BibTeX entry  Paper (PS) 



F. Baader, R. Küsters, and R. Molitor: Structural Subsumption Considered from an Automata Theoretic Point of View. LTCS-98-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS)  Paper (PS) 

Abstract:

This paper compares two approaches for deriving subsumption algorithms for the description logic ALN: structural subsumption and an automata-theoretic characterization of subsumption. It turns out that structural subsumption algorithms can be seen as special implementations of the automata-theoretic characterization.



I. Horrocks and U. Sattler: A Description Logic with Transitive and Converse Roles and Role Hierarchies. LTCS-98-05, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.
BibTeX entry  Paper (PS) 



F. Baader and R. Küsters: Computing the least common subsumer and the most specific concept in the presence of cyclic ALN-concept descriptions. LTCS-98-06, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.
BibTeX entry  Paper (PS) 

Abstract:

Computing least common subsumers (lcs) and most specific concepts (msc) are inference tasks that can be used to support the ``bottom up'' construction of knowledge bases for KR systems based on description logic. For the description logic ALN, the msc need not always exist if one restricts the attention to acyclic concept descriptions. In this paper, we extend the notions lcs and msc to cyclic descriptions, and show how they can be computed. Our approach is based on the automata-theoretic characterizations of fixed-point semantics for cyclic terminologies developed in previous papers.



F. Baader and P. Narendran: Unification of Concept Terms in Description Logics: Revised Version. LTCS-98-07, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.
BibTeX entry  Paper (PS) 

Abstract:

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to substitute certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language. This is a revised version of LTCS-Report 97-02: it provides a stronger complexity result in Section 6.



I. Horrocks, U. Sattler, and S. Tobies: A PSpace-algorithm for deciding ALCNIR+-satisfiability. LTCS-98-08, LuFG Theoretical Computer Science, RWTH Aachen, 1998.
BibTeX entry  Paper (PS) 

Abstract:

ALCIR+—ALC augmented with transitive and inverse roles—is an expressive Description Logic which is especially well-suited for the representation of complex, aggregated objects. Despite its expressiveness, it has been conjectured that concept satisfiability for this logic could be decided in a comparatively efficient way. In this paper we prove the correctness of this conjecture by presenting a PSpace algorithm for deciding satisfiability and subsumption of ALCIR+-concepts. The space-efficiency of this tableau-based algorithm is due to a sophisticated guidance of the search for a solution. This algorithm will be the basis for an efficient implementation.



F. Baader, R. Küsters, and R. Molitor: Computing Least Common Subsumers in Description Logics with Existential Restrictions. LTCS-98-09, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998. See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.
BibTeX entry  Paper (PS) 

Abstract:

Computing least common subsumers (lcs) is an inference task that can be used to support the "bottom-up" construction of knowledge bases for KR systems based on description logics. Previous work on how to compute the lcs has concentrated on description logics that allow for universal value restrictions, but not for existential restrictions. The main new contribution of this paper is the treatment of description logics with existential restrictions. More precisely, we show that, for the description logic ALE (which allows for conjunction, universal value restrictions, existential restrictions, negation of atomic concepts, as well as the top and the bottom concept), the lcs always exists and can effectively be computed. Our approach for computing the lcs is based on an appropriate representation of concept descriptions by certain trees, and a characterization of subsumption by homomorphisms between these trees. The lcs operation then corresponds to the product operation on trees.



F. Baader, R. Molitor, and S. Tobies: The Guarded Fragment of Conceptual Graphs. LTCS-98-10, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998. See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html
BibTeX entry  Paper (PS) 

Abstract:

Conceptual graphs (CGs) are an expressive and intuitive formalism, which plays an important role in the area of knowledge representation. Due to their expressiveness, most interesting problems for CGs are inherently undecidable. We identify the syntactically defined guarded fragment of CGs, for which both subsumption and validity is decidable in deterministic exponential time.



F. Baader, R. Molitor, and S. Tobies: On the Relation between Descripion Logics and Conceptual Graphs. LTCS-98-11, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
BibTeX entry  Paper (PS) 




1997

F. Baader and U. Sattler: Description Logics with Aggregates and Concrete Domains. LTCS-97-01, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1997. An abridged version has appeared in the Proceedings of the International Workshop on Description Logics 97.
BibTeX entry  Paper (PS) 

Abstract:

We show that extending description logics by simple aggregation functions as available in database systems may lead to undecidability of inference problems such as satisfiability and subsumption.



F. Baader and P. Narendran: Unification of Concept Terms in Description Logics. LTCS-97-02, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1997.
BibTeX entry  Paper (PS) 

Abstract:

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to substitute certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language.



F. Baader: On the Complexity of Boolean Unification. LTCS-97-03, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1997.
BibTeX entry  Paper (PS) 

Abstract:

Unification modulo the theory of Boolean algebras has been investigated by several autors. Nevertheless, the exact complexity of the decision problem for unification with constants and general unification was not known. In this research note, we show that the decision problem is p2-complete for unification with constants and PSPACE-complete for general unification. In contrast, the decision problem for elementary unification (where the terms to be unified contain only symbols of the signature of Boolean algebras) is ``only'' NP-complete.



R. Küsters: Characterizing the semantics of terminological cycles in ALN using finite automata. LTCS-97-04, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1997.
BibTeX entry  Paper (PS) 

Abstract:

The representation of terminological knowledge may naturally lead to terminological cycles. In addition to descriptive semantics, the meaning of cyclic terminologies can also be captured by fixed-point semantics, namely, greatest and least fixed-point semantics. To gain a more profound understanding of these semantics and to obtain inference algorithms as well as complexity results for inconsistency, subsumption, and related inference tasks, this paper provides automata theoretic characterizations of these semantics. More precisely, the already existing results for FL0 are extended to the language ALN, which additionally allows for primitive negation and number-restrictions. Unlike FL0, the language ALN can express inconsistent concepts, which makes non-trivial extensions of the characterizations and algorithms necessary. Nevertheless, the complexity of reasoning does not increase when going from FL0 to ALN. This distinguishes ALN from the very expressive languages with fixed-point operators proposed in the literature. It will be shown, however, that cyclic ALN-terminologies are expressive enough to capture schemata in certain semantic data models.



M. S. Hacid, P. Marcel, and C. Rigotti: A rule based data manipulation language for OLAP systems. LTCS-97-05, LuFg Theoretical Computer Science, RWTH Aachen, 1997. A short version has appeared in the Proceedings of the 5th International Conference on Deductive and Object-Oriented Databases (DOOD'97), Montreux, Switzerland
BibTeX entry  Paper (PS) 

Abstract:

This paper proposes an extension of Datalog devoted to data manipulations in On-Line Analytical Processing (OLAP) systems. This language provides a declarative and concise way to specify the basic standard restructuring and summarizing operations on multidimensional cubes used in these systems. We define its model-theoretic semantics and an equivalent fixpoint semantics that leads to a naive evaluation procedure. We also illustrate its applicability to specify usefull more complex data manipulations arising in OLAP systems.




1996

F. Baader and C. Tinelli: A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. LTCS-96-01, LuFg Theoretical Computer Science, RWTH Aachen, 1996. An abridged version has appeared in Proc. CADE'97, Springer LNAI 1249.
BibTeX entry  Paper (PS) 

Abstract:

The Nelson-Oppen combination method can be used to combine decision procedures for the validity of quantifier-free formulae in first-order theories with disjoint signatures, provided that the theories to be combined are stably infinite. We show that, even though equational theories need not satisfy this property, Nelson and Oppen's method can be applied, after some minor modifications, to combine decision procedures for the validity of quantifier-free formulae in equational theories. Unfortunately, and contrary to a common belief, the method cannot be used to combine decision procedures for the word problem. We present a method that solves this kind of combination problem. Our method is based on transformation rules and also applies to equational theories that share a finite number of constant symbols.



F. Baader and U. Sattler: Number Restrictions on Complex Roles in Description Logics. LTCS-96-02, LuFg Theoretical Computer Science, RWTH Aachen, 1996. An abridged version has appeared in the Proceedings of the Fifth International Conference on Knowledge Representation and Reasoning, 1996, Cambridge, Massachusetts.
BibTeX entry  Paper (PS) 



F. Baader and U. Sattler: Description Logics with Symbolic Number Restrictions. LTCS-96-03, LuFg Theoretical Computer Science, RWTH Aachen, 1996. An abridged version has appeared in the Proceedings of the 12th European Conference on Artificial Intelligence, 1996, Budapest, Hungary.
BibTeX entry  Paper (PS) 



S. Kepser and J. Richts: Optimisation Techniques for Combining Constraint Solvers. LTCS-96-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1996.
BibTeX entry  Paper (PS) 

Abstract:

In recent years, techniques that had been developed for the combination of unification algorithms for equational theories were extended to combining constraint solvers. These techniques inherited an old deficit that was already present in the combination of equational theories which makes them rather unsuitable for practical use: The underlying combination algorithms are highly non-deterministic. This paper is concerned with the practical problem of how to optimise the combination method of Baader and Schulz. We present two optimisation methods, called the iterative and the deductive method. The iterative method reorders and localises the non-deterministic decisions. The deductive method uses specific algorithms for the components to reach certain decisions deterministically. Run time tests of our implementation indicate that the optimised combination method yields combined decision procedures that are efficient enough to be used in practice.



F. Baader: Combination of Compatible Reduction Orderings that are Total on Ground Terms. LTCS-96-05, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1996.
BibTeX entry  Paper (PS) 

Abstract:

Reduction orderings that are compatible with an equational theory E and total on (the E-equivalence classes of) ground terms play an important role in automated deduction. We present a general approach for combining such orderings. To be more precise, we show how E1-compatible reduction orderings total on 1-ground terms and E2-compatible reduction orderings total on 2-ground terms can be used to construct an (E1 E2)-compatible reduction ordering total on (1 2)-ground terms, provided that the signatures are disjoint and some other (rather weak) restrictions are satisfied. This work was motivated by the observation that it is often easier to construct such orderings for ``small'' signatures and theories separately, rather than directly for their union.




Back to the hompage of the Chair of Automata Theory.
Generated Mon Jan 15 13:51:23 2018.