Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints
This work addresses decidability issues in description logics with mixed cardinality constraints, which is incremental for the knowledge representation and reasoning community.
The paper introduces ALCSCC++, a description logic that mixes global and local cardinality constraints, and shows that while satisfiability checking remains decidable without inverse roles, adding inverse roles makes it undecidable, and conjunctive query entailment is undecidable even without inverse roles, but decidability can be regained by restricting constraints.
We introduce and investigate the expressive description logic (DL) ALCSCC++, in which the global and local cardinality constraints introduced in previous papers can be mixed. On the one hand, we prove that this does not increase the complexity of satisfiability checking and other standard inference problems. On the other hand, the satisfiability problem becomes undecidable if inverse roles are added to the languages. In addition, even without inverse roles, conjunctive query entailment in this DL turns out to be undecidable. We prove that decidability of querying can be regained if global and local constraints are not mixed and the global constraints are appropriately restricted. The latter result is based on a locally-acyclic model construction, and it reduces query entailment to ABox consistency in the restricted setting, i.e., to ABox consistency w.r.t. restricted cardinality constraints in ALCSCC, for which we can show an ExpTime upper bound.