Chair for Automata Theory of the Institute for Theoretical Computer Science, Faculty of Computer Science at TU Dresden

Technical Reports

2004

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

Abstract

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

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

Abstract

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

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

Abstract

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

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

Abstract

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

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

Abstract

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

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

Abstract

Description Logics (DLs) with concrete domains are a useful tool in many applications. To further enhance the expressive power of such DLs, it has been proposed to add database-style key constraints. Up to now, however, only uniqueness constraints have been considered in this context, thus neglecting the second fundamental family of key constraints: functional dependencies. In this paper, we consider the basic DL with concrete domains \alcd, 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 \NExpTime-complete in some slightly restricted variants of our logic.

There is also a complete overview of our technical reports.
home Back to the homepage of the Chair for Automata Theory.
Generated at Fri Jun 12 11:21:13 CEST 2009.