A set-theoretical approach for ABox reasoning services (Extended Version)

TL;DR

The paper addresses decidability and practical reasoning for expressive ABox tasks in the description logic $DL_D^{4,\times}$ by reducing ABox reasoning to satisfiability in the set-theoretic fragment $4LQS^R$ and introducing Higher Order Conjunctive Query Answering (HOCQA). It develops a KE-tableau–based procedure to compute HO answers, mapping DL knowledge bases to $4LQS^R$ formulae via a $\theta$ translation and proving correctness, completeness, and termination. The main contributions include a decidability result for HOCQA in $DL_D^{4,\times}$, an effective HOCQA algorithm, and a complexity analysis, with a clearer EXPTIME bound in restricted settings. This framework enables rich ABox reasoning with data types and rule-like constructs while preserving decidability and paves the way for implementation and future extensions of the underlying set-theoretic fragments.

Abstract

In this paper we consider the most common ABox reasoning services for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment \flqsr. The description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ is very expressive, as it admits various concept and role constructs, and data types, that allow one to represent rule-based languages such as SWRL. Decidability results are achieved by defining a generalization of the conjunctive query answering problem, called HOCQA (Higher Order Conjunctive Query Answering), that can be instantiated to the most wide\-spread ABox reasoning tasks. We also present a \ke\space based procedure for calculating the answer set from $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ knowledge bases and higher order $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ conjunctive queries, thus providing means for reasoning on several well-known ABox reasoning tasks. Our calculus extends a previously introduced \ke\space based decision procedure for the CQA problem.

Figures (1)

• Figure 1: Expansion rules for the KE-tableau.

Theorems & Definitions (16)

• lemma 1
• theorem 1
• proof
• lemma 2
• proof
• lemma 3
• proof
• theorem 2
• proof
• theorem 3