Satisfiability Checking and Conjunctive Query Answering in Description Logics with Global and Local Cardinality Constraints

Franz BaaderFranz Baader, Bartosz BednarczykBartosz Bednarczyk, Sebastian RudolphSebastian Rudolph

Download

Franz Baader, Bartosz Bednarczyk, Sebastian Rudolph
Satisfiability Checking and Conjunctive Query Answering in Description Logics with Global and Local Cardinality Constraints
Technical Report, Computational Logic Group, 2019

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@techreport{BBR2019,
  author      = {Franz Baader and Bartosz Bednarczyk and Sebastian Rudolph},
  title       = {Satisfiability Checking and Conjunctive Query Answering in
                 Description Logics with Global and Local Cardinality
                 Constraints},
  institution = {Computational Logic Group},
  year        = {2019}
}