Towards More Effective Tableaux Reasoning for CKR

Contextualized Knowledge Repository (CKR) is a DL based framework for representation and reasoning with context dependent knowledge. The only reasoning algorithm for CKR proposed so far is obtained via reduction to a single DL knowledge base. While this method is useful to prove complexity of reasoning in CKR, it does not provide suggestions for the construction of a genuine contextualized reasoning procedure, taking advantage of the distinctive divide-and-conquer approach of a contextual view. In this paper we present a sound and complete tableaux algorithm for reasoning in ALC-based CKR, an important step towards practical decision algorithms for contextualized knowledge based on ALC and more expressive DL. Consequently we discuss possible optimizations of the algorithm including dimensional coverage caching, parallelization and a set of new rules that optimize the propagation of symbols among local tableaux.