ExpTime Tableaux Algorithm for Contextualized ALC

Contextualized Knowledge Repository (CKR) is a DL-based framework for representation and reasoning with context dependent knowledge. It addresses the widely recognized need for contextualization of the Semantic Web data sources. Reasoning with CKR is possible thanks to a reduction to standard DL, and more recently a NExpTime tableaux algorithm was introduced for ALC -based CKR. In this paper we present an ExpTime tableaux algorithm for ALC -based CKR. The algorithm not only formally defines a tableaux decision procedure with optimal complexity, it is also presented in a form that can be effectively applied in practice employing a suitable rule application strategy together with node caching.