Soundness preserving approximation for TBox reasoning in R

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 inR and our preliminary evaluation shows that a naive implementation of our complement-integrated TBox reasoning algorithm outperforms existing reasoners on most of these ontologies.