=Paper=
{{Paper
|id=Vol-2954/abstract-4
|storemode=property
|title=Finite-Controllability of Conjunctive Queries in the Z family of Description Logics (Extended Abstract)
|pdfUrl=https://ceur-ws.org/Vol-2954/abstract-4.pdf
|volume=Vol-2954
|authors=Bartosz Bednarczyk,Emanuel Kieroński
|dblpUrl=https://dblp.org/rec/conf/dlog/BednarczykK21
}}
==Finite-Controllability of Conjunctive Queries in the Z family of Description Logics (Extended Abstract)==
https://ceur-ws.org/Vol-2954/abstract-4.pdf
Finite-Controllability of Conjunctive Queries in
the Z family of Description Logics
(Extended Abstract)?
Bartosz Bednarczyk1,2 B and Emanuel Kieroński2 B
1
Computational Logic Group, Technische Universität Dresden, Germany
2
Institute of Computer Science, University of Wrocław, Poland
{bartosz.bednarczyk, emanuel.kieronski}@cs.uni.wroc.pl
The description logics (DLs) from the Z family [3] are among the most powerful
KR formalisms on the verge of decidability [7,2]. For brevity we assume that
TBoxes of ZIQ, ZOI and ZOQ are in a normal form. A normal form TBox
can be computed from an original TBox in polynomial time and is a conjunction
of concept definitions of the following form:
A ≡ {o}, A ≡ ¬B, A ≡ B t B0 , A ≡ >ns.B, A ≡ ∃pA .B, A ≡ ∃s.Self
where A, B, B0 are concept names, s is a simple role, o is an individual name
and pA is a so-called automaton role with A being an NFA. Simple roles s are
generated by the following grammar: s ::= r | s ∩ s | s ∪ s | s \ s, where r is an
atomic role or the inverse of an atomic role. Automaton roles are interpreted in
a natural way, e.g. d ∈ (∃pA .B)I , if there is an element in BI and a path leading
to it from d ∈ ∆I that is accepted by A. In ZIQ, ZOQ we exclude, respectively,
nominals and inverse roles, and in ZOI we assume that n = 1.
Important computational problems, like the knowledge-base satisfiability prob-
lem (KBSAT) and the query entailment problem (QEnt), for ZIQ/ZOQ/ZOI
are well understood. They are ExpTime-complete [4] and 2ExpTime-complete,
respectively, even for the class of positive regular two-way queries [4,2]. Surpris-
ingly, in stark contrast with those results, nearly nothing is known about the
behaviour of the Z family of DLs in the finite-world scenario. The only result that
we are aware of is a quite recent proof of the finite model property of ZOI from [4].
Thus, starting a quest for understanding the finite model reasoning in the Z fam-
ily, we investigate the decidability/complexity of KBSAT and QEnt for the class
of local queries, i.e. for conjunctive queries (CQs) and unions thereof (UCQs).
Let K be a ZOI/ZOQ knowledge base and let q be a UCQ. If there exists
an interpretation I satisfying K but not q, we say that I is a countermodel
for K and q. A description logic is called finitely-UCQ-controllable if for all its
knowledge bases and UCQs, if there is a countermodel for them there is also a
finite one. Our main technical result is:
Theorem 1. ZOI and ZOQ are finitely-UCQ-controllable.
?
Conference version of this paper is under submission.
Copyright ©2021 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
2 Bartosz Bednarczyk, Emanuel Kieroński
This yields also the finite model property of ZOQ and ZOI, thus complementing
the results of [4]. Harvesting from the complexity results of [3,2] we conclude:
Corollary 2. Finite knowledge-base satisfiability problem for ZOI and ZOQ is
ExpTime-complete, while their finite CQ/UCQ query entailment is 2ExpTime-
complete.
Roughly speaking, our proof method is as follows. We start from an infinite
forest-shaped finite branching countermodel I for a ZOI/ZOQ knowledge base
and a query q (with K atoms), on which we can additionally assume that whether
an element requires a witness for some existential restriction, then such a witness
is always reachable by a path going downward the forest. Next, we identify in I
the set of all possible downward types π, i.e. the isomorphism types of subtrees
of depth K rooted at some element from I. For every downward type π we select
one representative, extend it by providing witnesses for ∃pA .B requirements of
its root (note that a path accepted by A is finite by definition) and make such
a substructure sibling- and parent closed. Its domain is denoted with ∆π . Such
modified representatives are called components: they serve as the main building
blocks in the construction of a finite countermodel for K and q. For technical
reasons we distinguish nominal types and components, i.e. the ones whose roots
are roots of I.
Let L be the maximal number of leaves across all the components and let
M be the maximal number of children of a node in I. The domain of our finite
countermodel J is:
[ [ 0
∆J := ∆π ∪ ∆ππ,`,m
,b
,
nominal components π non-nominal components π
where decorated ∆π are just disjoint copies of ∆π , π 0 ranges over nominal types,
1≤`≤L, 1≤m≤M and b ∈ {0, 1}. For every π, π 0 , `, m, b as above, we make
π 0 ,b 0
Dπ,`,m := J ∆ππ,`,m
,b
isomorphic to the corresponding component from I and
similarly Dπ := J ∆π for nominal components. What remains to be done is to
define roles between different components of J . For every component, its leaves
are connected to the roots of other components, in order to provide the leaves
π 0 ,1−b
their local witnesses. For every π the root of Dπ,`,m will serve as the m-th child
of the `-th leaf of any of the components Dπ∗,b
0 ,∗,∗ , or, in the case when b = 1 and
π 0 is nominal, of the component Dπ0 . This finishes the construction of J .
It can be shown that J indeed preserves the given knowledge base satisfiability
and the query. For the former task it is very convenient that we use automaton
roles instead of regular expressions which are used in the original definition of
the logics from Z. For the latter it is important that our building blocks are of
depth at least K.
For the logic ZIQ, for which the finite and unrestricted KBSAT do not
coincide (see e.g. [1, Theorem 3.19] for a much weaker logic), we provide an
exponential time reduction from finite conjunctive query entailment to its finite
KBSAT. This is optimal, modulo the conjecture that finite KBSAT for ZIQ is
ExpTime-complete, which is quite probable. Unfortunately, we were not able
Finite-Controllability of CQs in the Z family of DLs (Extended Abstract) 3
to prove this conjecture and even show the decidability of ZIQ TBoxes. This is
probably due to the fact that the decidability results for logics with inverses and
counting are usually obtained via integer programming, which does not seem to
be suitable for dealing with regular expressions.
The main idea of our reduction is to produce, from an input interpretation,
an equivalent interpretation of high “girth”, so for the query it locally looks like
a tree. For simplicity, the construction is presented in the ABox-free setting, but
its slightly more complicated version works with ABoxes.
Theorem 3. The finite conjunctive query entailment problem over L TBoxes,
where L is any fragment ZIQ extending ALCI ∩
Self , can be reduced in exponential
time to its finite TBox satisfiability.
The above theorem can be applied, e.g. to infer the decidability of finite CQ
entailment for ALCHIF extended with transitive closure of roles, see: [6].
For the future work we plan to take a closer look at the finite KBSAT for ZIQ
and try to establish some results on finite entailment of non-local querying for
the Z family. A good idea to start with seems to be to consider transitive-closure
enriched conjunctive queries, as done in [5].
Acknowledgements
Bartosz Bednarczyk is supported by the European Research Council through the
Consolidator Grant No. 771779 (DeciGUT). Emanuel Kieroński was supported
by the Polish National Science Centre grant 2018/31/B/ST6/03662.
References
1. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic.
Cambridge University Press (2017). https://doi.org/10.1017/9781139025355
2. Bednarczyk, B., Rudolph, S.: Worst-Case Optimal Querying of Very Expressive
Description Logics with Path Expressions and Succinct Counting. IJCAI 2019 (2019)
3. Calvanese, D., Eiter, T., Ortiz, M.: Regular Path Queries in Expressive Description
Logics with Nominals. IJCAI 2009 (2009)
4. Calvanese, D., Ortiz, M., Simkus, M.: Verification of Evolving Graph-structured Data
under Expressive Path Constraints. In: ICDT 2016 (2016)
5. Gogacz, T., Gutiérrez-Basulto, V., Gutowski, A., Ibáñez-García, Y., Murlak, F.: On
Finite Entailment of Non-Local Queries in Description Logics. In: KR 2020 (2020)
6. Jung, J.C., Lutz, C., Zeume, T.: On the Decidability of Expressive Description Logics
with Transitive Closure and Regular Role Expressions. In: KR 2020 (2020)
7. Rudolph, S.: Undecidability Results for Database-Inspired Reasoning Problems in
Very Expressive Description Logics. In: KR 2016 (2016)