Table of Contents
Fetching ...

Revisiting Conjunctive Query Entailment for $\mathcal S$

Yazmín Ibáñez-García, Jean Christoph Jung, Vincent Michielini, Filip Murlak

TL;DR

The paper settles the complexity of UCQ entailment over knowledge bases formulated in description logic $\mathcal{S}$ by demonstrating $2\mathrm{ExpTime}$-completeness when two transitive roles may occur in queries, even for trivial ABoxes. It also shows $coNExpTime$-completeness for rooted UCQs or when at most one transitive role is used, providing matching upper and lower bounds. The authors develop a small-witness property and a mosaic/tiles framework to transform entailment questions into mosaic existence and to bound tile sizes exponentially, enabling nondeterministic exponential-time decision procedures. The work clarifies how the presence and number of transitive roles fundamentally alter complexity, and it offers a unified three-step approach that integrates ABox elimination, mosaic construction, and size bounds to derive the upper bounds. These results close long-standing gaps and have implications for reasoning tasks in knowledge bases using expressive description logics.

Abstract

We clarify the complexity of answering unions of conjunctive queries over knowledge bases formulated in the description logic $\mathcal S$, the extension of $\mathcal{ALC}$ with transitive roles. Contrary to what existing partial results suggested, we show that the problem is in fact 2ExpTime-complete; hardness already holds in the presence of two transitive roles and for Boolean conjunctive queries. We complement this result by showing that the problem remains in coNExpTime when the input query is rooted or is restricted to use at most one transitive role (but may use arbitrarily many non-transitive roles).

Revisiting Conjunctive Query Entailment for $\mathcal S$

TL;DR

The paper settles the complexity of UCQ entailment over knowledge bases formulated in description logic by demonstrating -completeness when two transitive roles may occur in queries, even for trivial ABoxes. It also shows -completeness for rooted UCQs or when at most one transitive role is used, providing matching upper and lower bounds. The authors develop a small-witness property and a mosaic/tiles framework to transform entailment questions into mosaic existence and to bound tile sizes exponentially, enabling nondeterministic exponential-time decision procedures. The work clarifies how the presence and number of transitive roles fundamentally alter complexity, and it offers a unified three-step approach that integrates ABox elimination, mosaic construction, and size bounds to derive the upper bounds. These results close long-standing gaps and have implications for reasoning tasks in knowledge bases using expressive description logics.

Abstract

We clarify the complexity of answering unions of conjunctive queries over knowledge bases formulated in the description logic , the extension of with transitive roles. Contrary to what existing partial results suggested, we show that the problem is in fact 2ExpTime-complete; hardness already holds in the presence of two transitive roles and for Boolean conjunctive queries. We complement this result by showing that the problem remains in coNExpTime when the input query is rooted or is restricted to use at most one transitive role (but may use arbitrarily many non-transitive roles).

Paper Structure

This paper contains 24 sections, 33 theorems, 18 equations, 8 figures.

Key Result

Theorem 1

UCQ Entailment in $\mathcal{S}$ is 2ExpTime-complete. It is 2ExpTime-hard already for CQs and trivial ABoxes, as long as at least two transitive roles are available.

Figures (8)

  • Figure 1: Encoding runs of alternating Turing machines.
  • Figure 2: Detecting copying errors.
  • Figure 3: Interpretation $\mathcal{J}_a$ in the two cases.
  • Figure 4: A Boolean PTQ over a transitive role $t$ and non-transitive role $s$, its cluster tree, and a query corresponding to its root cluster.
  • Figure 5: A naughty query using transitive roles $s$, $t$.
  • ...and 3 more figures

Theorems & Definitions (60)

  • Theorem 1
  • Theorem 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Lemma 5
  • Theorem 6
  • Theorem 7
  • Theorem 8
  • Definition 9
  • ...and 50 more