# Technische Berichte

2018 2017 2016 2015 2014 2013 2012 2011

2010 2009 2008 2007 2006 2005 2004 2003 2002 2001

2000 1999 1998 1997 1996 1995 1994 1993 1992 1991

1990 1989 1985

## 2018

Franz Baader, Francesco Kriegel, Adrian Nuradiansyah, and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Repairing Description Logic Ontologies by Weakening Axioms**. LTCS-Report 18-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2018.Abstract BibTeX Entry PDF File

The classical approach for repairing a Description Logic ontology \(\mathfrak{O}\) in the sense of removing an unwanted consequence \(\alpha\) is to delete a minimal number of axioms from \(\mathfrak{O}\) such that the resulting ontology \(\mathfrak{O}'\) does not have the consequence \(\alpha\). However, the complete deletion of axioms may be too rough, in the sense that it may also remove consequences that are actually wanted. To alleviate this problem, we propose a more gentle way of repair in which axioms are not necessarily deleted, but only weakened. On the one hand, we investigate general properties of this gentle repair method. On the other hand, we propose and analyze concrete approaches for weakening axioms expressed in the Description Logic \(\mathcal{E\!L}\).

@techreport{ BaKrNuPe-LTCS-18-01, address = {Dresden, Germany}, author = {Franz {Baader} and Francesco {Kriegel} and Adrian {Nuradiansyah} and Rafael {Pe\~{n}aloza}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {18-01}, title = {Repairing Description Logic Ontologies by Weakening Axioms}, type = {LTCS-Report}, year = {2018}, }

Francesco Kriegel:

Abstract BibTeX Entry PDF File

**Terminological Knowledge Acquisition in Probabilistic Description Logic**. LTCS-Report 18-03, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2018.Abstract BibTeX Entry PDF File

For a probabilistic extension of the description logic \(\mathcal{E\!L}^{\bot}\), we consider the task of automatic acquisition of terminological knowledge from a given probabilistic interpretation. Basically, such a probabilistic interpretation is a family of directed graphs the vertices and edges of which are labeled, and where a discrete probability measure on this graph family is present. The goal is to derive so-called concept inclusions which are expressible in the considered probabilistic description logic and which hold true in the given probabilistic interpretation. A procedure for an appropriate axiomatization of such graph families is proposed and its soundness and completeness is justified.

@techreport{ Kr-LTCS-18-03, address = {Dresden, Germany}, author = {Francesco {Kriegel}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {18-03}, title = {Terminological Knowledge Acquisition in Probabilistic Description Logic}, type = {LTCS-Report}, year = {2018}, }

Franz Baader, Oliver Fernández Gil, and Maximilian Pensel:

Abstract BibTeX Entry PDF File

**Standard and Non-Standard Inferences in the Description Logic**\(\mathcal{FL}_0\)**Using Tree Automata**. LTCS-Report 18-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2018.Abstract BibTeX Entry PDF File

Although being quite inexpressive, the description logic (DL) FL0, which provides only conjunction, value restriction and the top concept as concept constructors, has an intractable subsumption problem in the presence of terminologies (TBoxes): subsumption reasoning w.r.t. acyclic FL0 TBoxes is coNP-complete, and becomes even ExpTime-complete in case general TBoxes are used. In the present paper, we use automata working on infinite trees to solve both standard and non-standard inferences in FL0 w.r.t. general TBoxes. First, we give an alternative proof of the ExpTime upper bound for subsumption in FL0 w.r.t. general TBoxes based on the use of looping tree automata. Second, we employ parity tree automata to tackle non-standard inference problems such as computing the least common subsumer and the difference of FL0 concepts w.r.t. general TBoxes.

@techreport{ BaFePe-LTCS-18-04, address = {Dresden, Germany}, author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil} and Maximilian {Pensel}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {18-04}, title = {Standard and Non-Standard Inferences in the Description Logic $\mathcal{FL}_0$ Using Tree Automata}, type = {LTCS-Report}, year = {2018}, }

Patrick Koopmann and Benjamin Zarrieß:

Abstract BibTeX Entry PDF File

**On the Complexity of Verifying Timed Golog Programs over Description Logic Actions (Extended Version)**. LTCS-Report 18-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2018.Abstract BibTeX Entry PDF File

Golog programs allow to model complex behaviour of agents by combining primitive actions defined in a Situation Calculus theory using imperative and non-deterministic programming language constructs. In general, verifying temporal properties of Golog programs is undecidable. One way to establish decidability is to restrict the logic used by the program to a Description Logic (DL), for which recently some complexity upper bounds for verification problem have been established. However, so far it was open whether these results are tight, and lightweight DLs such as EL have not been studied at all. Furthermore, these results only apply to a setting where actions do not consume time, and the properties to be verified only refer to the timeline in a qualitative way. In a lot of applications, this is an unrealistic assumption. In this work, we study the verification problem for timed Golog programs, in which actions can be assigned differing durations, and temporal properties are specified in a metric branching time logic. This allows to annotate temporal properties with time intervals over which they are evaluated, to specify for example that some property should hold for at least n time units, or should become specified within some specified time window. We establish tight complexity bounds of the verification problem for both expressive and lightweight DLs. Our lower bounds already apply to a very limited fragment of the verification problem, and close open complexity bounds for the non-metrical cases studied before.

@techreport{ KoZa-LTCS-18-06, address = {Dresden, Germany}, author = {Patrick {Koopmann} and Benjamin {Zarrie{\ss}}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}}, number = {18-06}, title = {On the Complexity of Verifying Timed {Golog} Programs over Description Logic Actions (Extended Version)}, type = {LTCS-Report}, year = {2018}, }

## 2017

Maximilian Pensel and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File

**Making Quantification Relevant again—the case of Defeasible**\(\mathcal{EL}_{bot}\). LTCS-Report 17-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017.Abstract BibTeX Entry PDF File

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 EL_{bot}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.

@techreport{ PeTu-LTCS-17-01, address = {Dresden, Germany}, author = {Maximilian {Pensel} and Anni-Yasmin {Turhan}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {17-01}, title = {Making Quantification Relevant again---the case of Defeasible $\mathcal{EL}_{bot}$}, type = {LTCS-Report}, year = {2017}, }

Franz Baader:

Abstract BibTeX Entry PDF File

**Concept Descriptions with Set Constraints and Cardinality Constraints**. LTCS-Report 17-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017.Abstract BibTeX Entry PDF File

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.

@techreport{ Baad-LTCS-17-02, address = {Dresden, Germany}, author = {Franz {Baader}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {17-02}, title = {Concept Descriptions with Set Constraints and Cardinality Constraints}, type = {LTCS-Report}, year = {2017}, }

Franz Baader, Stefan Borgwardt, Patrick Koopmann, Ana Ozaki, and Veronika Thost:

Abstract BibTeX Entry PDF File

**Metric Temporal Description Logics with Interval-Rigid Names (Extended Version)**. LTCS-Report 17-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBoKoOzTh-LTCS-17-03, address = {Dresden, Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Patrick {Koopmann} and Ana {Ozaki} and Veronika {Thost}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}}, number = {17-03}, title = {Metric Temporal Description Logics with Interval-Rigid Names (Extended Version)}, type = {LTCS-Report}, year = {2017}, }

Franz Baader, Stefan Borgwardt, and Marcel Lippmann:

Abstract BibTeX Entry PDF File

**Query Rewriting for DL-Lite with**\(n\)**-ary Concrete Domains (Extended Version)**. LTCS-Report 17-04, Chair for Automata Theory, Technische Universität Dresden, Germany, 2017.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBL-LTCS-17-04, address = {Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Marcel {Lippmann}}, institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden}, note = {see \url{https://lat.inf.tu-dresden.de/research/reports.html}}, number = {17-04}, title = {Query Rewriting for \textit{{DL-Lite}} with {$n$}-ary Concrete Domains (Extended Version)}, type = {LTCS-Report}, year = {2017}, }

Franz Baader, Patrick Koopmann, and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File

**Using Ontologies to Query Probabilistic Numerical Data (Extended Version)**. LTCS-Report 17-05, Chair for Automata Theory, Technische Universität Dresden, Germany, 2017.Abstract BibTeX Entry PDF File

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.

@techreport{ BaKoTu-LTCS-17-05, address = {Germany}, author = {Franz {Baader} and Patrick {Koopmann} and Anni-Yasmin {Turhan}}, institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden}, note = {See \url{https://lat.inf.tu-dresden.de/research/reports.html}}, number = {17-05}, title = {Using Ontologies to Query Probabilistic Numerical Data (Extended Version)}, type = {LTCS-Report}, year = {2017}, }

Camille Bourgaux and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File

**Temporal Query Answering in DL-Lite over Inconsistent Data**. LTCS-Report 17-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017.Abstract BibTeX Entry PDF File

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-Lite_{R}temporal knowledge bases, and furthermore complete the picture for the consistent case.

@techreport{ BoTu-LTCS-17-06, address = {Dresden, Germany}, author = {Camille {Bourgaux} and Anni-Yasmin {Turhan}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {see \url{http://lat.inf.tu-dresden.de/research/reports.html}}, number = {17-06}, title = {Temporal Query Answering in {DL-Lite} over Inconsistent Data}, type = {LTCS-Report}, year = {2017}, }

Franz Baader, Stefan Borgwardt, and Barbara Morawska:

Abstract BibTeX Entry PDF File

**Constructing SNOMED CT Concepts via Disunification**. LTCS-Report 17-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2017.Abstract BibTeX Entry PDF File

We investigate the use of disunification in \(\mathcal{EL}\) for ontology generation. In particular, we study how disunification can construct new SNOMED CT concepts when given information about the position of the new concept in the concept hierarchy. To evaluate our approach, we randomly select concept names from SNOMED CT, remove their definitions, and formulate disunification problems that recover these definitions from information about the parents and siblings of the removed concept names. Our evaluation shows that this approach works well for some subhierarchies of SNOMED CT. Overall, one can reconstruct about 6% of all SNOMED CT concept names in this way.

@techreport{ BaBM-LTCS-17-07, address = {Dresden, Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See https://tu-dresden.de/ing/informatik/thi/lat/forschung/technische-berichte.}, number = {17-07}, title = {Constructing {SNOMED CT} Concepts via Disunification}, type = {LTCS-Report}, year = {2017}, }

## 2016

Claudia Carapelle and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File

**Decidability of**\(\mathcal{ALC}^P\!(\mathcal{D})\)**for concrete domains with the EHD-property**. LTCS-Report 16-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016.Abstract BibTeX Entry PDF File

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.

@techreport{ CaTu-LTCS-16-01, address = {Dresden, Germany}, author = {Claudia {Carapelle} and Anni-Yasmin {Turhan}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, number = {16-01}, title = {Decidability of $\mathcal{ALC}^P\!(\mathcal{D})$ for concrete domains with the EHD-property}, type = {LTCS-Report}, year = {2016}, }

Franz Baader and Oliver Fernández Gil:

Abstract BibTeX Entry PDF File

**Extending Description Logic**\(t\mathcal{E\!L}(\mathit{deg})\)**with Acyclic TBoxes**. LTCS-Report 16-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016.Abstract BibTeX Entry PDF File

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.

@techreport{ BaFe-LTCS-16-02, address = {Dresden, Germany}, author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {16-02}, title = {Extending Description Logic {$t\mathcal{E\!L}(\mathit{deg})$} with Acyclic TBoxes}, type = {LTCS-Report}, year = {2016}, }

Franz Baader, Pavlos Marantidis, and Alexander Okhotin:

Abstract BibTeX Entry PDF File

**Approximately Solving Set Equations**. LTCS-Report 16-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016.Abstract BibTeX Entry PDF File

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 \(\ell\) violations for a given threshold value \(\ell\).

@techreport{ BaMaOk-LTCS-16-03, address = {Dresden, Germany}, author = {Franz {Baader} and Pavlos {Marantidis} and Alexander {Okhotin}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {16-03}, title = {Approximately Solving Set Equations}, type = {LTCS-Report}, year = {2016}, }

Franz Baader, Pavlos Marantidis, and Alexander Okhotin:

Abstract BibTeX Entry PDF File

**Approximate Unification in the Description Logic**\(\mathcal{FL}_0\). LTCS-Report 16-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016.Abstract BibTeX Entry PDF File

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 \(\mathcal{FL}_0\), 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 \(\mathcal{FL}_0\) can be reduced to approximately solving language equations, and devise algorithms for solving the latter problem for two particular distance measures.

@techreport{ BaMaOk-LTCS-16-04, address = {Dresden, Germany}, author = {Franz {Baader} and Pavlos {Marantidis} and Alexander {Okhotin}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {16-04}, title = {Approximate Unification in the Description Logic {$\mathcal{FL}_0$}}, type = {LTCS-Report}, year = {2016}, }

Franz Baader and Oliver Fernández Gil:

Abstract BibTeX Entry PDF File

**Decidability and Complexity of Threshold Description Logics Induced by Concept Similarity Measures**. LTCS-Report 16-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016.Abstract BibTeX Entry PDF File

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).

@techreport{ BaFe-LTCS-16-07, address = {Dresden, Germany}, author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {16-07}, title = {Decidability and Complexity of Threshold Description Logics Induced by Concept Similarity Measures}, type = {LTCS-Report}, year = {2016}, }

Franz Baader, Oliver Fernández Gil, and Pavlos Marantidis:

Abstract BibTeX Entry PDF File

**Approximation in Description Logics: How Weighted Tree Automata Can Help to Define the Required Concept Comparison Measures in**\(\mathcal{FL}_0\). LTCS-Report 16-08, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2016.Abstract BibTeX Entry PDF File

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.

@techreport{ BaFM-LTCS-16-08, address = {Dresden, Germany}, author = {Franz {Baader} and Oliver {Fern{\'a}ndez Gil} and Pavlos {Marantidis}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {16-08}, title = {Approximation in Description Logics: How Weighted Tree Automata Can Help to Define the Required Concept Comparison Measures in $\mathcal{FL}_0$}, type = {LTCS-Report}, year = {2016}, }

## 2015

Francesco Kriegel:

Abstract BibTeX Entry

**NextClosures – Parallel Exploration of Constrained Closure Operators**. LTCS-Report 15-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry

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, and partially known closure operators can be explored.

@techreport{ Kr-LTCS-15-01, address = {Dresden, Germany}, author = {Francesco {Kriegel}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {15-01}, title = {NextClosures -- Parallel Exploration of Constrained Closure Operators}, type = {LTCS-Report}, year = {2015}, }

Francesco Kriegel:

Abstract BibTeX Entry

**Model-Based Most Specific Concept Descriptions and Least Common Subsumers in**\(\mathcal{ALEQ}^{\geq}\mathcal{N}^{\leq}(\mathsf{Self})\). LTCS-Report 15-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry

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

@techreport{ Kr-LTCS-15-02, address = {Dresden, Germany}, author = {Francesco {Kriegel}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {15-02}, title = {Model-Based Most Specific Concept Descriptions and Least Common Subsumers in $\mathcal{ALEQ}^{\geq}\mathcal{N}^{\leq}(\mathsf{Self})$}, type = {LTCS-Report}, year = {2015}, }

Franz Baader, Stefan Borgwardt, and Barbara Morawska:

Abstract BibTeX Entry PDF File

**Dismatching and Local Disunification in**\(\mathcal{EL}\). LTCS-Report 15-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBM-LTCS-15-03, address = {Dresden, Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {15-03}, title = {Dismatching and Local Disunification in {$\mathcal{EL}$}}, type = {LTCS-Report}, year = {2015}, }

Stephan Böhme and Marcel Lippmann:

Abstract BibTeX Entry PDF File

**Description Logics of Context with Rigid Roles Revisited**. LTCS-Report 15-04, Chair of Automata Theory, TU Dresden, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BoLi-LTCS-15-04, author = {Stephan {B{\"o}hme} and Marcel {Lippmann}}, institution = {Chair of Automata Theory, TU Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {15-04}, title = {Description Logics of Context with Rigid Roles Revisited}, type = {LTCS-Report}, year = {2015}, }

Stefan Borgwardt, Marco Cerami, and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Subsumption in Finitely Valued Fuzzy**\(\mathcal{EL}\). LTCS-Report 15-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BoCP-LTCS-15-06, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Marco {Cerami} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {15-06}, title = {Subsumption in Finitely Valued Fuzzy {$\mathcal{EL}$}}, type = {LTCS-Report}, year = {2015}, }

Stefan Borgwardt and Veronika Thost:

Abstract BibTeX Entry PDF File

**LTL over**\(\mathcal{EL}\)**Axioms**. LTCS-Report 15-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BoTh-LTCS-15-07, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Veronika {Thost}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {15-07}, title = {{LTL} over {$\mathcal{EL}$} Axioms}, type = {LTCS-Report}, year = {2015}, }

Stefan Borgwardt and Veronika Thost:

Abstract BibTeX Entry PDF File

**Temporal Query Answering in**\(\mathcal{EL}\). LTCS-Report 15-08, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BoTh-LTCS-15-08, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Veronika {Thost}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {15-08}, title = {Temporal Query Answering in {$\mathcal{EL}$}}, type = {LTCS-Report}, year = {2015}, }

Franz Baader, Gerhard Brewka, and Oliver Fernández Gil:

Abstract BibTeX Entry PDF File

**Adding Threshold Concepts to the Description Logic**\(\mathcal{E\!L}\). LTCS-Report 15-09, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBrF-LTCS-15-09, address = {Dresden, Germany}, author = {Franz {Baader} and Gerhard {Brewka} and Oliver Fern{\'a}ndez {Gil}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {15-09}, title = {Adding Threshold Concepts to the Description Logic $\mathcal{E\!L}$}, type = {LTCS-Report}, year = {2015}, }

Benjamin Zarrieß and Jens Claßen:

Abstract BibTeX Entry PDF File

**Verification of Knowledge-Based Programs over Description Logic Actions**. LTCS-Report 15-10, Chair of Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ ZaCl-LTCS-15-10, address = {Dresden, Germany}, author = {Benjamin {Zarrie{\ss}} and Jens {Cla{\ss}en}}, institution = {Chair of Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html}, number = {15-10}, title = {Verification of Knowledge-Based Programs over Description Logic Actions}, type = {LTCS-Report}, year = {2015}, }

Stefan Borgwardt and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Infinitely Valued Gödel Semantics for Expressive Description Logics**. LTCS-Report 15-11, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BoPe-LTCS-15-11, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {15-11}, title = {Infinitely Valued G{\"o}del Semantics for Expressive Description Logics}, type = {LTCS-Report}, year = {2015}, }

Veronika Thost, Jan Holste, and Özgür Özçep:

Abstract BibTeX Entry PDF File

**On Implementing Temporal Query Answering in DL-Lite**. LTCS-Report 15-12, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ THOe-LTCS-15-12, address = {Dresden, Germany}, author = {Veronika {Thost} and Jan {Holste} and \"Ozg\"ur {\"Oz\c{c}ep}}, institution = {Chair of Automata Theory, TU Dresden}, number = {15-12}, title = {On Implementing Temporal Query Answering in {\textit{DL-Lite}}}, type = {LTCS-Report}, year = {2015}, }

Daniel Borchmann, Felix Distel, and Francesco Kriegel:

Abstract BibTeX Entry PDF File

**Axiomatization of General Concept Inclusions from Finite Interpretations**. LTCS-Report 15-13, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BoDiKr-LTCS-15-13, address = {Dresden, Germany}, author = {Daniel {Borchmann} and Felix {Distel} and Francesco {Kriegel}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {15-13}, title = {{Axiomatization of General Concept Inclusions from Finite Interpretations}}, type = {LTCS-Report}, year = {2015}, }

Francesco Kriegel:

Abstract BibTeX Entry PDF File

**Learning General Concept Inclusions in Probabilistic Description Logics**. LTCS-Report 15-14, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ Kr-LTCS-15-14, address = {Dresden, Germany}, author = {Francesco {Kriegel}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {15-14}, title = {Learning General Concept Inclusions in Probabilistic Description Logics}, type = {LTCS-Report}, year = {2015}, }

Stefan Borgwardt and Veronika Thost:

Abstract BibTeX Entry PDF File

**Temporal Query Answering in DL-Lite with Negation**. LTCS-Report 15-16, Chair for Automata Theory, Technische Universität Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BoTh-LTCS-15-16, address = {Germany}, author = {Stefan {Borgwardt} and Veronika {Thost}}, institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden}, number = {15-16}, title = {Temporal Query Answering in {{\textit{DL-Lite}}} with Negation}, type = {LTCS-Report}, year = {2015}, }

Franz Baader, Stefan Borgwardt, and Marcel Lippmann:

Abstract BibTeX Entry PDF File

**Temporal Conjunctive Queries in Expressive DLs with Non-simple Roles**. LTCS-Report 15-17, Chair for Automata Theory, Technische Universität Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBL-LTCS-15-17, address = {Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Marcel {Lippmann}}, institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden}, number = {15-17}, title = {Temporal Conjunctive Queries in Expressive {DLs} with Non-simple Roles}, type = {LTCS-Report}, year = {2015}, }

Stefan Borgwardt and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**A Tableau Algorithm for**\(\mathcal{SROIQ}\)**under Infinitely Valued Gödel Semantics**. LTCS-Report 15-18, Chair for Automata Theory, Technische Universität Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ BoPe-LTCS-15-18, address = {Germany}, author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Technische Universit{\"a}t Dresden}, number = {15-18}, title = {A Tableau Algorithm for {$\mathcal{SROIQ}$} under Infinitely Valued {G}{\"o}del Semantics}, type = {LTCS-Report}, year = {2015}, }

Benjamin Zarrieß and Jens Claßen:

Abstract BibTeX Entry PDF File

**Decidable Verification of Golog Programs over Non-Local Effect Actions**. LTCS-Report 15-19, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2015.Abstract BibTeX Entry PDF File

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.

@techreport{ ZaCla-LTCS-15-19, address = {Dresden, Germany}, author = {Benjamin {Zarrie{\ss}} and Jens {Cla{\ss}en}}, institution = {Chair of Automata Theory, TU Dresden}, note = {Extended version. See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {15-19}, title = {Decidable Verification of Golog Programs over Non-Local Effect Actions}, type = {LTCS-Report}, year = {2015}, }

## 2014

Franz Baader and Marcel Lippmann:

Abstract BibTeX Entry PDF File

**Runtime Verification Using a Temporal Description Logic Revisited**. LTCS-Report 14-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014.Abstract BibTeX Entry PDF File

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.

@techreport{ BaLi-LTCS-14-01, address = {Dresden, Germany}, author = {Franz {Baader} and Marcel {Lippmann}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {14-01}, title = {Runtime Verification Using a Temporal Description Logic Revisited}, type = {LTCS-Report}, year = {2014}, }

Stefan Borgwardt:

Abstract BibTeX Entry PDF File

**The Complexity of Fuzzy Description Logics over Finite Lattices with Nominals**. LTCS-Report 14-02, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014.Abstract BibTeX Entry PDF File

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.

@techreport{ Borg-LTCS-14-02, address = {Dresden, Germany}, author = {Stefan {Borgwardt}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {14-02}, title = {The Complexity of Fuzzy Description Logics over Finite Lattices with Nominals}, type = {LTCS-Report}, year = {2014}, }

Franz Baader and Barbara Morawska:

Abstract BibTeX Entry PDF File

**Matching with respect to general concept inclusions in the Description Logic**\(\mathcal{EL}\). LTCS-Report 14-03, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014.Abstract BibTeX Entry PDF File

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.

@techreport{ BaMo-LTCS-14-3, address = {Dresden, Germany}, author = {Franz {Baader} and Barbara {Morawska}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {14-03}, title = {Matching with respect to general concept inclusions in the Description Logic $\mathcal{EL}$}, type = {LTCS-Report}, year = {2014}, }

Rafael Peñaloza, Veronika Thost, and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File

**Conjunctive Query Answering in Rough EL**. LTCS-Report 14-04, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014.Abstract BibTeX Entry PDF File

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.

@techreport{ PeTT-LTCS-14-04, address = {Dresden, Germany}, author = {Rafael {Pe{\~n}aloza} and Veronika {Thost} and Anni-Yasmin {Turhan}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {14-04}, title = {Conjunctive Query Answering in Rough EL}, type = {LTCS-Report}, year = {2014}, }

Yue Ma and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Towards Parallel Repair Using Decompositions**. LTCS-Report 14-05, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014.Abstract BibTeX Entry PDF File

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.

@techreport{ MaPe-LTCS-14-05, address = {Dresden, Germany}, author = {Yue {Ma} and Rafael {Pe{\~n}aloza}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {14-05}, title = {Towards Parallel Repair Using Decompositions}, type = {LTCS-Report}, year = {2014}, }

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost:

Abstract BibTeX Entry PDF File

**Reasoning with Temporal Properties over Axioms of DL-Lite**. LTCS-Report 14-06, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2014.Abstract BibTeX Entry PDF File

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.

@techreport{ BoLT-LTCS-13-05, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Marcel {Lippmann} and Veronika {Thost}}, institution = {Chair of Automata Theory, TU Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {14-06}, title = {Reasoning with Temporal Properties over Axioms of \textit{DL-Lite}}, type = {LTCS-Report}, year = {2014}, }

Michel Ludwig and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Error-Tolerant Reasoning in the Description Logic EL**. LTCS-Report 14-11, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2014.Abstract BibTeX Entry PDF File

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.

@techreport{ LuPe-LTCS-14-11, address = {Dresden, Germany}, author = {Michel {Ludwig} and Rafael {Pe{\~n}aloza}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {14-11}, title = {Error-Tolerant Reasoning in the Description Logic EL}, type = {LTCS-Report}, year = {2014}, }

## 2013

Franz Baader, Stefan Borgwardt, and Marcel Lippmann:

Abstract BibTeX Entry PDF File

**On the Complexity of Temporal Query Answering**. LTCS-Report 13-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBoLi-LTCS-13-01, address = {Dresden, Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Marcel {Lippmann}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {13-01}, title = {On the Complexity of Temporal Query Answering}, type = {LTCS-Report}, year = {2013}, }

Daniel Borchmann:

Abstract BibTeX Entry PDF File

**A General Form of Attribute Exploration**. LTCS-Report 13-02, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ Borc-LTCS-13-02, address = {Dresden, Germany}, author = {Daniel {Borchmann}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {13-02}, title = {{A General Form of Attribute Exploration}}, type = {LTCS-Report}, year = {2013}, }

Yue Ma and Felix Distel:

Abstract BibTeX Entry PDF File

**Learning Formal Definitions for Snomed CT from Text**. LTCS-Report 13-03, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ MaDi-LTCS-13-03, address = {Dresden, Germany}, author = {Yue {Ma} and Felix {Distel}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {13-03}, title = {{Learning Formal Definitions for Snomed CT from Text}}, type = {LTCS-Report}, year = {2013}, }

Daniel Borchmann:

Abstract BibTeX Entry PDF File

**Exploration by Confidence**. LTCS-Report 13-04, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ Borch-LTCS-13-04, address = {Dresden, Germany}, author = {Daniel {Borchmann}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {13-04}, title = {{Exploration by Confidence}}, type = {LTCS-Report}, year = {2013}, }

Stefan Borgwardt, Marcel Lippmann, and Veronika Thost:

Abstract BibTeX Entry PDF File

**Temporal Query Answering w.r.t. DL-Lite-Ontologies**. LTCS-Report 13-05, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ BoLT-LTCS-13-05, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Marcel {Lippmann} and Veronika {Thost}}, institution = {Chair of Automata Theory, TU Dresden}, note = {Revised version. See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {13-05}, title = {Temporal Query Answering w.r.t.\ \textit{DL-Lite}-Ontologies}, type = {LTCS-Report}, year = {2013}, }

Benjamin Zarrieß and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File

**Most Specific Generalizations w.r.t. General**\(\mathcal{EL}\)**-TBoxes**. LTCS-Report 13-06, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ ZaTu-LTCS-13-06, address = {Dresden, Germany}, author = {Benjamin {Zarrie{\"s}} and Anni-Yasmin {Turhan}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {13-06}, title = {Most Specific Generalizations w.r.t.\ General $\mathcal{EL}$-TBoxes}, type = {LTCS-Report}, year = {2013}, }

Franz Baader, Oliver Fernández Gil, and Barbara Morawska:

Abstract BibTeX Entry PDF File

**Hybrid Unification in the Description Logic EL**. LTCS-Report 13-07, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ BaFM-LTCS-13-07, address = {Dresden, Germany}, author = {Franz {Baader} and Oliver {Fern\'{a}ndez Gil} and Barbara {Morawska}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {13-07}, title = {Hybrid Unification in the Description Logic EL}, type = {LTCS-Report}, year = {2013}, }

Franz Baader and Benjamin Zarrieß:

BibTeX Entry PDF File

**Verification of Golog Programs over Description Logic Actions**. LTCS-Report 13-08, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2013.BibTeX Entry PDF File

@techreport{ BaZa-LTCS-13-08, address = {Dresden, Germany}, author = {Franz {Baader} and Benjamin {Zarrie{\"s}}}, institution = {Chair of Automata Theory, TU Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {13-08}, title = {Verification of Golog Programs over Description Logic Actions}, type = {LTCS-Report}, year = {2013}, }

Stefan Borgwardt, Felix Distel, and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Goedel Description Logics: Decidability in the Absence of the Finitely-Valued Model Property**. LTCS-Report 13-09, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ BoDP-LTCS-13-09, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Felix {Distel} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {13-09}, title = {Goedel Description Logics: Decidability in the Absence of the Finitely-Valued Model Property}, type = {LTCS-Report}, year = {2013}, }

Benjamin Zarrieß and Jens Claßen:

Abstract BibTeX Entry PDF File

**On the Decidability of Verifying LTL Properties of Golog Programs**. LTCS-Report 13-10, Chair of Automata Theory, TU Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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 C^{2}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.

@techreport{ ZaCla-LTCS-13-10, address = {Dresden, Germany}, author = {Benjamin {Zarrie{\ss}} and Jens {Cla{\ss}en}}, institution = {Chair of Automata Theory, TU Dresden}, note = {Extended version. See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {13-10}, title = {On the Decidability of Verifying LTL Properties of Golog Programs}, type = {LTCS-Report}, year = {2013}, }

Daniel Borchmann:

Abstract BibTeX Entry PDF File

**Model Exploration by Confidence with Completely Specified Counterexamples**. LTCS-Report 13-11, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ Borc-LTCS-13-11, address = {Dresden, Germany}, author = {Daniel {Borchmann}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {13-11}, title = {{Model Exploration by Confidence with Completely Specified Counterexamples}}, type = {LTCS-Report}, year = {2013}, }

Andreas Ecke and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File

**Similarity Measures for Computing Relaxed Instances w.r.t. General**\(\mathcal{EL}\)**-TBoxes**. LTCS-Report 13-12, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2013.Abstract BibTeX Entry PDF File

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.

@techreport{ EcTu-TR-13, address = {Dresden, Germany}, author = {Andreas {Ecke} and Anni-Yasmin {Turhan}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See \url{http://lat.inf.tu-dresden.de/research/reports.html}.}, number = {13-12}, title = {Similarity Measures for Computing Relaxed Instances w.r.t.\ General $\mathcal{EL}$-{TBoxes}}, type = {LTCS-Report}, year = {2013}, }

## 2012

Franz Baader and Alexander Okhotin:

Abstract BibTeX Entry PDF File

**Solving Language Equations and Disequations Using Looping Tree Automata with Colors**. LTCS-Report 12-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012.Abstract BibTeX Entry PDF File

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.

@techreport{ BaOk-LTCS-12-01, address = {Dresden, Germany}, author = {Franz {Baader} and Alexander {Okhotin}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {12-01}, title = {Solving Language Equations and Disequations Using Looping Tree Automata with Colors}, type = {LTCS-Report}, year = {2012}, }

Franz Baader, Stefan Borgwardt, and Barbara Morawska:

Abstract BibTeX Entry PDF File

**SAT Encoding of Unification in**\(\mathcal{ELH}_{R^+}\)**w.r.t. Cycle-Restricted Ontologies**. LTCS-Report 12-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBM-LTCS-12-02, address = {Dresden, Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {12-02}, title = {{SAT} Encoding of Unification in {$\mathcal{ELH}_{R^+}$} w.r.t. Cycle-Restricted Ontologies}, type = {LTCS-Report}, year = {2012}, }

Franz Baader, Stefan Borgwardt, and Barbara Morawska:

Abstract BibTeX Entry PDF File

**Computing Minimal**\(\mathcal{EL}\)**-Unifiers is Hard**. LTCS-Report 12-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBM-LTCS-12-03, address = {Dresden, Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {12-03}, title = {Computing Minimal {$\mathcal{EL}$}-Unifiers is Hard}, type = {LTCS-Report}, year = {2012}, }

Stefan Borgwardt and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Consistency in Fuzzy Description Logics over Residuated De Morgan Lattices**. LTCS-Report 12-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012.Abstract BibTeX Entry PDF File

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.

@techreport{ BoPe-LTCS-12-04, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {12-04}, title = {Consistency in Fuzzy Description Logics over Residuated De Morgan Lattices}, type = {LTCS-Report}, year = {2012}, }

Franz Baader, Stefan Borgwardt, and Barbara Morawska:

Abstract BibTeX Entry PDF File

**A Goal-Oriented Algorithm for Unification in**\(\mathcal{ELH}_{R^+}\)**w.r.t. Cycle-Restricted Ontologies**. LTCS-Report 12-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBM-LTCS-12-05, address = {Dresden, Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {12-05}, title = {A Goal-Oriented Algorithm for Unification in {$\mathcal{ELH}_{R^+}$} w.r.t. Cycle-Restricted Ontologies}, type = {LTCS-Report}, year = {2012}, }

Daniel Borchmann:

Abstract BibTeX Entry PDF File

**On Confident GCIs of Finite Interpretations**. LTCS-Report 12-06, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2012.Abstract BibTeX Entry PDF File

In the work of Baader and Distel, a method has been proposed to axiomatize all general concept inclusions (GCIs) expressible in the description logic EL^{b}ot and valid in a given interpretation I. This provides us with an effective method to learn EL^{b}ot 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 EL_{g}fp^{b}ot bases into EL^{b}ot bases.

@techreport{ Borc-LTCS-12-06, address = {Dresden, Germany}, author = {Daniel {Borchmann}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {12-06}, title = {On Confident GCIs of Finite Interpretations}, type = {LTCS-Report}, year = {2012}, }

## 2011

Franz Baader, Nguyen Thanh Binh, Stefan Borgwardt, and Barbara Morawska:

Abstract BibTeX Entry PDF File

**Unification in the Description Logic**\(\mathcal{EL}\)**Without the Top Concept**. LTCS-Report 11-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.Abstract BibTeX Entry PDF File

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.

@techreport{ BBBM-LTCS-11-01, address = {Dresden, Germany}, author = {Franz {Baader} and Nguyen Thanh {Binh} and Stefan {Borgwardt} and Barbara {Morawska}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {11-01}, title = {Unification in the Description Logic {$\mathcal{EL}$} Without the Top Concept}, type = {LTCS-Report}, year = {2011}, }

Stefan Borgwardt and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Complementation and Inclusion of Weighted Automata on Infinite Trees: Revised Version**. LTCS-Report 11-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.Abstract BibTeX Entry PDF File

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.

@techreport{ BoPe-LTCS-11-02, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {11-02}, title = {Complementation and Inclusion of Weighted Automata on Infinite Trees: Revised Version}, type = {LTCS-Report}, year = {2011}, }

Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Towards a Tableau Algorithm for Fuzzy ALC with Product T-norm**. LTCS-Report 11-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.Abstract BibTeX Entry PDF File

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.

@techreport{ Pena-LTCS-11-03, address = {Dresden, Germany}, author = {Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {11-03}, title = {Towards a Tableau Algorithm for Fuzzy ALC with Product T-norm}, type = {LTCS-Report}, year = {2011}, }

Stefan Borgwardt and Barbara Morawska:

Abstract BibTeX Entry PDF File

**Finding Finite Herbrand Models**. LTCS-Report 11-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.Abstract BibTeX Entry PDF File

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 FL_{0}. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.

@techreport{ BoMo-LTCS-11-04, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Barbara {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {11-04}, title = {Finding Finite {H}erbrand Models}, type = {LTCS-Report}, year = {2011}, }

Franz Baader, Stefan Borgwardt, and Barbara Morawska:

Abstract BibTeX Entry PDF File

**Unification in the Description Logic**\(\mathcal{EL}\)**w.r.t. Cycle-Restricted TBoxes**. LTCS-Report 11-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.Abstract BibTeX Entry PDF File

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.

@techreport{ BaBM-LTCS-11-05, address = {Dresden, Germany}, author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {11-05}, title = {Unification in the Description Logic {$\mathcal{EL}$} w.r.t.\ Cycle-Restricted {TB}oxes}, type = {LTCS-Report}, year = {2011}, }

Stefan Borgwardt and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Undecidability of Fuzzy Description Logics**. LTCS-Report 11-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2011.Abstract BibTeX Entry PDF File

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.

@techreport{ BoPe-LTCS-11-06, address = {Dresden, Germany}, author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {11-06}, title = {Undecidability of Fuzzy Description Logics}, type = {LTCS-Report}, year = {2011}, }

## 2010

Franz Baader, Marcel Lippmann, and Hongkai Liu:

Abstract BibTeX Entry PDF File

**Adding Causal Relationships to DL-based Action Formalisms**. LTCS-Report 10-01, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2010.Abstract BibTeX Entry PDF File

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.

@techreport{ BaLiLi-LTCS-10-01, address = {Dresden, Germany}, author = {Franz {Baader} and Marcel {Lippmann} and Hongkai {Liu}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {10-01}, title = {Adding Causal Relationships to {DL}-based Action Formalisms}, type = {LTCS-Report}, year = {2010}, }

Franz Baader and Barbara Morawska:

Abstract BibTeX Entry PDF File

**SAT Encoding of Unification in**\(\mathcal{EL}\). LTCS-Report 10-04, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2010.Abstract BibTeX Entry PDF File

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.

@techreport{ BaMo-LTCS-10-04, address = {Dresden, Germany}, author = {Franz {Baader} and Barbara {Morawska}}, institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {10-04}, title = {SAT Encoding of Unification in $\mathcal{EL}$}, type = {LTCS-Report}, year = {2010}, }

Rafael Peñaloza and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File PS File

**Completion-based computation of least common subsumers with limited role-depth for**\({\mathcal{EL}}\)**and Prob-**\({\mathcal{EL}^{01}}\). LTCS-Report LTCS-10-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2010.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ PenTur-ltcs-10-02, address = {Germany}, author = {Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-10-02}, title = {Completion-based computation of least common subsumers with limited role-depth for {${\mathcal{EL}}$} and Prob-{${\mathcal{EL}^{01}}$}}, type = {LTCS-Report}, year = {2010}, }

Rafael Peñaloza and Anni-Yasmin Turhan:

Abstract BibTeX Entry PDF File PS File

**Completion-based computation of most specific concepts with limited role-depth for**\({\mathcal{EL}}\)**and Prob-**\({\mathcal{EL}^{01}}\). LTCS-Report LTCS-10-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2010.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ PenTur-ltcs-10-03, address = {Germany}, author = {Rafael {Pe{\~n}aloza} and Anni-Yasmin {Turhan}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-10-03}, title = {Completion-based computation of most specific concepts with limited role-depth for {${\mathcal{EL}}$} and Prob-{${\mathcal{EL}^{01}}$}}, type = {LTCS-Report}, year = {2010}, }

Stefan Borgwardt and Rafael Peñaloza:

Abstract BibTeX Entry PDF File

**Complementation and Inclusion of Weighted Automata on Infinite Trees**. LTCS-Report LTCS-10-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2010.Abstract BibTeX Entry PDF File

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.

@techreport{ BoPe-ltcs-10-05, address = {Germany}, author = {Stefan {Borgwardt} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-10-05}, title = {Complementation and Inclusion of Weighted Automata on Infinite Trees}, type = {LTCS-Report}, year = {2010}, }

## 2009

Conrad Drescher, Hongkai Liu, Franz Baader, Steffen Guhlemann, Uwe Petersohn, Peter Steinke, and Michael Thielscher:

Abstract BibTeX Entry PDF File

**Putting ABox Updates into Action**. LTCS-Report 09-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2009.Abstract BibTeX Entry PDF File

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.

@techreport{ LTCS-Report09-01, address = {Germany}, author = {Conrad {Drescher} and Hongkai {Liu} and Franz {Baader} and Steffen {Guhlemann} and Uwe {Petersohn} and Peter {Steinke} and Michael {Thielscher}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {09-01}, title = {Putting ABox Updates into Action}, type = {LTCS-Report}, year = {2009}, }

Franz Baader, Martin Knechtel, and Rafael Peñaloza:

Abstract BibTeX Entry PDF File PS File

**Computing Boundaries for Reasoning in Sub-Ontologies**. LTCS-Report 09-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2009.Abstract BibTeX Entry PDF File PS File

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 O_{l}, 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 O_{l}is the sub-ontology that a user with access right l is allowed to see, or as trust levels, in which case O_{l}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 O_{l}, determined by lattice elements l, C still follows. However, instead of reasoning with O_{l}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 m_{C}of L such that C follows from O_{l}iff l is smaller or equal to m_{C}. 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.

@techreport{ BaKP-LTCS-09, address = {Germany}, author = {Franz {Baader} and Martin {Knechtel} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {09-02}, title = {Computing Boundaries for Reasoning in Sub-Ontologies}, type = {LTCS-Report}, year = {2009}, }

Rafael Peñaloza and Barış Sertkaya:

Abstract BibTeX Entry PDF File PS File

**On the Complexity of Axiom Pinpointing in Description Logics**. LTCS-Report 09-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2009.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ PeSe-LTCS-09-04, address = {Germany}, author = {Rafael {Pe{\~n}aloza} and Bar\i{}\c{s} {Sertkaya}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {09-04}, title = {On the Complexity of Axiom Pinpointing in Description Logics}, type = {LTCS-Report}, year = {2009}, }

Franz Baader, Hongkai Liu, and Anees ul Mehdi:

Abstract BibTeX Entry PDF File

**Integrate Action Formalisms into Linear Temporal Description Logics**. LTCS-Report LTCS-09-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2009.Abstract BibTeX Entry PDF File

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.

@techreport{ BMLSW-LTCS-09-03, address = {Germany}, author = {Franz {Baader} and Hongkai {Liu} and Anees ul {Mehdi}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-09-03}, title = {{I}ntegrate {A}ction {F}ormalisms into {L}inear {T}emporal {D}escription {L}ogics}, type = {LTCS-Report}, year = {2009}, }

## 2008

Franz Baader, Silvio Ghilardi, and Carsten Lutz:

Abstract BibTeX Entry PDF File PS File

**LTL over Description Logic Axioms**. LTCS-Report 08-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2008.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ LTCS-Report08-01, address = {Germany}, author = {Franz {Baader} and Silvio {Ghilardi} and Carsten {Lutz}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {08-01}, title = {{LTL} over Description Logic Axioms}, type = {LTCS-Report}, year = {2008}, }

Felix Distel:

Abstract BibTeX Entry PDF File PS File

**Model-based Most Specific Concepts in Description Logics with Value Restrictions**. 08-04, Institute for theoretical computer science, TU Dresden, Dresden, Germany, 2008.Abstract BibTeX Entry PDF File PS File

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 logicsFLOandFLEwith cyclic TBoxes and forALCwith acyclic TBoxes. Since subsumption in^{}FLEwith 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.

@techreport{ Dist08, address = {Dresden, Germany}, author = {Felix {Distel}}, institution = {Institute for theoretical computer science, TU Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {08-04}, title = {Model-based Most Specific Concepts in Description Logics with Value Restrictions}, year = {2008}, }

Franz Baader and Felix Distel:

Abstract BibTeX Entry PDF File PS File

**Exploring finite models in the Description Logic**\(\mathcal{EL}_\mathrm{gfp}\). LTCS-Report 08-05, Institute for Theoretical Computer Science, TU Dresden, Dresden, 2008.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ BaaDi08, address = {Dresden}, author = {Franz {Baader} and Felix {Distel}}, institution = {Institute for Theoretical Computer Science, TU Dresden}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {08-05}, title = {Exploring finite models in the Description Logic {$\mathcal{EL}_\mathrm{gfp}$}}, type = {LTCS-Report}, year = {2008}, }

Franz Baader and Rafael Peñaloza:

Abstract BibTeX Entry PDF File PS File

**Blocking and Pinpointing in Forest Tableaux**. LTCS-Report LTCS-08-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2008.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ BaPe-LTCS-07-01, address = {Germany}, author = {Franz {Baader} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-08-02}, title = {Blocking and Pinpointing in Forest Tableaux}, type = {LTCS-Report}, year = {2008}, }

Franz Baader and Rafael Peñaloza:

Abstract BibTeX Entry PDF File PS File

**Pinpointing in Terminating Forest Tableaux**. LTCS-Report LTCS-08-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2008.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ BaPe-LTCS-08-03, address = {Germany}, author = {Franz {Baader} and Rafael {Pe{\~n}aloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-08-03}, title = {Pinpointing in Terminating Forest Tableaux}, type = {LTCS-Report}, year = {2008}, }

Barış Sertkaya:

Abstract BibTeX Entry PDF File PS File

**Some Computational Problems Related to Pseudo-intents**. LTCS-Report LTCS-08-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2008.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ sert-08-06, address = {Germany}, author = {Bar{\i}{\c{s}} {Sertkaya}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-08-06}, title = {Some Computational Problems Related to Pseudo-intents}, type = {LTCS-Report}, year = {2008}, }

## 2007

Franz Baader and Felix Distel:

Abstract BibTeX Entry PDF File

**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.Abstract BibTeX Entry PDF File

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.

@techreport{ Dist07, address = {Dresden, Germany}, author = {Franz {Baader} and Felix {Distel}}, institution = {Inst.\ f{\"u}r Theoretische Informatik, TU Dresden}, number = {07-02}, title = {A finite basis for the set of {EL}-implications holding in a finite model}, year = {2007}, }

Boontawee Suntisrivaraporn:

Abstract BibTeX Entry PDF File

**Module Extraction and Incremental Classification: A Pragmatic Approach for EL+ Ontologies**. LTCS-Report LTCS-07-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2007.Abstract BibTeX Entry PDF File

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.

@techreport{ Sun-07-LTCS, address = {Germany}, author = {Boontawee {Suntisrivaraporn}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-07-03}, title = {Module Extraction and Incremental Classification: A Pragmatic Approach for EL+ Ontologies}, type = {LTCS-Report}, year = {2007}, }

## 2006

Franz Baader and Alexander Okhotin:

Abstract BibTeX Entry PDF File PS File

**On Language Equations with One-sided Concatenation**. LTCS-Report LTCS-06-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ BaaderOkhotin-LTCS-06-01, address = {Germany}, author = {Franz {Baader} and Alexander {Okhotin}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-06-01}, title = {On Language Equations with One-sided Concatenation}, type = {LTCS-Report}, year = {2006}, }

Franz Baader, Bernhard Ganter, Ulrike Sattler, and Baris Sertkaya:

Abstract BibTeX Entry PDF File PS File

**Completing Description Logic Knowledge Bases using Formal Concept Analysis**. LTCS-Report LTCS-06-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ BGSS-LTCS-06-02, address = {Germany}, author = {Franz {Baader} and Bernhard {Ganter} and Ulrike {Sattler} and Baris {Sertkaya}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-06-02}, title = {Completing Description Logic Knowledge Bases using Formal Concept Analysis}, type = {LTCS-Report}, year = {2006}, }

H. Liu, C. Lutz, M. Milicic, and F. Wolter:

Abstract BibTeX Entry PDF File

**Description Logic Actions with general TBoxes: a Pragmatic Approach**. LTCS-Report LTCS-06-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006.Abstract BibTeX Entry PDF File

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.

@techreport{ LiLuMiWo-LTCS-06-03, address = {Germany}, author = {H. {Liu} and C. {Lutz} and M. {Milicic} and F. {Wolter}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-06-03}, title = {Description Logic Actions with general {T}{B}oxes: a Pragmatic Approach}, type = {LTCS-Report}, year = {2006}, }

F. Baader, J. Hladik, and R. Penaloza:

Abstract BibTeX Entry PDF File

**PSPACE Automata with Blocking for Description Logics**. LTCS-Report LTCS-06-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006.Abstract BibTeX Entry PDF File

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.

@techreport{ BaaHlaPen-LTCS-06, address = {Germany}, author = {F. {Baader} and J. {Hladik} and R. {Penaloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-06-04}, title = {{PSPACE} Automata with Blocking for Description Logics}, type = {LTCS-Report}, year = {2006}, }

Rafael Penaloza:

Abstract BibTeX Entry PDF File PS File

**Pinpointing in Tableaus**. LTCS-Report LTCS-06-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ Penaloza-LTCS-06-05, address = {Germany}, author = {Rafael {Penaloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-06-05}, title = {Pinpointing in Tableaus}, type = {LTCS-Report}, year = {2006}, }

Franz Baader and Rafael Penaloza:

Abstract BibTeX Entry PDF File PS File

**Axiom Pinpointing in General Tableaux**. LTCS-Report LTCS-07-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2006.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ BaaderPenaloza-LTCS-07-01, address = {Germany}, author = {Franz {Baader} and Rafael {Penaloza}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-07-01}, title = {Axiom Pinpointing in General Tableaux}, type = {LTCS-Report}, year = {2006}, }

## 2005

F. Baader, S. Brandt, and C. Lutz:

Abstract BibTeX Entry PS File

**Pushing the EL Envelope**. LTCS-Report LTCS-05-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderBrandtLutz-LTCS-05-01, address = {Germany}, author = {F. {Baader} and S. {Brandt} and C. {Lutz}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-01}, title = {Pushing the EL Envelope}, type = {LTCS-Report}, year = {2005}, }

F. Baader, M. Milicic, C. Lutz, U. Sattler, and F. Wolter:

Abstract BibTeX Entry PS File

**Integrating Description Logics and Action Formalisms for Reasoning about Web Services**. LTCS-Report LTCS-05-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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.

@techreport{ BMLSW-LTCS-05-02, address = {Germany}, author = {F. {Baader} and M. {Milicic} and C. {Lutz} and U. {Sattler} and F. {Wolter}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-02}, title = {Integrating Description Logics and Action Formalisms for Reasoning about Web Services}, type = {LTCS-Report}, year = {2005}, }

C. Lutz, D. Walther, and F. Wolter:

Abstract BibTeX Entry PS File

**Quantitative Temporal Logics: PSpace and below**. LTCS-Report LTCS-05-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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.

@techreport{ LutzWaltherWolter-LTCS-05-03, address = {Germany}, author = {C. {Lutz} and D. {Walther} and F. {Wolter}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-03}, title = {Quantitative Temporal Logics: PSpace and below}, type = {LTCS-Report}, year = {2005}, }

Franz Baader and Silvio Ghilardi:

Abstract BibTeX Entry PS File

**Connecting Many-Sorted Theories**. LTCS-Report LTCS-05-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderGhilardiLTCS-05-04, address = {Germany}, author = {Franz {Baader} and Silvio {Ghilardi}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-04}, title = {Connecting Many-Sorted Theories}, type = {LTCS-Report}, year = {2005}, }

C. Lutz:

Abstract BibTeX Entry PS File

**PDL with Intersection and Converse is Decidable**. LTCS-Report LTCS-05-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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).

@techreport{ Lutz-LTCS-05-05, address = {Germany}, author = {C. {Lutz}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-05}, title = {PDL with Intersection and Converse is Decidable}, type = {LTCS-Report}, year = {2005}, }

P. Bonatti, C. Lutz, and F. Wolter:

Abstract BibTeX Entry PS File

**Expressive Non-Monotonic Description Logics Based on Circumscription**. LTCS-Report LTCS-05-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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 NP^{N}Exp and NExp^{N}P, 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.

@techreport{ BonattiLutzWolter-LTCS-05-06, address = {Germany}, author = {P. {Bonatti} and C. {Lutz} and F. {Wolter}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-06}, title = {Expressive Non-Monotonic Description Logics Based on Circumscription}, type = {LTCS-Report}, year = {2005}, }

C. Lutz and M. Milicic:

Abstract BibTeX Entry PS File

**A Tableau Algorithm for DLs with Concrete Domains and GCIs**. LTCS-Report LTCS-05-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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.

@techreport{ LutzMilicic-LTCS-05-07, address = {Germany}, author = {C. {Lutz} and M. {Milicic}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-07}, title = {A Tableau Algorithm for DLs with Concrete Domains and GCIs}, type = {LTCS-Report}, year = {2005}, }

Franz Baader, Carsten Lutz, Eldar Karabaev, and Manfred Theißen:

Abstract BibTeX Entry PDF File PS File

**A New**\(n\)**-ary Existential Quantifier in Description Logics**. LTCS-Report LTCS-05-08, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ BaaderEtAll-LTCS-05-08, address = {Germany}, author = {Franz {Baader} and Carsten {Lutz} and Eldar {Karabaev} and Manfred {Thei{\ss}en}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-08}, title = {A New $n$-ary Existential Quantifier in Description Logics}, type = {LTCS-Report}, year = {2005}, }

C. Lutz:

Abstract BibTeX Entry PS File

**Complexity and Succinctness of Public Announcement Logic**. LTCS-Report LTCS-05-09, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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.

@techreport{ Lutz-LTCS-05-09, address = {Germany}, author = {C. {Lutz}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-09}, title = {Complexity and Succinctness of Public Announcement Logic}, type = {LTCS-Report}, year = {2005}, }

H. Liu, C. Lutz, M. Milicic, and F. Wolter:

Abstract BibTeX Entry PS File

**Updating Description Logic ABoxes**. LTCS-Report LTCS-05-10, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005.Abstract BibTeX Entry PS File

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).

@techreport{ LiLuMiWo-LTCS-05-10, address = {Germany}, author = {H. {Liu} and C. {Lutz} and M. {Milicic} and F. {Wolter}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-05-10}, title = {Updating Description Logic ABoxes}, type = {LTCS-Report}, year = {2005}, }

## 2004

B. Morawska:

Abstract BibTeX Entry PS File

**A nice Cycle Rule for Goal-Directed**\(E\)**-Unification**. LTCS-Report LTCS-04-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004.Abstract BibTeX Entry PS File

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.

@techreport{ Morawska-LTCS-04-01, address = {Germany}, author = {B. {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-04-01}, title = {A nice Cycle Rule for Goal-Directed $E$-Unification}, type = {LTCS-Report}, year = {2004}, }

F. Baader:

Abstract BibTeX Entry PS File

**A Graph-Theoretic Generalization of the Least Common Subsumer and the Most Specific Concept in the Description Logic EL**. LTCS-Report LTCS-04-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004.Abstract BibTeX Entry PS File

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.

@techreport{ Baader-LTCS-04-02, address = {Germany}, author = {F. {Baader}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-04-02}, title = {A Graph-Theoretic Generalization of the Least Common Subsumer and the Most Specific Concept in the Description Logic EL}, type = {LTCS-Report}, year = {2004}, }

S. Brandt:

Abstract BibTeX Entry PDF File PS File

**Reasoning in**\(\mathcal{ELH}\)**w.r.t. General Concept Inclusion Axioms**. LTCS-Report LTCS-04-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ Brandt-LTCS-04-03, address = {Germany}, author = {S. {Brandt}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-04-03}, title = {Reasoning in $\mathcal{ELH}$ w.r.t.\ General Concept Inclusion Axioms}, type = {LTCS-Report}, year = {2004}, }

S. Brandt:

Abstract BibTeX Entry PDF File

**Subsumption and Instance Problem in**\(\mathcal{ELH}\)**w.r.t. General TBoxes**. LTCS-Report LTCS-04-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004.Abstract BibTeX Entry PDF File

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.

@techreport{ Brandt-LTCS-04-04, address = {Germany}, author = {S. {Brandt}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-04-04}, title = {Subsumption and Instance Problem in $\mathcal{ELH}$ w.r.t.\ General TBoxes}, type = {LTCS-Report}, year = {2004}, }

C. Lutz and F. Wolter:

Abstract BibTeX Entry PS File

**Modal Logics of Topological Relations**. LTCS-Report LTCS-04-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004.Abstract BibTeX Entry PS File

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.

@techreport{ LutzWolter-LTCS-04-05, address = {Germany}, author = {C. {Lutz} and F. {Wolter}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-04-05}, title = {Modal Logics of Topological Relations}, type = {LTCS-Report}, year = {2004}, }

C. Lutz and M. Milicic:

Abstract BibTeX Entry PDF File PS File

**Description Logics with Concrete Domains and Functional Dependencies**. LTCS-Report LTCS-04-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2004.Abstract BibTeX Entry PDF File PS File

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.

@techreport{ LutzMilicic-LTCS-04-06, address = {Germany}, author = {C. {Lutz} and M. {Milicic}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-04-06}, title = {Description Logics with Concrete Domains and Functional Dependencies}, type = {LTCS-Report}, year = {2004}, }

## 2003

S. Brandt, A.-Y. Turhan, and R. Küsters:

Abstract BibTeX Entry PS File

**Foundations of non-standard Inferences for Description Logics with transitive Roles and Role Hierarchies**. LTCS-Report 03-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003.Abstract BibTeX Entry PS File

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).

@techreport{ BrTuKu-LTCS-03-02, address = {Germany}, author = {S. {Brandt} and A.-Y. {Turhan} and R. {K{\"u}sters}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, number = {03-02}, title = {Foundations of non-standard Inferences for Description Logics with transitive Roles and Role Hierarchies}, type = {LTCS-Report}, year = {2003}, }

F. Baader:

Abstract BibTeX Entry PS File

**The Instance Problem and the Most Specific Concept in the Description Logic**\(\mathcal{EL}\)**w.r.t. Terminological Cycles with Descriptive Semantics**. LTCS-Report LTCS-03-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003.Abstract BibTeX Entry PS File

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.

@techreport{ Baader-LTCS-03-01, address = {Germany}, author = {F. {Baader}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-03-01}, title = {The Instance Problem and the Most Specific Concept in the Description Logic {$\mathcal{EL}$} w.r.t.\ Terminological Cycles with Descriptive Semantics}, type = {LTCS-Report}, year = {2003}, }

B. Morawska:

Abstract BibTeX Entry PS File

**Completness of**\(E\)**-unification with eager Variable Elimination**. LTCS-Report LTCS-03-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003.Abstract BibTeX Entry PS File

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.

@techreport{ Morawska-LTCS-03-03, address = {Germany}, author = {B. {Morawska}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-03-03}, title = {Completness of $E$-unification with eager Variable Elimination}, type = {LTCS-Report}, year = {2003}, }

C. Lutz and D. Walther:

Abstract BibTeX Entry PS File

**PDL with Negation of Atomic Programs**. LTCS-Report LTCS-03-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003.Abstract BibTeX Entry PS File

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.

@techreport{ LuWa-LTCS-03-04, address = {Germany}, author = {C. {Lutz} and D. {Walther}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-03-04}, title = {PDL with Negation of Atomic Programs}, type = {LTCS-Report}, year = {2003}, }

F. Baader, Silvio Ghilardi, and Cesare Tinelli:

Abstract BibTeX Entry PS File

**A New Combination Procedure for the Word Problem that Generalizes Fusion Decidability Results in Modal Logics**. LTCS-Report LTCS-03-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003.Abstract BibTeX Entry PS File

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.

@techreport{ BaGiTiLTCS-03-05, address = {Germany}, author = {F. {Baader} and Silvio {Ghilardi} and Cesare {Tinelli}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-03-05}, title = {A New Combination Procedure for the Word Problem that Generalizes Fusion Decidability Results in Modal Logics}, type = {LTCS-Report}, year = {2003}, }

## 2002

S. Brandt and A.-Y. Turhan:

Abstract BibTeX Entry PS File

**An Approach for Optimizing ALE-Approximation of ALC-Concepts**. LTCS-Report 02-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.Abstract BibTeX Entry PS File

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.

@techreport{ BrTu-LTCS-02, address = {Germany}, author = {S. {Brandt} and A.-Y. {Turhan}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {02-03}, title = {An Approach for Optimizing {ALE}-Approximation of {ALC}-Concepts}, type = {LTCS-Report}, year = {2002}, }

C. Lutz:

Abstract BibTeX Entry PS File

**Reasoning about Entity Relationship Diagrams with Complex Attribute Dependencies**. LTCS-Report LTCS-02-01, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2002.Abstract BibTeX Entry PS File

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.

@techreport{ Lutz-LTCS-02-01, address = {Germany}, author = {C. {Lutz}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-02-01}, title = {Reasoning about Entity Relationship Diagrams with Complex Attribute Dependencies}, type = {LTCS-Report}, year = {2002}, }

F. Baader:

Abstract BibTeX Entry PS File

**Terminological Cycles in a Description Logic with Existential Restrictions**. LTCS-Report LTCS-02-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.Abstract BibTeX Entry PS File

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.

@techreport{ Baader-LTCS-02-02, address = {Germany}, author = {F. {Baader}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-02-02}, title = {Terminological Cycles in a Description Logic with Existential Restrictions}, type = {LTCS-Report}, year = {2002}, }

C. Lutz, C. Areces, I. Horrocks, and U. Sattler:

Abstract BibTeX Entry PS File

**Keys, Nominals, and Concrete Domains**. LTCS-Report LTCS-02-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.Abstract BibTeX Entry PS File

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.

@techreport{ LutAreHorSat-LTCS-02-04, address = {Germany}, author = {C. {Lutz} and C. {Areces} and I. {Horrocks} and U. {Sattler}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-02-04}, title = {Keys, Nominals, and Concrete Domains}, type = {LTCS-Report}, year = {2002}, }

C. Lutz, U. Sattler, and L. Tendera:

Abstract BibTeX Entry PS File

**The Complexity of Finite Model Reasoning in Description Logics**. LTCS-Report LTCS-02-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.Abstract BibTeX Entry PS File

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.

@techreport{ LutzSattlerTendera-LTCS-02-05, address = {Germany}, author = {C. {Lutz} and U. {Sattler} and L. {Tendera}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-02-05}, title = {The Complexity of Finite Model Reasoning in Description Logics}, type = {LTCS-Report}, year = {2002}, }

I. Horrocks and U. Sattler:

Abstract BibTeX Entry PS File

**Decidability of SHIQ with Complex Role Inclusion Axioms**. LTCS-Report LTCS-02-06, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.Abstract BibTeX Entry PS File

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.

@techreport{ HorrocksSattler-LTCS-02-06, address = {Germany}, author = {I. {Horrocks} and U. {Sattler}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-02-06}, title = {Decidability of {SHIQ} with Complex Role Inclusion Axioms}, type = {LTCS-Report}, year = {2002}, }

F. Baader:

Abstract BibTeX Entry PS File

**Least Common Subsumers, Most Specific Concepts, and Role-Value-Maps in a Description Logic with Existential Restrictions and Terminological Cycles**. LTCS-Report LTCS-02-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.Abstract BibTeX Entry PS File

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.

@techreport{ Baader-LTCS-02-07, address = {Germany}, author = {F. {Baader}}, institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology}, note = {See http://lat.inf.tu-dresden.de/research/reports.html.}, number = {LTCS-02-07}, title = {Least Common Subsumers, Most Specific Concepts, and Role-Value-Maps in a Description Logic with Existential Restrictions and Terminological Cycles}, type = {LTCS-Report}, year = {2002}, }

## 2001

F. Baader, S. Brandt, and R. Küsters:

Abstract BibTeX Entry PS File

**Matching under Side Conditions in Description Logics**. LTCS-Report 01-02, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.Abstract BibTeX Entry PS File

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 \(\aln\) and its sublanguages.

@techreport{ BaaderBrandt+-LTCS-01-02, address = {Germany}, author = {F. {Baader} and S. {Brandt} and R. {K{\"u}sters}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {01-02}, title = {Matching under Side Conditions in Description Logics}, type = {LTCS-Report}, year = {2001}, }

F. Baader and S. Tobies:

Abstract BibTeX Entry PS File

**The Inverse Method Implements the Automata Approach for Modal Satisfiability**. LTCS-Report 01-03, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderTobies-LTCS-01-03, address = {Germany}, author = {F. {Baader} and S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {01-03}, title = {The Inverse Method Implements the Automata Approach for Modal Satisfiability}, type = {LTCS-Report}, year = {2001}, }

F. Baader and R. Küsters:

Abstract BibTeX Entry PS File

**Unification in a Description Logic with Transitive Closure of Roles**. LTCS-Report 01-05, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.Abstract BibTeX Entry PS File

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 FL_{0}, 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 FL_{0}) 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.

@techreport{ BaaderKuesters-LTCS-01-05, address = {Germany}, author = {F. {Baader} and R. {K{\"u}sters}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {01-05}, title = {Unification in a Description Logic with Transitive Closure of Roles}, type = {LTCS-Report}, year = {2001}, }

S. Brandt, R. Küsters, and A.-Y. Turhan:

Abstract BibTeX Entry PS File

**Approximation and Difference in Description Logics**. LTCS-Report 01-06, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.Abstract BibTeX Entry PS File

Approximation is a new inference service in Description Logics first mentioned by Baader, Kü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.

@techreport{ BrandtKuesters+-LTCS-01-06, address = {Germany}, author = {S. {Brandt} and R. {K{\"u}sters} and A.-Y. {Turhan}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, number = {01-06}, title = {Approximation and Difference in Description Logics}, type = {LTCS-Report}, year = {2001}, }

C. Lutz, H. Sturm, F. Wolter, and M. Zakharyaschev:

Abstract BibTeX Entry PS File

**A Tableau Calculus for Temporal Description Logic: The Constant Domain Case**. LTCS-Report LTCS-01-01, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.Abstract BibTeX Entry PS File

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 PTL_{A}LC 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.

@techreport{ LuStuWoZa-LTCS-01-01, address = {Germany}, author = {C. {Lutz} and H. {Sturm} and F. {Wolter} and M. {Zakharyaschev}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-01-01}, title = {A Tableau Calculus for Temporal Description Logic: The Constant Domain Case}, type = {LTCS-Report}, year = {2001}, }

C. Lutz, U. Sattler, and F. Wolter:

Abstract BibTeX Entry PS File

**Modal Logic and the two-variable fragment**. LTCS-Report LTCS-01-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.Abstract BibTeX Entry PS File

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 FO^{2}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 FO^{2}satisfiability is NExpTime-complete. We indicate that the relation between L and FO^{2}provides a general framework for comparing modal and temporal languages with first-order languages.

@techreport{ LutzSattlerWolter-LTCS-01-04, address = {Germany}, author = {C. {Lutz} and U. {Sattler} and F. {Wolter}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-01-04}, title = {Modal Logic and the two-variable fragment}, type = {LTCS-Report}, year = {2001}, }

C. Lutz:

Abstract BibTeX Entry PS File

**Adding Numbers to the**\({\cal SHIQ}\)**Description Logic—First Results**. LTCS-Report LTCS-01-07, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.Abstract BibTeX Entry PS File

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.

@techreport{ Lutz-LTCS-01-07, address = {Germany}, author = {C. {Lutz}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-01-07}, title = {Adding Numbers to the ${\cal SHIQ}$ Description Logic---First Results}, type = {LTCS-Report}, year = {2001}, }

I. Horrocks and U. Sattler:

Abstract BibTeX Entry PS File

**Optimised Reasoning for SHIQ**. LTCS-Report LTCS-01-08, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2001.Abstract BibTeX Entry PS File

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. <p> 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. <p> 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.

@techreport{ HorrocksSattler-LTCS-01-08, address = {Germany}, author = {I. {Horrocks} and U. {Sattler}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-01-08}, title = {Optimised Reasoning for SHIQ}, type = {LTCS-Report}, year = {2001}, }

## 2000

F. Baader, R. Küsters, and R. Molitor:

Abstract BibTeX Entry PS File

**Rewriting Concepts Using Terminologies – Revisited**. LTCS-Report 00-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderKuestersMolitor-LTCS-00-04, address = {Germany}, author = {F. {Baader} and R. {K{\"u}sters} and R. {Molitor}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {00-04}, title = {Rewriting Concepts Using Terminologies -- Revisited}, type = {LTCS-Report}, year = {2000}, }

R. Küsters and R. Molitor:

Abstract BibTeX Entry PS File

**Computing Most Specific Concepts in Description Logics with Existential Restrictions**. LTCS-Report 00-05, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.Abstract BibTeX Entry PS File

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.

@techreport{ KuestersMolitor-LTCS-00-05, address = {RWTH Aachen, Germany}, author = {R. {K{\"u}sters} and R. {Molitor}}, institution = {LuFG Theoretical Computer Science}, number = {00-05}, title = {Computing Most Specific Concepts in Description Logics with Existential Restrictions}, type = {LTCS-Report}, year = {2000}, }

R. Küsters and R. Molitor:

Abstract BibTeX Entry PS File

**Computing Least Common Subsumers in ALEN**. LTCS-Report 00-07, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.Abstract BibTeX Entry PS File

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.

@techreport{ KuestersMolitor-LTCS-00-07, address = {Germany}, author = {R. {K{\"u}sters} and R. {Molitor}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {00-07}, title = {Computing Least Common Subsumers in ALEN}, type = {LTCS-Report}, year = {2000}, }

C. Lutz:

Abstract BibTeX Entry PS File

**NExpTime-complete Description Logics with Concrete Domains**. LTCS-Report LTCS-00-01, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.Abstract BibTeX Entry PS File

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: <UL> <LI> acyclic TBoxes <LI> inverse roles, and <LI> a role-forming predicate constructor. </UL> 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.

@techreport{ Lutz-LTCS-00-01, address = {Germany}, author = {C. {Lutz}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-00-01}, title = {NExpTime-complete Description Logics with Concrete Domains}, type = {LTCS-Report}, year = {2000}, }

C. Lutz and U. Sattler:

Abstract BibTeX Entry PS File

**The Complexity of Reasoning with Boolean Modal Logics (Extended Version)**. LTCS-Report LTCS-00-02, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.Abstract BibTeX Entry PS File

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.

@techreport{ Lutz-Sattler-LTCS-00-02, address = {Germany}, author = {C. {Lutz} and U. {Sattler}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-00-02}, title = {The Complexity of Reasoning with Boolean Modal Logics (Extended Version)}, type = {LTCS-Report}, year = {2000}, }

C. Hirsch and S. Tobies:

BibTeX Entry PS File

**A Tableaux Algorithm for the Clique Guarded Fragment, Preliminary Version**. LTCS-Report LTCS-00-03, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.BibTeX Entry PS File

@techreport{ Hirsch-Tobies-LTCS-00-03, address = {Germany}, author = {C. {Hirsch} and S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-00-03}, title = {A Tableaux Algorithm for the Clique Guarded Fragment, Preliminary Version}, type = {LTCS-Report}, year = {2000}, }

C. Lutz:

Abstract BibTeX Entry PS File

**Interval-based Temporal Reasoning with General TBoxes**. LTCS-Report LTCS-00-06, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 2000.Abstract BibTeX Entry PS File

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.

@techreport{ Lutz-LTCS-00-06, address = {Germany}, author = {C. {Lutz}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-00-06}, title = {Interval-based Temporal Reasoning with General TBoxes}, type = {LTCS-Report}, year = {2000}, }

## 1999

F. Baader, R. Küsters, and R. Molitor:

Abstract BibTeX Entry PS File

**Rewriting Concepts Using Terminologies – Revisited**. LTCS-Report 99-12, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

@techreport{ BaaderKuestersMolitor-LTCS-99-12, address = {Germany}, author = {F. {Baader} and R. {K{\"u}sters} and R. {Molitor}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {Please refer to the revised version LTCS-Report 00-04.}, number = {99-12}, title = {Rewriting Concepts Using Terminologies -- Revisited}, type = {LTCS-Report}, year = {1999}, }

Franz Baader and Cesare Tinelli:

Abstract BibTeX Entry PS File

**Combining Equational Theories Sharing Non-Collapse-Free Constructors**. 99-13, Department of Computer Science, University of Iowa, October 1999.Abstract BibTeX Entry PS File

In a previous work, we describe a method to combine decision procedures for the word problem for theories sharing constructors. One of the requirements of our combination method is that the constructors be collapse-free. This paper removes that requirement by modifying the method so that it applies to non-collapse-free constructors as well. This broadens the scope of our combination results considerably, for example in the direction of equational theories corresponding to modal logics.

@techreport{ Baader-Tinelli-Report-99-13, author = {Franz {Baader} and Cesare {Tinelli}}, institution = {Department of Computer Science, University of Iowa}, month = {October}, number = {99-13}, title = {Combining Equational Theories Sharing Non-Collapse-Free Constructors}, year = {1999}, }

A. Borgida and R. Küsters:

BibTeX Entry PS File

**What's not in a name? Initial Explorations of a Structural Approach to Integrating Large Concept Knowledge-Bases**. DCS-TR-391, Rutgers University, USA, 1999.BibTeX Entry PS File

@techreport{ BorgidaKuesters-DCS-TR-391-1999, author = {A. {Borgida} and R. {K{\"u}sters}}, institution = {Rutgers University, USA}, number = {DCS-TR-391}, title = {What's not in a name? {I}nitial Explorations of a Structural Approach to Integrating Large Concept Knowledge-Bases}, year = {1999}, }

R. Küsters and A. Borgida:

Abstract BibTeX Entry PS File

**What's in an Attribute? Consequences for the Least Common Subsumer**. DCS-TR-404, Rutgers University, USA, 1999.Abstract BibTeX Entry PS File

Functional relationships between objects, called ``attributes'', are of considerable importance in knowledge representation languages, including Description Logics (DLs). A study of the literature indicates that papers have made, often implicitly, different assumptions about the nature of attributes: whether they are always required to have a value, or whether they can be partial functions. The work presented here is the first explicit study of this difference for (sub-)classes of the CLASSIC DL, involving the same-as concept constructor. It is shown that although determining subsumption between concept descriptions has the same complexity (though requiring different algorithms), the story is different in the case of determining the least common subsumer (lcs). For attributes interpreted as partial functions, the lcs exists and can be computed relatively easily; even in this case our results correct and extend three previous papers about the lcs of DLs. In the case where attributes must have a value, the lcs may not exist, and even if it exists it may be of exponential size. Interestingly, it is possible to decide in polynomial time if the lcs exists.

@techreport{ KuestersBorgida-DCS-TR-404-1999, author = {R. {K{\"u}sters} and A. {Borgida}}, institution = {Rutgers University, USA}, number = {DCS-TR-404}, title = {What's in an Attribute? {C}onsequences for the Least Common Subsumer}, year = {1999}, }

C. Lutz:

Abstract BibTeX Entry PS File

**The Complexity of Reasoning with Concrete Domains (Revised Version)**. LTCS-Report LTCS-99-01, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ Lutz-LTCS-99-01, address = {Germany}, author = {C. {Lutz}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.}, number = {LTCS-99-01}, title = {The Complexity of Reasoning with Concrete Domains (Revised Version)}, type = {LTCS-Report}, year = {1999}, }

M.-S. Hacid and C. Rigotti:

Abstract BibTeX Entry PS File

**Representing and Reasoning on Conceptual Queries Over Image Databases**. LTCS-Report LTCS-99-02, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ Hacid-Rigotti-LTCS-99, address = {Germany}, author = {M.-S. {~Hacid} and C. {Rigotti}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html}, number = {LTCS-99-02}, title = {{R}epresenting and {R}easoning on {C}onceptual {Q}ueries {O}ver {I}mage {D}atabases}, type = {LTCS-Report}, year = {1999}, }

C. Decleir, M.-S. Hacid, and J. Kouloumdjian:

Abstract BibTeX Entry PS File

**A Database Approach for Modeling and Querying Video Data**. LTCS-Report LTCS-99-03, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ Decleir-Hacid-Kouloumdjian-LTCS-99, address = {Germany}, author = {C. {Decleir} and M.-S. {Hacid} and J. {Kouloumdjian}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html}, number = {LTCS-99-03}, title = {{A} {D}atabase {A}pproach for {M}odeling and {Q}uerying {V}ideo {D}ata}, type = {LTCS-Report}, year = {1999}, }

C. Lutz:

Abstract BibTeX Entry

**On the Complexity of Terminological Reasoning**. LTCS-Report LTCS-99-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry

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.

@techreport{ Lutz-LTCS-99-04, address = {Germany}, author = {C. {Lutz}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {This report is superceded by the LTCS-00-01 technical report and my LPAR'99 paper.}, number = {LTCS-99-04}, title = {On the Complexity of Terminological Reasoning}, type = {LTCS-Report}, year = {1999}, }

S. Tobies:

Abstract BibTeX Entry PS File

**A NEXPTIME-complete Description Logic Strictly Contained in**\(C^2\). LTCS-Report LTCS-99-05, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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 C^{2}, the two variable fragment of predicate logic with counting quantifiers. We prove that ALCQI has the same complexity as C^{2}but does not reach its expressive power.

@techreport{ Tobies-LTCS-99-05, address = {Germany}, author = {S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {An abriged version appeared at CSL-99.}, number = {LTCS-99-05}, title = {A NEXPTIME-complete Description Logic Strictly Contained in {$C^2$}}, type = {LTCS-Report}, year = {1999}, }

F. Baader and R. Molitor:

Abstract BibTeX Entry PS File

**Rewriting Concepts using Terminologies**. LTCS-Report LTCS-99-06, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderMolitor-LTCS-99-06, address = {Germany}, author = {F. {Baader} and R. {Molitor}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html}, number = {LTCS-99-06}, title = {Rewriting Concepts using Terminologies}, type = {LTCS-Report}, year = {1999}, }

F. Baader and R. Küsters:

Abstract BibTeX Entry PS File

**Matching in Description Logics with Existential Restrictions**. LTCS-Report LTCS-99-07, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderKuesters-LTCS-99-07-1999, address = {Germany}, author = {F. {Baader} and R. {K{\"u}sters}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html}, number = {LTCS-99-07}, title = {Matching in Description Logics with Existential Restrictions}, type = {LTCS-Report}, year = {1999}, }

I. Horrocks, U. Sattler, and S. Tobies:

Abstract BibTeX Entry PS File

**A Description Logic with Transitive and Converse Roles, Role Hierarchies and Qualifying Number Restrictions**. LTCS-Report LTCS-99-08, LuFG Theoretical Computer Science, RWTH Aachen, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ HoSatTob-LTCS-99-08, author = {I. {Horrocks} and U. {Sattler} and S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {Revised version. See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html}, number = {LTCS-99-08}, title = {A Description Logic with Transitive and Converse Roles, Role Hierarchies and Qualifying Number Restrictions}, type = {LTCS-Report}, year = {1999}, }

S. Tobies:

Abstract BibTeX Entry PS File

**A PSpace-algorithm for ALCQI-satisfiability**. LTCS-Report LTCS-99-09, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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 HREF=http://www-lti.informatik.rwth-aachen.de/Forschung/Papers-1999.html#Tobies-CADE-99>A PSPACE Algorithm for Graded Modal Logic</A> to deal with qualifying number restrictions and from <A HREF=http://www-lti.informatik.rwth-aachen.de/Forschung/Papers-1999.html#HorrocksSattlerTobies-M4M-99>Practical Reasoning for Description Logics with Functional Restrictions, Inverse and Transitive Roles, and Role Hierarchies</A> to deal with converse roles.

@techreport{ Tobies-LTCS-99-09, address = {Germany}, author = {S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.}, number = {LTCS-99-09}, title = {A {PSpace}-algorithm for {ALCQI}-satisfiability}, type = {LTCS-Report}, year = {1999}, }

S. Tobies:

Abstract BibTeX Entry PS File

**PSpace Reasoning for DLs with Qualifying Number Restrictions**. LTCS-Report LTCS-99-11, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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 HREF=http://www-lti.informatik.rwth-aachen.de/Forschung/Papers-1999.html#Tobies-CADE-99>A PSPACE Algorithm for Graded Modal Logic</A> to deal with qualifying number restrictions and from <A HREF=http://www-lti.informatik.rwth-aachen.de/Forschung/Papers-1999.html#HorrocksSattlerTobies-M4M-99>Practical Reasoning for Description Logics with Functional Restrictions, Inverse and Transitive Roles, and Role Hierarchies</A> to deal with converse roles. Additionally, we extend the result to ALCQIR which extends ALCQI by role intersections.

@techreport{ Tobies-LTCS-99-11, address = {Germany}, author = {S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.}, number = {LTCS-99-11}, title = {{PSpace} Reasoning for {DLs} with Qualifying Number Restrictions}, type = {LTCS-Report}, year = {1999}, }

F. Baader and R. Küsters:

Abstract BibTeX Entry PS File

**Matching Concept Descriptions with Existential Restrictions Revisited**. LTCS-Report LTCS-99-13, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderKuesters-LTCS-99-13-1999, address = {Germany}, author = {F. {Baader} and R. {K{\"u}sters}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-99-13}, title = {Matching Concept Descriptions with Existential Restrictions Revisited}, type = {LTCS-Report}, year = {1999}, }

I. Horrocks and S. Tobies:

Abstract BibTeX Entry PS File

**Optimisation of Terminological Reasoning**. LTCS-Report LTCS-99-14, LuFG Theoretical Computer Science, RWTH Aachen, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ HorrocksTobies-LTCS-99-14, author = {I. {Horrocks} and S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html}, number = {LTCS-99-14}, title = {Optimisation of Terminological Reasoning}, type = {LTCS-Report}, year = {1999}, }

I. Horrocks, U. Sattler, S. Tessaris, and S. Tobies:

Abstract BibTeX Entry PS File

**Query Containment Using a DLR ABox**. LTCS-Report LTCS-99-15, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1999.Abstract BibTeX Entry PS File

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.

@techreport{ HorrocksSattler+-LTCS-99-15, address = {Germany}, author = {I. {Horrocks} and U. {Sattler} and S. {Tessaris} and S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-99-15}, title = {Query Containment Using a {DLR} {ABox}}, type = {LTCS-Report}, year = {1999}, }

## 1998

Martin Leucker and Stephan Tobies:

Abstract BibTeX Entry PS File

**Truth—A Platform for Verification of Distributed Systems**. Aachener Informatik Bericht 98-05, RWTH Aachen, May 1998.Abstract BibTeX Entry PS File

Formal Methods are becoming more an more important for the development of hardware and software systems. Verification tools support the employment of Formal Methods. This paper gives an overview of the design and implementation of the verification tool Truth. We define and explain requirements for verification tools. Furthermore, we discuss several semantic models, specification languages and logics and their visualisation from a tool builder's perspective and show how these requirements were adopted in Truth.

@techreport{ LeuckerTobies-AIB-98-5, author = {Martin {Leucker} and Stephan {Tobies}}, institution = {RWTH Aachen}, month = {May}, number = {98-05}, title = {Truth---A Platform for Verification of Distributed Systems}, type = {Aachener Informatik Bericht}, year = {1998}, }

C.B. Tresp and R. Molitor:

Abstract BibTeX Entry PS File

**A Description Logic for Vague Knowledge**. LTCS-Report LTCS-98-01, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.Abstract BibTeX Entry PS File

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.

@techreport{ TrespMolitor-LTCS-98-01, address = {Germany}, author = {C.B. {Tresp} and R. {Molitor}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html}, number = {LTCS-98-01}, title = {A Description Logic for Vague Knowledge}, type = {LTCS-Report}, year = {1998}, }

F. Baader and U. Sattler:

BibTeX Entry PS File

**Description Logics with Aggregates and Concrete Domains, Part II (extended)**. LTCS-Report LTCS-98-02, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.BibTeX Entry PS File

@techreport{ BaSat98, author = {F. {Baader} and U. {Sattler}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-98-02}, title = {Description Logics with Aggregates and Concrete Domains, Part II (extended)}, type = {LTCS-Report}, year = {1998}, }

R. Molitor:

BibTeX Entry PS File

**Structural Subsumption for**\(\cal A\!L\!N\). LTCS-Report LTCS-98-03, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998.BibTeX Entry PS File

@techreport{ Molitor-LTCS-98-03, author = {R. {Molitor}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-98-03}, title = {Structural {S}ubsumption for {$\cal A\!L\!N$}}, type = {LTCS-Report}, year = {1998}, }

F. Baader, R. Küsters, and R. Molitor:

Abstract BibTeX Entry PS File PS File

**Structural Subsumption Considered from an Automata Theoretic Point of View**. LTCS-Report LTCS-98-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998.Abstract BibTeX Entry PS File PS File

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.

@techreport{ BaaderKuestersMolitor-LTCS-98-04, address = {Germany}, author = {F. {Baader} and R. {K{\"u}sters} and R. {Molitor}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-98-04}, title = {Structural Subsumption Considered from an Automata Theoretic Point of View}, type = {LTCS-Report}, year = {1998}, }

I. Horrocks and U. Sattler:

BibTeX Entry PS File

**A Description Logic with Transitive and Converse Roles and Role Hierarchies**. LTCS-Report LTCS-98-05, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.BibTeX Entry PS File

@techreport{ HoSat98, author = {I. {Horrocks} and U. {Sattler}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-98-05}, title = {A Description Logic with Transitive and Converse Roles and Role Hierarchies}, type = {LTCS-Report}, year = {1998}, }

F. Baader and R. Küsters:

Abstract BibTeX Entry PS File

**Computing the least common subsumer and the most specific concept in the presence of cyclic ALN-concept descriptions**. LTCS-Report LTCS-98-06, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderKuesters-LTCS-98-06-1998, author = {F. {Baader} and R. {K{\"u}sters}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-98-06}, title = {Computing the least common subsumer and the most specific concept in the presence of cyclic ALN-concept descriptions}, type = {LTCS-Report}, year = {1998}, }

F. Baader and P. Narendran:

Abstract BibTeX Entry PS File

**Unification of Concept Terms in Description Logics: Revised Version**. LTCS-Report LTCS-98-07, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1998.Abstract BibTeX Entry PS File

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.

@techreport{ Baader-Narendran-LTCS-98, author = {F. {Baader} and P. {Narendran}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-98-07}, title = {Unification of Concept Terms in Description Logics: Revised Version}, type = {LTCS-Report}, year = {1998}, }

I. Horrocks, U. Sattler, and S. Tobies:

Abstract BibTeX Entry PS File

**A PSpace-algorithm for deciding**\(\mathcal{ALCNI}_{R^+}\)**-satisfiability**. LTCS-Report LTCS-98-08, LuFG Theoretical Computer Science, RWTH Aachen, 1998.Abstract BibTeX Entry PS File

ALCI_{R+}—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 ALCI_{R+}-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.

@techreport{ HoSatTob98, author = {I. {Horrocks} and U. {Sattler} and S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, number = {LTCS-98-08}, title = {A PSpace-algorithm for deciding {$\mathcal{ALCNI}_{R^+}$}-satisfiability}, type = {LTCS-Report}, year = {1998}, }

F. Baader, R. Küsters, and R. Molitor:

Abstract BibTeX Entry PS File

**Computing Least Common Subsumers in Description Logics with Existential Restrictions**. LTCS-Report LTCS-98-09, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998.Abstract BibTeX Entry PS File

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.

@techreport{ BaaderKuesters+-LTCS-98-09, address = {Germany}, author = {F. {Baader} and R. {K{\"u}sters} and R. {Molitor}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.}, number = {LTCS-98-09}, title = {Computing Least Common Subsumers in Description Logics with Existential Restrictions}, type = {LTCS-Report}, year = {1998}, }

F. Baader, R. Molitor, and S. Tobies:

Abstract BibTeX Entry PS File

**The Guarded Fragment of Conceptual Graphs**. LTCS-Report LTCS-98-10, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998.Abstract BibTeX Entry PS File

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.

@techreport{ Baader-Molitor-Tobies-LTCS-98a, address = {Germany}, author = {F. {Baader} and R. {Molitor} and S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html}, number = {LTCS-98-10}, title = {The Guarded Fragment of Conceptual Graphs}, type = {LTCS-Report}, year = {1998}, }

F. Baader, R. Molitor, and S. Tobies:

BibTeX Entry PS File

**On the Relation between Descripion Logics and Conceptual Graphs**. LTCS-Report LTCS-98-11, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1998.BibTeX Entry PS File

@techreport{ BaaderMolitorTobies-LTCS-98-11, address = {Germany}, author = {F. {Baader} and R. {Molitor} and S. {Tobies}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.}, number = {LTCS-98-11}, title = {On the Relation between Descripion Logics and Conceptual Graphs}, type = {LTCS-Report}, year = {1998}, }

F. Baader and C. Tinelli:

Abstract BibTeX Entry PS File

**Deciding the Word Problem in the Union of Equational Theories**. UIUCDCS-Report UIUCDCS-R-98-2073, Department of Computer Science, University of Illinois at Urbana-Champaign, 1998.Abstract BibTeX Entry PS File

The main contribution of this report is a new method for combining decision procedures for the word problem in equational theories. In contrast to previous methods, it is based on transformation rules, and also applies to theories sharing ``constructors.'' In addition, we show that—contrary to a common belief—the Nelson-Oppen combination method cannot be used to combine decision procedures for the word problem, even in the case of equational theories with disjoint signatures.

@techreport{ Baader-Tinelli-UIUCDCS-R-98-2073, author = {F. {Baader} and C. {Tinelli}}, institution = {Department of Computer Science, University of Illinois at Urbana-Champaign}, number = {UIUCDCS-R-98-2073}, title = {Deciding the Word Problem in the Union of Equational Theories}, type = {{UIUCDCS}-Report}, year = {1998}, }

## 1997

Franz Baader and Klaus U. Schulz:

Abstract BibTeX Entry PS File

**Unification Theory – An Introduction**. Research Report CIS-Rep-97-103, Center for Language and Information Processing (CIS), Oettingenstraße 67, D-80538 Munich, Germany, January 1997.Abstract BibTeX Entry PS File

This work is a preliminary version of the chapter on unification theory in a volume on automated deduction produced by the participants of the nationwide German research programme on automated deduction (SSP ``Deduktion'').

@techreport{ BaaderSchulz-CIS-97-103, address = {Oettingenstra{\ss}e 67, D-80538 Munich, Germany}, author = {Franz {Baader} and Klaus U. {Schulz}}, institution = {Center for Language and Information Processing (CIS)}, month = {January}, number = {CIS-Rep-97-103}, title = {Unification Theory -- {A}n Introduction}, type = {Research Report}, year = {1997}, }

F. Baader and U. Sattler:

Abstract BibTeX Entry PS File

**Description Logics with Aggregates and Concrete Domains**. LTCS-Report LTCS-97-01, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1997.Abstract BibTeX Entry PS File

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.

@techreport{ BaSat97, author = {F. {Baader} and U. {Sattler}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, note = {An abridged version has appeared in the Proceedings of the International Workshop on Description Logics 97.}, number = {LTCS-97-01}, title = {Description Logics with Aggregates and Concrete Domains}, type = {LTCS-Report}, year = {1997}, }

F. Baader and P. Narendran:

Abstract BibTeX Entry PS File

**Unification of Concept Terms in Description Logics**. LTCS-Report LTCS-97-02, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1997.Abstract BibTeX Entry PS File

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.

@techreport{ Baader-Narendran-LTCS-97, author = {F. {Baader} and P. {Narendran}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-97-02}, title = {Unification of Concept Terms in Description Logics}, type = {LTCS-Report}, year = {1997}, }

F. Baader:

Abstract BibTeX Entry PS File

**On the Complexity of Boolean Unification**. LTCS-Report LTCS-97-03, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1997.Abstract BibTeX Entry PS File

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 \(\Pi^p_2\)-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.

@techreport{ Baader-LTCS-97-03, author = {F. {Baader}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-97-03}, title = {On the Complexity of Boolean Unification}, type = {LTCS-Report}, year = {1997}, }

R. Küsters:

Abstract BibTeX Entry PS File

**Characterizing the semantics of terminological cycles in**\(\mathcal{ALN}\)**using finite automata**. LTCS-Report LTCS-97-04, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1997.Abstract BibTeX Entry PS File

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 FL_{0}are extended to the language ALN, which additionally allows for primitive negation and number-restrictions. Unlike FL_{0}, 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 FL_{0}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.

@techreport{ Kuesters-LTCS-97-04, author = {R. {K{\"u}sters}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-97-04}, title = {Characterizing the semantics of terminological cycles in {$\mathcal{ALN}$} using finite automata}, type = {LTCS-Report}, year = {1997}, }

M. S. Hacid, P. Marcel, and C. Rigotti:

Abstract BibTeX Entry PS File

**A rule based data manipulation language for OLAP systems**. LTCS-Report LTCS-97-05, LuFg Theoretical Computer Science, RWTH Aachen, 1997.Abstract BibTeX Entry PS File

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.

@techreport{ Hacid&al97a, author = {M. S. {Hacid} and P. {Marcel} and C. {Rigotti}}, booktitle = {Proc. of the 5th Intl. Conf. on Deductive and Object-Oriented Databases (DOOD'97)}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, note = {A short version has appeared in the Proceedings of the 5th International Conference on Deductive and Object-Oriented Databases (DOOD'97), Montreux, Switzerland}, number = {LTCS-97-05}, publisher = {SPRINGER}, series = {LNCS}, title = {A rule based data manipulation language for {OLAP} systems}, type = {LTCS-Report}, year = {1997}, }

## 1996

F. Baader and C. Tinelli:

Abstract BibTeX Entry PS File

**A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method**. LTCS-Report LTCS-96-01, LuFg Theoretical Computer Science, RWTH Aachen, 1996.Abstract BibTeX Entry PS File

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.

@techreport{ Baader-Tinelli-LTCS-96, author = {F. {Baader} and C. {Tinelli}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, note = {An abridged version has appeared in Proc.\ CADE'97, Springer LNAI 1249.}, number = {LTCS-96-01}, title = {A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the {Nelson-Oppen} Combination Method}, type = {LTCS-Report}, year = {1996}, }

F. Baader and U. Sattler:

BibTeX Entry PS File

**Number Restrictions on Complex Roles in Description Logics**. LTCS-96-02, LuFg Theoretical Computer Science, RWTH Aachen, 1996.BibTeX Entry PS File

@techreport{ BaaderSattler-LTCS-96-02, author = {F. {Baader} and U. {Sattler}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, note = {An abridged version has appeared in the Proceedings of the Fifth International Conference on Knowledge Representation and Reasoning, 1996, Cambridge, Massachusetts.}, number = {LTCS-96-02}, title = {Number Restrictions on Complex Roles in Description Logics}, year = {1996}, }

F. Baader and U. Sattler:

BibTeX Entry PS File

**Description Logics with Symbolic Number Restrictions**. LTCS-96-03, LuFg Theoretical Computer Science, RWTH Aachen, 1996.BibTeX Entry PS File

@techreport{ BaaderSattler-LTCS-96-03, author = {F. {Baader} and U. {Sattler}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen}, note = {An abridged version has appeared in the Proceedings of the 12th European Conference on Artificial Intelligence, 1996, Budapest, Hungary.}, number = {LTCS-96-03}, title = {Description Logics with Symbolic Number Restrictions}, year = {1996}, }

S. Kepser and J. Richts:

Abstract BibTeX Entry PS File

**Optimisation Techniques for Combining Constraint Solvers**. LTCS-Report LTCS-96-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1996.Abstract BibTeX Entry PS File

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.

@techreport{ KepserRichts-LTCS-96-04, address = {Germany}, author = {S. {Kepser} and J. {Richts}}, institution = {LuFG Theoretical Computer Science, RWTH Aachen}, number = {LTCS-96-04}, title = {Optimisation Techniques for Combining Constraint Solvers}, type = {LTCS-Report}, year = {1996}, }

F. Baader:

Abstract BibTeX Entry PS File

**Combination of Compatible Reduction Orderings that are Total on Ground Terms**. LTCS-Report LTCS-96-05, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1996.Abstract BibTeX Entry PS File

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 \(E_1\)-compatible reduction orderings total on \(\Sigma_1\)-ground terms and \(E_2\)-compatible reduction orderings total on \(\Sigma_2\)-ground terms can be used to construct an \((E_1\cup E_2)\)-compatible reduction ordering total on \((\Sigma_1\cup \Sigma_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.

@techreport{ Baader-LTCS-96, author = {F. {Baader}}, institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany}, number = {LTCS-96-05}, title = {Combination of Compatible Reduction Orderings that are Total on Ground Terms}, type = {LTCS-Report}, year = {1996}, }

## 1995

Franz Baader and Hans Jürgen Ohlbach:

Abstract BibTeX Entry PS File

**A Multi-Dimensional Terminological Knowledge Representation Language**. Technical Report MPI-I-95-2-005, Max-Planck-Institut für Informatik, Saarbrücken, 1995.Abstract BibTeX Entry PS File

An extension of the concept description language ALC used in KL-ONE-like terminological reasoning is presented. The extension includes multi-modal operators that can either stand for the usual role quantifications or for modalities such as belief, time etc. The modal operators can be used at all levels of the concept terms, and they can be used to modify both concepts and roles. This is an instance of a new kind of combination of modal logics where the modal operators of one logic may operate directly on the operators of the other logic. Different versions of this logic are investigated and various results about decidability and undecidability are presented. The main problem, however, decidability of the basic version of the logic, remains open.

@techreport{ MPI-I-95-2-005, address = {Saarbr{\"u}cken}, author = {Franz {Baader} and Hans J{\"u}rgen {Ohlbach}}, institution = {Max-Planck-Institut f{\"u}r Informatik}, number = {MPI-I-95-2-005}, pages = {32}, title = {A Multi-Dimensional Terminological Knowledge Representation Language}, type = {Technical Report}, year = {1995}, }

## 1994

F. Baader and K. Schulz:

Abstract BibTeX Entry PS File

**On the Combination of Symbolic Constraints, Solution Domains, and Constraint Solvers**. CIS-Report 94-82, Universität München, 1994.Abstract BibTeX Entry PS File

When combining languages for symbolic constraints, one is typically faced with the problem of how to treat ``mixed'' constraints. The two main problems are (1) how to define a combined solution structure over which these constraints are to be solved, and (2) how to combine the constraint solving methods for pure constraints into one for mixed constraints. The paper introduces the notion of a ``free amalgamated product'' as a possible solution to the first problem. Subsequently, we define so-called simply-combinable structures (SC-structures). For SC-structures over disjoint signatures, a canonical amalgamation construction exists, which for the subclass of strong SC-structures yields the free amalgamated product. The combination technique of [Baader&Schulz92,Baader&Schulz95] can be used to combine constraint solvers for (strong) SC-structures over disjoint signatures into a solver for their (free) amalgamated product. In addition to term algebras modulo equational theories, the class of SC-structures contains many solution structures that have been used in constraint logic programming, such as the algebra of rational trees, feature structures, domains consisting of hereditarily finite (wellfounded or non-wellfounded) nested sets and lists.

@techreport{ CIS-94-82, author = {F. {Baader} and K. {Schulz}}, institution = {Universit\"at M\"unchen}, number = {94-82}, title = {On the Combination of Symbolic Constraints, Solution Domains, and Constraint Solvers}, type = {{CIS}-Report}, year = {1994}, }

Franz Baader and Klaus U. Schulz:

Abstract BibTeX Entry PS File

**Combination of Constraint Solving Techniques: An Algebraic Point of View**. Research Report CIS-Rep-94-75, Center for Language and Information Processing (CIS), Wagmüllerstraße 23, D-80538 Munich, Germany, July 1994.Abstract BibTeX Entry PS File

In a previous paper we have introduced a method that allows one to combine decision procedures for unifiability in disjoint equational theories. Lately, it has turned out that the prerequisite for this method to apply—namely that unification with so-called linear constant restrictions is decidable in the single theories—is equivalent to requiring decidability of the positive fragment of the first order theory of the equational theories. Thus, the combination method can also be seen as a tool for combining decision procedures for positive theories of free algebras defined by equational theories. The present paper uses this observation as the starting point of a more abstract, algebraic approach to formulating and solving the combination problem. Its contributions are twofold. As a new result, we describe an (optimized) extension of our combination method to the case of constraint solvers that also take relational constraints (such as ordering constraints) into account. The second contribution is a new proof method, which depends on abstract notions and results from universal algebra, as opposed to technical manipulations of terms (such as ordered rewriting, abstraction functions, etc.)

@techreport{ BaaderSchulz-CIS-94-75, address = {Wagm\"ullerstra{\ss}e 23, D-80538 Munich, Germany}, author = {Franz {Baader} and Klaus U. {Schulz}}, institution = {Center for Language and Information Processing (CIS)}, month = {July}, number = {CIS-Rep-94-75}, title = {Combination of Constraint Solving Techniques: {A}n Algebraic Point of View}, type = {Research Report}, year = {1994}, }

F. Baader and A. Laux:

Abstract BibTeX Entry

**Terminological Logics with Modal Operators**. DFKI Research Report RR-94-33, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1994.Abstract BibTeX Entry

Terminological knowledge representation formalisms can be used to represent objective, time-independent facts about an application domain. Notions like belief, intentions, time—which are essential for the representation of multi-agent environments—can only be expressed in a very limited way. For such notions, modal logics with possible worlds semantics provides a formally well-founded and well-investigated basis. <P> This paper presents a framework for integrating modal operators into terminological knowledge representation languages. These operators can be used both inside of concept expressions and in front of terminological and assertional axioms. The main restrictions are that all modal operators are interpreted in the basic logic <em>K</em>, and that we consider increasing domains instead of constant domains. We introduce syntax and semantics of the extended language, and show that satisfiability of finite sets of formulas is decidable.

@techreport{ DFKI-RR-94-33, author = {F. {Baader} and A. {Laux}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-94-33}, title = {Terminological Logics with Modal Operators}, type = {{DFKI} Research Report}, year = {1994}, }

## 1993

F. Baader and H.-J. Ohlbach:

BibTeX Entry

**A Multi-Dimensional Terminological Knowledge Representation Language**. MPII Report MPI-I-93-212, Max-Planck-Institut für Informatik, Saarbrücken, 1993.BibTeX Entry

@techreport{ MPII-I-93-212, author = {F. {Baader} and H.-J. {Ohlbach}}, institution = {Max-Planck-Institut f\"ur Informatik, Saarbr\"ucken}, number = {MPI-I-93-212}, title = {A Multi-Dimensional Terminological Knowledge Representation Language}, type = {{MPII} Report}, year = {1993}, }

F. Baader, B. Hollunder, B. Nebel, H.J. Profitlich, and E. Franconi:

BibTeX Entry

**An Empirical Analysis of Optimization Techniques for Terminological Representation Systems, or: Making KRIS get a move on**. DFKI Research Report RR-93-03, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1993.BibTeX Entry

@techreport{ DFKI-RR-93-03, author = {F. {Baader} and B. {Hollunder} and B. {Nebel} and H.J. {Profitlich} and E. {Franconi}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-93-03}, title = {An Empirical Analysis of Optimization Techniques for Terminological Representation Systems, or: {M}aking {KRIS} get a move on}, type = {{DFKI} Research Report}, year = {1993}, }

F. Baader and K. Schulz:

BibTeX Entry

**Combination Techniques and Decision Problems for Disunification**. DFKI Research Report RR-93-05, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1993.BibTeX Entry

@techreport{ DFKI-RR-93-05, author = {F. {Baader} and K. {Schulz}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-93-05}, title = {Combination Techniques and Decision Problems for Disunification}, type = {{DFKI} Research Report}, year = {1993}, }

F. Baader and K. Schlechta:

BibTeX Entry

**A Semantics for Open Normal Defaults via a Modified Preferential Approach**. DFKI Research Report RR-93-13, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1993.BibTeX Entry

@techreport{ DFKI-RR-93-13, author = {F. {Baader} and K. {Schlechta}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-93-13}, title = {A Semantics for Open Normal Defaults via a Modified Preferential Approach}, type = {{DFKI} Research Report}, year = {1993}, }

F. Baader and B. Hollunder:

Abstract BibTeX Entry PS File

**Embedding Defaults into Terminological Representation Systems**. DFKI Research Report RR-93-20, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1993.Abstract BibTeX Entry PS File

We consider the problem of integrating Reiter's default logic into terminological representation systems. It turns out that such an integration is less straightforward than we expected, considering the fact that the terminological language is a decidable sublanguage of first-order logic. Semantically, one has the unpleasant effect that the consequences of a terminological default theory may be rather unintuitive, and may even vary with the syntactic structure of equivalent concept expressions. This is due to the unsatisfactory treatment of open defaults via Skolemization in Reiter's semantics. On the algorithmic side, we show that this treatment may lead to an undecidable default consequence relation, even though our base language is decidable, and we have only finitely many (open) defaults. Because of these problems, we then consider a restricted semantics for open defaults in our terminological default theories: default rules are only applied to individuals that are explicitly present in the knowledge base. In this semantics it is possible to compute all extensions of a finite terminological default theory, which means that this type of default reasoning is decidable.

@techreport{ DFKI-RR-93-20, author = {F. {Baader} and B. {Hollunder}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-93-20}, title = {Embedding Defaults into Terminological Representation Systems}, type = {{DFKI} Research Report}, year = {1993}, }

F. Baader, M. Buchheit, and B. Hollunder:

Abstract BibTeX Entry

**Cardinality Restrictions on Concepts**. DFKI Research Report RR-93-48, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1993.Abstract BibTeX Entry

The concept description formalisms of existing terminological systems allow the user to express local cardinality restrictions on the fillers of a particular role. It is not possible, however, to introduce global restrictions on the number of instances of a given concept. The paper argues that such cardinality restrictions on concepts are of importance in applications such as configuration of technical systems, an application domain of terminological systems that is currently gaining in interest. It shows that including such restrictions into the description language leaves the important inference problems such as instance testing decidable. The algorithm combines and simplifies the ideas developed for the treatment of qualifying number restrictions and of general terminological axioms.

@techreport{ DFKI-RR-93-48, author = {F. {Baader} and M. {Buchheit} and B. {Hollunder}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, note = {A short version has appeared in Proceedings of the {KI}'94, Springer LNCS 861}, number = {{RR}-93-48}, title = {Cardinality Restrictions on Concepts}, type = {{DFKI} Research Report}, year = {1993}, }

## 1992

F. Baader and K. Schulz:

BibTeX Entry

**General A- and AX-Unification via Optimized Combination Procedures**. CIS-Report 92-58, Universität München, 1992.BibTeX Entry

@techreport{ CIS-92-58, author = {F. {Baader} and K. {Schulz}}, institution = {Universit\"at M\"unchen}, number = {92-58}, title = {General {A}- and {AX}-Unification via Optimized Combination Procedures}, type = {{CIS}-Report}, year = {1992}, }

Jörn Richts:

Abstract BibTeX Entry PS File

**Allgemeine**\(AC\)**-Unifikation durch Variablenabstraktion mit Fremdtermbedingungen**. Seki Working Paper SWP–92–12, Fachbereich Informatik, Universität Kaiserslautern, Postfach 3049, D–67663 Kaiserslautern, Germany, 1992.Abstract BibTeX Entry PS File

This work investigates general <em>AC</em>-unification, i.e. unification in the combination of free function symbols and free Abelian semigroups, whose function symbols fulfill associativity and commutativity.<p> The three necessary parts of general <em>AC</em>-unification are presented: a combination algorithm, a procedure for elementary <em>AC</em>-unification, and methods for solving systems of diophantine equations. Starting with A. Boudet's unification algorithm for the combination of regular and collapse-free theories, an efficient algorithm for general <em>AC</em>-unification is developed, setting out conditions that must be fulfilled by the solutions of elementary <em>AC</em>-unification. These conditions are used by the procedure for elementary <em>AC</em>-unification whereby further conditions are set out that must be fulfilled by the solutions of the diophantine equations. Then three methods (those of E. Contejean and H. Devie, E. Domenjoud, L. Pottier) for solving systems of diophantine equations are presented. The three methods are compared and evaluated, trying to use the conditions efficiently.<p> Finally some problems which arise from the reuse of <em>AC</em>-unifiers in unification, such as merging, are presented. It is shown that reusing <em>AC</em>-unifiers for partial problems is often worse than solving the entire problem from the beginning.

@techreport{ SWP-92-12, address = {Postfach 3049, D--67663 Kaiserslautern, Germany}, author = {J{\"o}rn {Richts}}, institution = {Fachbereich Informatik, Universit{\"a}t Kaiserslautern}, number = {SWP--92--12}, title = {Allgemeine {$AC$}-{U}nifikation durch {V}ariablenabstraktion mit {F}remdtermbedingungen}, type = {Seki Working Paper}, year = {1992}, }

F. Baader:

BibTeX Entry

**Unification Theory**. DFKI Research Report RR-92-33, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1992.BibTeX Entry

@techreport{ DFKI-RR-92-33, author = {F. {Baader}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-92-33}, title = {Unification Theory}, type = {{DFKI} Research Report}, year = {1992}, }

F. Baader and P. Hanschke:

BibTeX Entry

**Extensions of Concept Languages for a Mechanical Engineering Application**. DFKI Research Report RR-92-36, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1992.BibTeX Entry

@techreport{ DFKI-RR-92-36, author = {F. {Baader} and P. {Hanschke}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-92-36}, title = {Extensions of Concept Languages for a Mechanical Engineering Application}, type = {{DFKI} Research Report}, year = {1992}, }

F. Baader and B. Hollunder:

BibTeX Entry

**How to Prefer More Specific Defaults in Terminological Default Logic**. DFKI Research Report RR-92-58, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1992.BibTeX Entry

@techreport{ DFKI-RR-92-58, author = {F. {Baader} and B. {Hollunder}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-92-58}, title = {How to Prefer More Specific Defaults in Terminological Default Logic}, type = {{DFKI} Research Report}, year = {1992}, }

## 1991

F. Baader, H.-J. Bürckert, B. Nebel, W. Nutt, and G. Smolka:

BibTeX Entry

**On the Expressivity of Feature Logics with Negation, Functional Uncertainty, and Sort Equations**. DFKI Research Report RR-91-01, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1991.BibTeX Entry

@techreport{ DFKI-RR-91-01, author = {F. {Baader} and H.-J. {B\"urckert} and B. {Nebel} and W. {Nutt} and G. {Smolka}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-91-01}, title = {On the Expressivity of Feature Logics with Negation, Functional Uncertainty, and Sort Equations}, type = {{DFKI} Research Report}, year = {1991}, }

B. Hollunder and F. Baader:

BibTeX Entry

**Qualifying Number Restrictions in Concept Languages**. DFKI Research Report RR-91-03, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1991.BibTeX Entry

@techreport{ DFKI-RR-91-03, author = {B. {Hollunder} and F. {Baader}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-91-03}, title = {Qualifying Number Restrictions in Concept Languages}, type = {{DFKI} Research Report}, year = {1991}, }

F. Baader and P. Hanschke:

Abstract BibTeX Entry PS File

**A Scheme for Integrating Concrete Domains into Concept Languages**. DFKI Research Report RR-91-10, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1991.Abstract BibTeX Entry PS File

A drawback which concept languages based on KL-ONE have is that all the terminological knowledge has to be defined on an abstract logical level. In many applications, one would like to be able to refer to concrete domains and predicates on these domains when defining concepts. Examples for such concrete domains are the integers, the real numbers, or also non-arithmetic domains, and predicates could be equality, inequality, or more complex predicates. In the present paper we shall propose a scheme for integrating such concrete domains into concept languages rather than describing a particular extension by some specific concrete domain. We shall define a terminological and an assertional language, and consider the important inference problems such as subsumption, instantiation, and consistency. The formal semantics as well as the reasoning algorithms are given on the scheme level. In contrast to existing KL-ONE based systems, these algorithms will be not only sound but also complete. They generate subtasks which have to be solved by a special purpose reasoner of the concrete domain.

@techreport{ DFKI-RR-91-10, author = {F. {Baader} and P. {Hanschke}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-91-10}, title = {A Scheme for Integrating Concrete Domains into Concept Languages}, type = {{DFKI} Research Report}, year = {1991}, }

F. Baader and K. Schulz:

Abstract BibTeX Entry PS File

**Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures**. DFKI Research Report RR-91-33, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1991.Abstract BibTeX Entry PS File

Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms which compute finite complete sets of unifiers. Thus the developed combination methods usually cannot be used to combine decision procedures, i.e., algorithms which just decide solvability of unification problems without computing unifiers. In this paper we describe a combination algorithm for decision procedures which works for arbitrary equational theories, provided that solvability of so-called unification problems with constant restrictions—a slight generalization of unification problems with constants—is decidable for these theories. As a consequence of this new method, we can for example show that general A-unifiability, i.e., solvability of A-unification problems with free function symbols, is decidable. Here A stands for the equational theory of one associative function symbol. Our method can also be used to combine algorithms which compute finite complete sets of unifiers. Manfred Schmidt-Schauss' combination result, the until now most general result in this direction, can be obtained as a consequence of this fact. We also get the new result that unification in the union of disjoint equational theories is finitary, if general unification—i.e., unification of terms with additional free function symbols—is finitary in the single theories.

@techreport{ DFKI-RR-91-33, author = {F. {Baader} and K. {Schulz}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-91-33}, title = {Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures}, type = {{DFKI} Research Report}, year = {1991}, }

## 1990

F. Baader:

BibTeX Entry

**Terminological Cycles in KL-ONE-based Knowledge Representation Languages**. DFKI Research Report RR-90-01, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1990.BibTeX Entry

@techreport{ DFKI-RR-90-01, author = {F. {Baader}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-90-01}, title = {Terminological Cycles in {KL}-{ONE}-based Knowledge Representation Languages}, type = {{DFKI} Research Report}, year = {1990}, }

F. Baader:

BibTeX Entry

**A Formal Definition for Expressive Power of Knowledge Representation Languages**. DFKI Research Report RR-90-05, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1990.BibTeX Entry

@techreport{ DFKI-RR-90-05, author = {F. {Baader}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-90-05}, title = {A Formal Definition for Expressive Power of Knowledge Representation Languages}, type = {{DFKI} Research Report}, year = {1990}, }

F. Baader, H.-J. Bürckert, B. Hollunder, W. Nutt, and J. Siekmann:

BibTeX Entry PS File

**Concept Logic**. DFKI Research Report RR-90-10, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1990.BibTeX Entry PS File

@techreport{ DFKI-RR-90-10, author = {F. {Baader} and H.-J. {B\"urckert} and B. {Hollunder} and W. {Nutt} and J. {Siekmann}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-90-10}, title = {Concept Logic}, type = {{DFKI} Research Report}, year = {1990}, }

F. Baader:

BibTeX Entry PS File

**Augmenting Concept Languages by Transitive Closure of Roles: An Alternative to Terminological Cycles**. DFKI Research Report RR-90-13, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1990.BibTeX Entry PS File

@techreport{ DFKI-RR-90-13, author = {F. {Baader}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-90-13}, title = {Augmenting Concept Languages by Transitive Closure of Roles: An Alternative to Terminological Cycles}, type = {{DFKI} Research Report}, year = {1990}, }

F. Baader and W. Nutt:

BibTeX Entry

**Adding Homomorphisms to Commutative/Monoidal Theories, or: How Algebra Can Help in Equational Unification**. DFKI Research Report RR-90-16, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1990.BibTeX Entry

@techreport{ DFKI-RR-90-16, author = {F. {Baader} and W. {Nutt}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{RR}-90-16}, title = {Adding Homomorphisms to Commutative/Monoidal Theories, or: {H}ow Algebra Can Help in Equational Unification}, type = {{DFKI} Research Report}, year = {1990}, }

F. Baader:

BibTeX Entry

**Unification in Commutative Theories, Hilbert's Basis Theorem and Gröbner Bases**. SEKI Report SR-90-1, Universität Kaiserslautern, 1990.BibTeX Entry

@techreport{ SEKI-SR-90-1, author = {F. {Baader}}, institution = {Universit\"at Kaiserslautern}, number = {{SR}-90-1}, title = {Unification in Commutative Theories, {H}ilbert's Basis Theorem and {G}r\"obner Bases}, type = {{SEKI} Report}, year = {1990}, }

F. Baader:

BibTeX Entry

**Unification, Weak Unification, Upper Bound, Lower Bound and Generalization Problems**. SEKI Report SR-90-2, Universität Kaiserslautern, 1990.BibTeX Entry

@techreport{ SEKI-SR-90-2, author = {F. {Baader}}, institution = {Universit\"at Kaiserslautern}, number = {{SR}-90-2}, title = {Unification, Weak Unification, Upper Bound, Lower Bound and Generalization Problems}, type = {{SEKI} Report}, year = {1990}, }

F. Baader and B. Hollunder:

BibTeX Entry

**KRIS: Knowledge Representation and Inference System, System Description**. DFKI Technical Memo TM-90-03, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1990.BibTeX Entry

@techreport{ DFKI-TM-90-03, author = {F. {Baader} and B. {Hollunder}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, number = {{TM}-90-03}, title = {{KRIS}: Knowledge Representation and Inference System, System Description}, type = {{DFKI} Technical Memo}, year = {1990}, }

F. Baader, H.-J. Bürckert, J. Heinsohn, J. Müller, B. Hollunder, B. Nebel, W. Nutt, and H.-J. Profitlich:

Abstract BibTeX Entry PS File

**Terminological Knowledge Representation: A Proposal for a Terminological Logic**. DFKI Technical Memo TM-90-04, Deutsches Forschungszentrum für Künstliche Intelligenz, Kaiserslautern, 1990.Abstract BibTeX Entry PS File

This paper contains a proposal for a terminological logic. The formalisms for representing knowledge as well as the needed inferences are described.

@techreport{ DFKI-TM-90-04, author = {F. {Baader} and H.-J. {B\"urckert} and J. {Heinsohn} and J. {M\"uller} and B. {Hollunder} and B. {Nebel} and W. {Nutt} and H.-J. {Profitlich}}, institution = {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, note = {Updated version, taking into account the results of a discussion at the ``International Worksop on Terminological Logics,'' Dagstuhl, May 1991.}, number = {{TM}-90-04}, title = {Terminological Knowledge Representation: A Proposal for a Terminological Logic}, type = {{DFKI} Technical Memo}, year = {1990}, }

## 1989

F. Baader:

BibTeX Entry

**Unifikation und Reduktionssysteme für Halbgruppenvarietäten**. Arbeitsbericht 8, Institut für Mathematische Maschinen und Datenverarbeitung, Universität Erlangen, 1989.BibTeX Entry

@techreport{ IMMD-89-22-8, author = {F. {Baader}}, institution = {Institut f{\"u}r Mathematische Maschinen und Datenverarbeitung, Universit{\"a}t Erlangen}, note = {Dissertation}, number = {8}, title = {Unifikation und {R}eduktionssysteme f{\"u}r {H}albgruppenvariet{\"a}ten}, type = {Arbeitsbericht}, volume = {22}, year = {1989}, }

## 1985

F. Baader:

BibTeX Entry

**Die S-Varietät DS und einige Untervarietäten**. Arbeitsbericht 8, Institut für Mathematische Maschinen und Datenverarbeitung, Universität Erlangen, 1985.BibTeX Entry

@techreport{ IMMD-85-18-8, author = {F. {Baader}}, institution = {Institut f{\"u}r Mathematische Maschinen und Datenverarbeitung, Universit{\"a}t Erlangen}, number = {8}, title = {Die {S}-{V}ariet{\"a}t {DS} und einige {U}ntervariet{\"a}ten}, type = {Arbeitsbericht}, volume = {18}, year = {1985}, }

Generated 14 August 2018, 13:02:09.