A set-theoretic approach to ABox reasoning services

t. In this paper we consider the most common ABox reasoning services for the description logic DL4LQSR,× (D) (DL4,× D , for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment 4LQSR. The description logic DL4,× D 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 widespread ABox reasoning tasks. We also present a KE-tableau based procedure for calculating the answer set from DL4,× D knowledge bases and higher order DL4,× D conjunctive queries, thus providing means for reasoning on several well-known ABox reasoning tasks. Our calculus extends a previously introduced KE-tableau based decision procedure for the CQA problem.