A Tableau Decision Algorithm for Modalized ALC with Constant Domains

Carsten LutzCarsten Lutz, Holger SturmHolger Sturm, Frank WolterFrank Wolter, M. ZakharyaschevM. Zakharyaschev

Download

Carsten Lutz, Holger Sturm, Frank Wolter, M. Zakharyaschev
A Tableau Decision Algorithm for Modalized ALC with Constant Domains
Studia Logica, 72(2):199-232, 2002

Details
Bibtex

KurzfassungAbstract
The aim of this paper is to construct a tableau decision algorithm for the modal description logic K/ALC with constant domains. More precisely, we present a tableau procedure that is capable of deciding, given an ALC-formula x with extra modal operators (which are applied only to concepts and TBox axioms, but not to roles), whether x is satisfiable in a model with constant domains and arbitrary accessibility relations. Tableau-based algorithms have been shown to be `practical' even for logics of rather high complexity. This gives us grounds to believe that, although the satisfiability problem for K/ALC is known to be NEXPTIME-complete, by providing a tableau decision algorithm we demonstrate that highly expressive description logics with modal operators have a chance to be implementable. The paper gives a solution to an open problem of Baader and Laux.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ LuStuWoZa-02,
  author = {C. {Lutz} and H. {Sturm} and F. {Wolter} and M. {Zakharyaschev}},
  journal = {Studia Logica},
  number = {2},
  pages = {199--232},
  title = {A Tableau Decision Algorithm for Modalized $\mathcal{ALC}$ with Constant Domains},
  volume = {72},
  year = {2002},
}