An optimized KE-tableau-based system for reasoning in the description logic \shdlssx

We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic \(\mathcal {DL}\langle \mathsf {4LQS^{R,\!\times }}\rangle (\mathbf {D})\), in short \(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\). The logic \(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\), representable in the decidable multi-sorted quantified set-theoretic fragment \(\mathsf {4LQS^R}\), combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics.