A set-based reasoner for the description logic ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\times }$ (Extended Version)

Abstract

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic $\mathcal{D}\mathcal{L}⟨4LQ{\mathsf{S}}^{\mathsf{R},\times }⟩(\mathbf{D})$ (${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\times }$, for short). Our application solves the main TBox and ABox reasoning problems for ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\times }$. In particular, it solves the consistency problem for ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\times }$-knowledge bases represented in set-theoretic terms, and a generalization of the \emph{Conjunctive Query Answering} problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and optimizes a previous prototype for the consistency checking of ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\times }$-knowledge bases (see \cite{cilc17}), is implemented in \textsf{C++}. It supports ${\mathcal{D}\mathcal{L}}_{\mathbf{D}}^{4,\times }$-knowledge bases serialized in the OWL/XML format, and it admits also rules expressed in SWRL (Semantic Web Rule Language).

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