Table of Contents
Fetching ...

Data Complexity in Expressive Description Logics With Path Expressions

Bartosz Bednarczyk

TL;DR

The paper analyzes data complexity for satisfiability and rooted-query entailment in highly expressive description logics with path constraints, establishing $NP$-completeness for $ZOIQ$-style logics over quasi-forests and $co{NExpTime}$-completeness for rooted CQ entailment. It introduces a modular two-phase approach: (i) precomputing an exponential-in-TBox set of $ZOIQ$-satisfiable substructures to guide model construction, and (ii) NP-guessing a clearing followed by PTIME verification, aided by automata decorations and counting decorations. A key contribution is the notion of elegant quasi-forest models and their summaries, enabling polynomial-size descriptions of clearings and exponential ghost-summaries that preserve the necessary automata and counting information; this yields a practical framework for deciding quasi-forest satisfiability in the data complexity setting and re-proving known results for decidable OWL2 fragments. The results extend to entailment of rooted queries, showing $co{NExpTime}$-completeness, by restricting attention to initial segments with bounded depth and extending them, using the same decoration-driven machinery. Overall, the work provides a principled, automata-based decomposition for reasoning in expressive DLs with regular path expressions, delivering tight complexity bounds and a scalable, modular reasoning blueprint.

Abstract

We investigate the data complexity of the satisfiability problem for the very expressive description logic ZOIQ (a.k.a. ALCHb Self reg OIQ) over quasi-forests and establish its NP-completeness. This completes the data complexity landscape for decidable fragments of ZOIQ, and reproves known results on decidable fragments of OWL2 (SR family). Using the same technique, we establish coNEXPTIME-completeness (w.r.t. the combined complexity) of the entailment problem of rooted queries in ZIQ.

Data Complexity in Expressive Description Logics With Path Expressions

TL;DR

The paper analyzes data complexity for satisfiability and rooted-query entailment in highly expressive description logics with path constraints, establishing -completeness for -style logics over quasi-forests and -completeness for rooted CQ entailment. It introduces a modular two-phase approach: (i) precomputing an exponential-in-TBox set of -satisfiable substructures to guide model construction, and (ii) NP-guessing a clearing followed by PTIME verification, aided by automata decorations and counting decorations. A key contribution is the notion of elegant quasi-forest models and their summaries, enabling polynomial-size descriptions of clearings and exponential ghost-summaries that preserve the necessary automata and counting information; this yields a practical framework for deciding quasi-forest satisfiability in the data complexity setting and re-proving known results for decidable OWL2 fragments. The results extend to entailment of rooted queries, showing -completeness, by restricting attention to initial segments with bounded depth and extending them, using the same decoration-driven machinery. Overall, the work provides a principled, automata-based decomposition for reasoning in expressive DLs with regular path expressions, delivering tight complexity bounds and a scalable, modular reasoning blueprint.

Abstract

We investigate the data complexity of the satisfiability problem for the very expressive description logic ZOIQ (a.k.a. ALCHb Self reg OIQ) over quasi-forests and establish its NP-completeness. This completes the data complexity landscape for decidable fragments of ZOIQ, and reproves known results on decidable fragments of OWL2 (SR family). Using the same technique, we establish coNEXPTIME-completeness (w.r.t. the combined complexity) of the entailment problem of rooted queries in ZIQ.
Paper Structure (10 sections, 25 theorems, 8 equations, 5 figures, 4 tables, 3 algorithms)

This paper contains 10 sections, 25 theorems, 8 equations, 5 figures, 4 tables, 3 algorithms.

Key Result

Lemma 1

Let $\mathcal{K} {\coloneqq} (\mathcal{A}, \mathcal{T})$ be a KB of $\mathcal{ZOQ}$, $\mathcal{ZOI}$, or $\mathcal{ZIQ}$. Then is an integer $\mathrm{N}$ (exponential w.r.t. $|\mathcal{T}|$) such that: (I) $\mathcal{K}$ is satisfiable iff $\mathcal{K}$ has an $\mathrm{N}$-bounded quasi-forest model,

Figures (5)

  • Figure 1: Basic paths and their corresponding decorations in quasi-forests, given in order of their introduction in Def. \ref{['def:basic-paths-in-quasi-forests']}, \ref{['def:A-concepts']}, and \ref{['def:A-roles']}.
  • Figure :
  • Figure :
  • Figure :
  • Figure :

Theorems & Definitions (42)

  • Definition 1
  • Example 1
  • Lemma 1
  • Lemma 2
  • Definition 2
  • Lemma 3
  • Lemma 4
  • Lemma 5
  • Definition 3
  • Lemma 6
  • ...and 32 more