Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Version)

TL;DR

The paper investigates the decidability and exact complexity of reasoning in the highly expressive Description Logic $ALCOSCC(\mathfrak{D})$, which combines counting (via $\mathsf{succ}$-restrictions) with concrete domain reasoning, under nominals. It shows that, when the concrete domain $\mathfrak{D}$ is ExpTime-$\omega$-admissible and its CSP is ExpTime, consistency is ExpTime-complete, matching the baseline complexity of $ALC$, and that certain natural extensions (tightening the interaction between concrete domains and number restrictions, adding transitivity, etc.) render the logic undecidable. The central contribution is a type-elimination algorithm that constructs augmented types and Venn-bags to encode CD-restrictions within a finite, decidable framework, achieving the ExpTime upper bound. The work also discusses how feature assertions, constants, and predicate assertions can be simulated or reduced, and outlines avenues for implementation and further study (e.g., inverse roles, tableaux approaches). Overall, the results delineate a sharp boundary between decidability and undecidability for DLs with concrete domains and counting under various interactions, with practical implications for knowledge representation in domains requiring quantitative and numerical constraints.

Abstract

Standard Description Logics (DLs) can encode quantitative aspects of an application domain through either number restrictions, which constrain the number of individuals that are in a certain relationship with an individual, or concrete domains, which can be used to assign concrete values to individuals using so-called features. These two mechanisms have been extended towards very expressive DLs, for which reasoning nevertheless remains decidable. Number restrictions have been generalized to more powerful comparisons of sets of role successors in $\mathcal{ALCSCC}$, while the comparison of feature values of different individuals in $\mathcal{ALC}(\mathfrak{D})$ has been studied in the context of $ω$-admissible concrete domains $\mathfrak{D}$. In this paper, we combine both formalisms and investigate the complexity of reasoning in the thus obtained DL $\mathcal{ALCOSCC}(\mathfrak{D})$, which additionally includes the ability to refer to specific individuals by name. We show that, in spite of its high expressivity, the consistency problem for this DL is ExpTime-complete, assuming that the constraint satisfaction problem of $\mathfrak{D}$ is also decidable in exponential time. It is thus not higher than the complexity of the basic DL $\mathcal{ALC}$. At the same time, we show that many natural extensions to this DL, including a tighter integration of the concrete domain and number restrictions, lead to undecidability.

Theorems & Definitions (6)

• definition thmcounterdefinition
• lemma thmcounterlemma: Baad17
• theorem thmcountertheorem
• proof
• definition thmcounterdefinition
• definition thmcounterdefinition