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

Technical Reports

2000

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

Abstract

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

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

Abstract

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

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

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

Abstract

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

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

Abstract

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

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

Abstract

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

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

Abstract

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

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.