# A Tableau Decision Algorithm for Modalized ALC with Constant Domains

##### Carsten LutzCarsten Lutz,  Holger SturmHolger Sturm,  Frank WolterFrank Wolter,  M. ZakharyaschevM. Zakharyaschev
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
• 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: Automatentheorie
@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},
}
`