Tableaux Algorithm for Reasoning with Contextualized Knowledge

The growth of the Semantic Web, a space where heterogeneous and contradicting knowledge sources coexist and are often combined, demands for effective methods to consider also the context within which the knowledge sources are intended to be valid. Contextualized Knowledge Repository (CKR) is a novel representation framework grounded in the well studied AI theories of context, whose aim is to bring the advantages of contextual representation to the Semantic Web. In this paper we present a sound and complete tableaux reasoning procedure for ALC-based CKR. We study the complexity of the algorithm and discuss possible optimization. In fact, this is the first direct tableaux algorithm (i.e., not obtained by reduction) for any kind of CKR. It constitutes an important step towards practical decision algorithms for CKR based on ALC and more expressive DL, as currently the only practical algorithm is a forward chaining algorithm for CKR build on top of OWL Horst.