On the Complexity of Counting in Description Logics

Many Description Logics (DLs) allow for counting expressions of various forms that are important in many applications, e.g., for reasoning with semantic data models and for applications concerned with the configuration of technical systems. We present two novel complexity results for DLs that contain counting constructs: (1) We prove that concept satisfiability for ALCQI is decidable in PSPACE even if binary coding of numbers in the input is assumed. (2) We prove that TBox consistency for ALCQI with cardinality restrictions is NEXPTIME-complete