A Tableau Algorithm for {DL}s with Concrete Domains and {GCI}s

C. LutzC. Lutz, M. MilicicM. Milicic

Download

C. Lutz, M. Milicic
A Tableau Algorithm for {DL}s with Concrete Domains and {GCI}s
Journal of Automated Reasoning, 38(1--3):227--259, 2007

Details
Bibtex

KurzfassungAbstract
To use description logics (DLs) in an application, it is crucial to
identify a DL that is sufficiently expressive to represent the relevant notions of the application domain, but for which reasoning is still decidable. Two means of expressivity that are required by many modern applications of DLs are concrete domains and general TBoxes. The former are used for decidablening concepts based on concrete qualities of their instances such as the weight, age, duration, and spatial extension. The purpose of the latter is to capture background knowledge by stating that the extension of a concept is included in the extension of another concept. Unfortunately, it is wellknown that combining concrete domains with general TBoxes often leads to DLs for which reasoning is undecidable. In this paper, we identify a general property of concrete domains that is sucient for proving decidability of DLs with both concrete domains and general TBoxes. We exhibit some useful concrete domains, most notably a spatial one based on the RCC-8 relations, which have this property. Then, we present a tableau algorithm for
reasoning in DLs equipped with concrete domains and general TBoxes.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ LuMi-Jar-07,
  author = {C. {Lutz} and M. {Milicic}},
  journal = {Journal of Automated Reasoning},
  number = {1--3},
  pages = {227--259},
  title = {A Tableau Algorithm for {DL}s with Concrete Domains and {GCI}s},
  volume = {38},
  year = {2007},
}