=Paper=
{{Paper
|id=Vol-2373/paper-47
|storemode=property
|title=On Finite and Unrestricted Query Entailment beyond SQ with Number Restrictions on Transitive Roles
|pdfUrl=https://ceur-ws.org/Vol-2373/paper-47.pdf
|volume=Vol-2373
|authors=Tomasz Gogacz,Víctor Gutiérrez Basulto,Yazmín Ibáñez-García,Jean Christoph Jung,Filip Murlak
|dblpUrl=https://dblp.org/rec/conf/dlog/GogaczGIJM19
}}
==On Finite and Unrestricted Query Entailment beyond SQ with Number Restrictions on Transitive Roles==
https://ceur-ws.org/Vol-2373/paper-47.pdf
On Finite and Unrestricted Query Entailment
beyond SQ with Number Restrictions on
Transitive Roles?
Tomasz Gogacz1 , Vı́ctor Gutiérrez-Basulto2 , Yazmı́n Ibáñez-Garcı́a2 ,
Jean Christoph Jung3 , and Filip Murlak1
University of Warsaw1 Cardiff University2 Universität Bremen3
We study query entailment in extensions of the description logic (DL) SQ allow-
ing number restrictions (Q) to be applied to transitive roles (S). Most previous
work on query entailment in expressive DLs, such as SHIQ or SHOQ, forbid
the interaction of number restrictions and transitive roles [2–4], but it is required
in areas like biomedicine, e.g., to restrict the number of certain parts an organ
has. For instance, one can express that the human heart has exactly one mitral
valve, which has to be shared by its left and right atrium [5]. Allowing for the
interaction of S and Q is dangerous in the sense that even modest extensions of
SQ, such as with role inclusions or inverse roles, lead to an undecidable satisfi-
ability problem [6]. Decidability of satisfiability in SQ and in its extension with
nominals was shown several years ago [6, 7], but only recently tight computa-
tional complexity bounds were established [8]. Even more recently, decidability
for entailment of regular path queries over SQ knowledge bases was established.
More precisely, based on a novel tree-like model property of SQ it was possible to
devise an automata-based decision procedure yielding a tight 2ExpTime upper
bound [5].
The objective of our investigation is to paint a more complete picture of
query entailment in DLs with number restrictions on transitive roles. We pursue
the following two specific goals.
1. We aim at understanding the limits of decidability of query entailment for
such DLs. To this end, we investigate the extensions of SQ by nominals
(SOQ) and controlled inverse roles (SIQ9 ), where we allow number re-
strictions on inverse non-transitive roles and only existential restrictions on
inverse transitive roles. As query language, we consider positive existential
regular path queries, thus capturing the common languages of conjunctive
queries and regular path queries.
2. We initiate the study of finite query entailment for SIQ9 and SOQ, where
one is interested in reasoning only over finite models. This distinction is
crucial because in database applications, both database instances and the
models they represent are commonly assumed to be finite. The study of
?
Accepted at IJCAI 2019 [1]. Gogacz and Murlak were funded by Poland’s National
Science Centre grant 2018/30/E/ST6/00042, Ibáñez-Garcı́a by ERC Starting grant
637277 FLEXILOG and Jung by ERC Consolidator grant 647289 CODA. This work
was partially funded by the OeAD WTZ project PL 15/2017.
finite query entailment in SQ is interesting since, due to the presence of
transitivity, SQ lacks finite controllability, and therefore unrestricted and
finite entailment do not coincide. Interestingly, most previous works on fi-
nite query entailment consider logics lacking finite controllability because of
number restrictions and inverse roles [9–12]. The study of finite query entail-
ment in logics with transitivity (without number restrictions on transitive
roles) started only recently [13–15]. Here, we focus on finite entailment of
positive existential queries in SOQ and of instance queries in SIQ9 .
Contributions. We start by showing a tree-like model property for both SOQ
and SIQ9 . More specifically, we carefully extend and adapt the canonical tree
decompositions that were introduced for SQ in previous work [5] to also incor-
porate the presence of controlled inverses and nominals. Next, we prove that if
a query is not entailed by a knowledge base (KB), then there is a counter-model
with a canonical tree decomposition of small width. This tree-like model prop-
erty is the basis for automata-based approaches to unrestricted and finite query
entailment in the remainder of the paper. First, we construct tree automata to
optimally decide entailment of regular path queries over SOQ and SIQ9 KBs in
2ExpTime. We move then to finite entailment of positive existential queries over
SOQ KBs, showing again an optimal 2ExpTime upper bound. To this end, we
look at more refined canonical tree decompositions, which ensure the existence
of a finite counter model. In other words, we reduce finite query entailment to
entailment over models with this special canonical tree decomposition. Finally,
we investigate the complexity for unrestricted and finite instance query (IQ) en-
tailment in SIQ9 . In particular, we show that IQ entailment is 2ExpTime-hard
both in the finite and in the unrestricted case. We found this surprising since
it is rarely the case that IQ entailment becomes more difficult when inverses
are added to the logic. Moreover, the result provides an orthogonal reason for
2ExpTime-hardness for conjunctive query entailment in SIQ9 [16]. We comple-
ment this lower bound with a matching upper bound in the unrestricted case,
thus confirming the conjecture that satisfiability in SIQ9 is decidable [6]. In the
finite case, we show a 2ExpTime-upper bound for KBs using a single transi-
tive role. Note that SIQ9 with a single transitive role is a notational variant
of the graded modal logic with converse K4(♦≥ , ♦9 ). Thus, our result entails
2ExpTime-completeness for global consequence in K4(♦≥ , ♦9 ), which was only
known to be decidable [17].
Outlook. This study provides a step towards a complete picture of query en-
tailment in DLs with number restrictions on transitive roles. There are several
natural next steps involving finite entailment. For SIQ9 the first thing to do
is to cover the full logic; the second thing is to go beyond instance queries. In
general, it would be interesting to study data complexity and consider transitive
closure instead of transitivity.
References
1. Gogacz, T., Gutiérrez-Basulto, V., Ibáñez-Garcı́a, Y., Jung, J.C., Murlak, F.: On
finite and unrestricted query entailment beyond SQ with number restrictions on
transitive roles. In: Proc. of IJCAI-19. (2019)
2. Glimm, B., Lutz, C., Horrocks, I., Sattler, U.: Conjunctive query answering for
the description logic SHIQ. J. Artif. Intell. Res. (JAIR) 31 (2008) 157–204
3. Glimm, B., Horrocks, I., Sattler, U.: Unions of conjunctive queries in SHOQ. In:
Proc. of KR-08. (2008) 252–262
4. Calvanese, D., Eiter, T., Ortiz, M.: Answering regular path queries in expressive
description logics via alternating tree-automata. Inf. Comput. 237 (2014) 12–55
5. Gutiérrez-Basulto, V., Ibáñez-Garcı́a, Y., Jung, J.C.: Answering regular path
queries over sq ontologies. In: Proc. of AAAI-18, AAAI Press (2018)
6. Kazakov, Y., Sattler, U., Zolin, E.: How many legs do I have? Non-simple roles in
number restrictions revisited. In: Proc. of LPAR-07. (2007) 303–317
7. Kaminski, M., Smolka, G.: Terminating tableaux for SOQ with number restrictions
on transitive roles. In: Proc. of the 6th IFIP TC. (2010) 213–228
8. Gutiérrez-Basulto, V., Ibáñez-Garcı́a, Y., Jung, J.C.: Number restrictions on tran-
sitive roles in description logics with nominals. In: Proc. of AAAI-17. (2017)
9. Rosati, R.: Finite model reasoning in dl-lite. In: Proc. of ESWC-19. (2008) 215–229
10. Pratt-Hartmann, I.: Data-complexity of the two-variable fragment with counting
quantifiers. Inf. Comput. 207(8) (2009) 867–888
11. Ibáñez-Garcı́a, Y., Lutz, C., Schneider, T.: Finite model reasoning in horn descrip-
tion logics. In: Proc. of KR-14. (2014)
12. Amarilli, A., Benedikt, M.: Finite open-world query answering with number re-
strictions. In: LICS-15. (2015) 305–316
13. Rudolph, S.: Undecidability results for database-inspired reasoning problems in
very expressive description logics. In: Proc. of KR-16. (2016) 247–257
14. Gogacz, T., Ibáñez-Garcı́a, Y., Murlak, F.: Finite query answering in expressive
description logics with transitive roles. In: Proc. of KR-18. (2018)
15. Danielski, D., Kieronski, E.: Finite satisfiability of unary negation fragment with
transitivity. arXiv:1809.03245 (2018)
16. Lutz, C.: The complexity of conjunctive query answering in expressive description
logics. In: Proceedings of IJCAR 2008. (2008) 179–193
17. Bednarczyk, B., Kieronski, E., Witkowski, P.: On the complexity of graded modal
logics with converse. In: JELIA. Volume 11468 of LNCS. (2019) 642–658