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

TL;DR

This paper introduces an optimized KE-tableau-based reasoning system for a highly expressive description logic, demonstrating significant performance improvements over existing methods, and advancing the development of efficient OWL ontology reasoners.

Contribution

The paper presents a novel KE$^ extgamma$-tableau system that enhances reasoning efficiency for the logic $ ext{DL}_{ ext{D}}^{4, imes}$, combining rule-based and set-theoretic approaches.

Findings

Reasoner performance up to 400% better than existing systems

First step towards efficient OWL ontology reasoners

Applicable to expressive description logics with set-theoretic foundations

Abstract

We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$, in short $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. The logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, representable in the decidable multi-sorted quantified set-theoretic fragment $\mathsf{4LQS^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.