Conjunctive Query Answering via a Fragment of Set Theory (Extended Version)

TL;DR

This paper introduces a set-theoretic approach to conjunctive query answering in an extended description logic, providing a decision procedure and analyzing its computational complexity.

Contribution

It formalizes $lqsr$-based reasoning for $ dlsx$ and develops a decision procedure and a extit{KE}-based method for query answering.

Findings

Decidable reasoning for $ dlsx$ using set-theoretic formulas.

A extit{KE}-based procedure suitable for implementation.

Analysis of the computational complexity of the decision procedure.

Abstract

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