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

Abstract

We study the complexity of the combination of the Description Logics AℒCscript Q sign and AℒCscript Q signI with a terminological formalism based on cardinality restrictions on concepts. These combinations can naturally be embedded into C2, 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 AℒCscript Q signI, as AℒCscript Q signI with cardinality restrictions has the same complexity as C2 (NEXPTIME-complete). In contrast, we show that for AℒCscript Q sign, 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 AℒCscript Q sign extended with nominals. Using the same reduction, we show that, for the extension of AℒCscript Q signI with nominals, reasoning with general axioms is a NEXPTIME-complete problem. Finally, we sharpen this result and show that pure concept satisfiability for AℒCscript Q signI with nominals is NEXPTIME-complete. Without nominals, this problem is known to be PSPACE-complete.