A C++ reasoner for the description logic ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\text{\hspace{0.17em}⁣}\times }$ (Extended Version)

We present an ongoing implementation of a KE-tableau based reasoner for a decidable fragment of stratified elementary set theory expressing 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}$)$(shortly$$\mathcal{D}\mathcal{L}$_{$\mathbf{D}$}^{4,!\times}$). The reasoner checks the consistency of ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\text{\hspace{0.17em}⁣}\times }$-knowledge bases (KBs) represented in set-theoretic terms. It is implemented in $\mathsf{\text{C++}}$ and supports ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\text{\hspace{0.17em}⁣}\times }$-KBs serialized in the OWL/XML format. To the best of our knowledge, this is the first attempt to implement a reasoner for the consistency checking of a description logic represented via a fragment of set theory that can also classify standard OWL ontologies.