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.
ExpTime Tableaux Algorithm for Contextualized ALC
Bozzato, Loris;Homola, Martin;Serafini, Luciano
2013-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.