An optimized KE-tableau-based system for reasoning in the description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ (Extended Version)
Domenico Cantone, Marianna Nicolosi-Asmundo, Daniele Francesco Santamaria
TL;DR
This work introduces a KE$^\gamma$-tableau decision procedure for $DL_{D}^{4,×}$, a Description Logic expressed via the decidable set-theoretic fragment $4LQS^R$. By replacing the standard KE-elimination with the $E^{\gamma}$-rule, the method handles universally quantified formulas on-the-fly, eliminating expensive preprocessing and achieving substantial practical speedups (up to ~400%) over prior KE-based and FO KE-tableau implementations. The approach provides a formal correctness and termination guarantee, along with a complexity analysis showing double-exponential behavior in general and EXPTIME under restricted cases, supported by benchmark results. This establishes a viable pathway toward scalable reasoning for expressive OWL ontologies that integrate SWRL-like rules and concrete data types, with planned extensions to data-type solvers and parallel architectures. Overall, the KE$^\gamma$-tableau framework significantly advances the feasibility of applying set-theoretic fragments to practical DL reasoning tasks.
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 $γ$-rule. The novel system, called KE$^γ$-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$^γ$-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.