An optimized KE-tableau-based system for reasoning in the description logic ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\text{\hspace{0.17em}⁣}\times }$ (Extended Version)

We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic $$\mathcal{D}\mathcal{L}$\langle $\mathsf{4}\mathsf{L}\mathsf{Q}{\mathsf{S}}^{\mathsf{R},\text{\hspace{0.17em}⁣}\times }$\rangle($\mathbf{D}$)$,inshort$$\mathcal{D}\mathcal{L}${$\mathbf{D}$}^{4,!\times}$\mathrm{.}Thelogic$$\mathcal{D}\mathcal{L}${$\mathbf{D}$}^{4,!\times}$, representable in the decidable multi-sorted quantified set-theoretic fragment $\mathsf{4}\mathsf{L}\mathsf{Q}{\mathsf{S}}^{\mathsf{R}}$, combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics. Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the $\gamma$-rule. The novel system, called KE${}^{\gamma }$-tableau, turns out to be an improvement of the system introduced in \cite{RR2017} and of standard first-order KE-tableau \cite{dagostino94}. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that the performances of the KE${}^{\gamma }$-tableau-based reasoner are often up to about 400% better than the ones of the other two systems. This a first step towards the construction of efficient reasoners for expressive OWL ontologies based on fragments of computable set-theory.