Soundness Preserving Approximation for TBox Reasoning in R

Abstract. TBox reasoning in description logics is hard. For example, reasoning in SROIQ (i.e. OWL2-DL) is N2EXPTIME-complete; even with R, a fragment of SROIQ supporting ALC GCIs and role chains, the complexity of reasoning is 2EXPTIME-hard. Although various optimisation techniques have been applied, existing tableau-based DL reasoners are still inefficient in dealing with arbitrary GCIs especially when complex role chains present. In this paper, we present a soundness preserving approximation for TBox reasoning in R. The main idea is to convert R ontologies to EL+ with an additional complement table maintaining the complementary relations between named concepts. Since existing benchmarks do not focus on complex GCIs and RIs, we propose a new set of testing ontologies for TBox reasoning in R and our preliminary evaluation shows that a naive implementation of our complement-integrated TBox reasoning algorithm outperforms existing reasoners on most of these ontologies.

• Type: Journal
• Year: 2009
• Where: DLOG
• Authors: Yuan Ren, Jeff Z. Pan, Yuting Zhao
• Keywords: Automated Reasoning, DLOG 2009, Reasoning, Role Chains, Tbox Reasoning