Conjunctive Query Answering via a Fragment of Set Theory

We address the problem of Conjunctive Query Answering (CQA) for the description logic DLh4LQSR,×i(D) (DL4,× D , for short) which extends the logic DLh4LQSR i(D) with Boolean operations on concrete roles and with the product of concepts. The result is obtained by formalizing DL4,× D -knowledge bases and DL4,× D - conjunctive queries in terms of formulae of the four-level set-theoretic fragment 4LQSR , which admits a restricted form of quantification on variables of the first three levels and on pair terms. We solve the CQA problem for DL4,× D through a decision procedure for the satisfiability problem of 4LQSR . We further define a KE-tableau based procedure for the same problem, more suitable for implementation purposes, and analyze its computational complexity.