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

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Toggle side column

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

Bartosz BednarczykBartosz Bednarczyk,  Franz BaaderFranz Baader,  Sebastian RudolphSebastian Rudolph
Bartosz Bednarczyk, Franz Baader, Sebastian Rudolph
Satisfiability Checking and Conjunctive Query Answering in Description Logics with Global and Local Cardinality Constraints
Technical Report, Computational Logic Group, 2019
  • 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 Logic
@techreport{BBR2019,
  author      = {Bartosz Bednarczyk and Franz Baader 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}
}