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

TL;DR

This paper introduces a KE-tableau-based reasoner for a decidable set-theoretic fragment of description logic, enabling reasoning tasks like consistency checking and conjunctive query answering with enhanced features.

Contribution

It presents an optimized, C++ implementation of a reasoner for $ ext{DL}_{ ext{D}}^{4, imes}$, extending previous prototypes and supporting OWL/XML and SWRL rules.

Findings

Successfully solves TBox and ABox reasoning problems.

Supports conjunctive queries with multiple variable sorts.

Implemented in C++ with compatibility for OWL/XML and SWRL.

Abstract

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short). Our application solves the main TBox and ABox reasoning problems for $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. In particular, it solves the consistency problem for $\mathcal{DL}_{\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{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases (see \cite{cilc17}), is implemented in \textsf{C++}. It supports $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases serialized in the OWL/XML format, and it admits also rules expressed in SWRL (Semantic Web Rule Language).