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

TL;DR

This paper introduces a set-theoretic approach to ABox reasoning in a highly expressive description logic, proving decidability and providing a extsc{KE} calculus for reasoning tasks involving complex queries and data types.

Contribution

It extends a extsc{KE} based decision procedure to handle a very expressive description logic with rule-based language features, ensuring decidability of ABox reasoning services.

Findings

Decidability of ABox reasoning services for $ ext{DL}_{ ext{D}}^{4, imes}$.

A extsc{KE} calculus for higher order conjunctive query answering.

Extension of previous decision procedures to more expressive logic.

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.