The Complexity of Reasoning with Cardinality Restrictions and Nominals in Expressive Description Logics

TL;DR

This paper analyzes the computational complexity of reasoning in expressive description logics with cardinality restrictions and nominals, establishing optimal complexity bounds for various logic combinations.

Contribution

It provides a detailed complexity analysis of ALCQ and ALCQI with cardinality restrictions and nominals, including reductions to known logical fragments and complexity classifications.

Findings

ALCQ with cardinality restrictions is ExpTime-complete.

ALCQI with cardinality restrictions is NExpTime-complete.

Reasoning with nominals increases complexity to NExpTime.

Abstract

We study the complexity of the combination of the Description Logics ALCQ and ALCQI with a terminological formalism based on cardinality restrictions on concepts. These combinations can naturally be embedded into C^2, the two variable fragment of predicate logic with counting quantifiers, which yields decidability in NExpTime. We show that this approach leads to an optimal solution for ALCQI, as ALCQI with cardinality restrictions has the same complexity as C^2 (NExpTime-complete). In contrast, we show that for ALCQ, the problem can be solved in ExpTime. This result is obtained by a reduction of reasoning with cardinality restrictions to reasoning with the (in general weaker) terminological formalism of general axioms for ALCQ extended with nominals. Using the same reduction, we show that, for the extension of ALCQI with nominals, reasoning with general axioms is a NExpTime-complete problem. Finally, we sharpen this result and show that pure concept satisfiability for ALCQI with nominals is NExpTime-complete. Without nominals, this problem is known to be PSpace-complete.