NExpTime-complete Description Logics with Concrete Domains

Carsten Lutz
NExpTime-complete Description Logics with Concrete Domains
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-00-01, 2000. LTCS-Report

Details
Bibtex

KurzfassungAbstract
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:
- acyclic TBoxes
- inverse roles, and
- a role-forming predicate constructor.
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.
Bemerkung: Note: See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@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},
}

NExpTime-complete Description Logics with Concrete Domains

NExpTime-complete Description Logics with Concrete Domains

Carsten LutzCarsten Lutz