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

Domenico Cantone, Marianna Nicolosi-Asmundo, Daniele Francesco Santamaria

We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic $\mathcal{D}\mathcal{L}⟨4LQ{\mathsf{S}}^{\mathsf{R},\times }⟩(\mathbf{D})$, in…