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

Abstract

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 short ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\times }$. The logic ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\times }$, representable in the decidable multi-sorted quantified set-theoretic fragment $4LQ{\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.

Please cite https://www.scopus.com/record/display.uri?eid=2-s2.0-85053216200&origin=resultslist. arXiv admin note: substantial text overlap with arXiv:1702.03096