Worst-Case Optimal Querying of Very Expressive Description Logics with Path Expressions and Succinct Counting

1 Introduction

Recent years have seen a convergence of the fields of logicbased knowledge representation (KR) and databases, with querying over knowledge bases (KBs, aka ontologies) as the archetypical inferencing task considered. Thereby, the query languages of interest have evolved from plain conjunctive queries to more expressive formalisms with path-navigational components such as the positive two-way regular path queries (P2RPQs) considered here. One popular and practically used way of specifying the to-be-queried knowledge bases is via description logics (DLs), whose most expressive exemplars feature advanced constructors for roles and path expressions. Certainly, the DLs from the Z family [Calvanese et al., 2009] are among the most powerful KR formalisms on the verge of decidability. For its most expressive proponent, ZOIQ, featuring nominals (O), role inverses (I), and number restrictions (Q), querying is undecidable [Ortiz et al., 2010; Rudolph, 2016] and even decidability of KB satisfiability is open, owing to the intricate interplay of the three mentioned features, but restricting the interaction of O, I, and Q (or excluding one of the features altogether) leads to beneficial model-theoretic properties, which give rise to upper bounds of EXPTIME for KB satisfiability and 2EXPTIME for querying, established using elaborate automata techniques [Calvanese et al., 2009]. While the first bound holds under the assumption of binary encoding of number restrictions, the proof for the second one requires unary encoding.

∗Work supported by "Diamentowy Grant" no. DI2017 006447 and by ERC Consolidator Grant 771779 (DeciGUT).

In our paper, we overcome this restriction. Leveraging said model-theoretic property of the considered DLs, we provide a novel reduction from the query entailment problem K |= q to the problem of checking unsatisfiability of some other knowledge base K¬q. Thereby, the size of the latter is exponential in the total size of q and K (even when assuming binary encoding), leading to a 2EXPTIME-complete complexity. Our technique also yields the new insight that the complexity drops to EXPTIME, when the number of atoms in q is bounded by a constant. The obtained results allow to correspondingly improve a number of previous results on query containment and can be transferred to DLs from the SR family.

Reaching out to the community researching decidable fragments of first-order logic, we show that our results also extend to entailment of P2RPQs by GC 2 databases, i.e. sets of unary and binary ground facts in the presence of a sentence of the guarded two-variable fragment with counting as defined by Pratt-Hartmann (2007).

2 Preliminaries

Description Logics

We will briefly recap syntax and semantics of the very expressive DL ZOIQ and its relevant sublogics following Calvanese et al. (2009). We assume a fixed signature consisting of sets NI of individual names, NC of concept names, and NR of role names. We let NC contain the special concept names ⊤ and ⊥, and NR the special role names ⊤ and ⊥. The following EBNF grammar defines atomic concepts B, concepts C, atomic roles R, simple roles S and roles T , with o, a, b ∈ NI, A ∈ NC, P ∈ NR \ {⊤}:

An assertion is of the form C(a), R(a, b), a ≈ b, or a ̸≈ b, a general concept inclusion (GCI) has the form C1 ⊑ C2. We use C1 ≡ C2 as abbreviation for C1 ⊑ C2, C2 ⊑ C1. A ZOIQ knowledge base (short: KB) K = (A, T ) consists of a finite set A (called ABox) of assertions and a finite set T (called TBox) of GCIs.

The semantics of ZOIQ is defined via interpretations I = (∆I , ·I ) composed of a non-empty set ∆I called the domain of I and a function ·I mapping individual names to elements of ∆I , concept names to subsets of ∆I , and role names to subsets of ∆I ×∆I . This mapping is extended to concepts, simple roles, and roles (cf. Table 1) and finally used to define satisfaction of assertions and GCIs (see Table 2). We say that an interpretation I satisfies a KB K = (A, T ) (or I is a model of K, written: I |= K) if it satisfies all axioms of A and T . K is called satisfiable if it has a model and unsatisfiable otherwise. From ZOIQ, we obtain ZIQ by disallowing nominal concepts {o}, ZOQ, by disallowing role inverses (.)- and ZOI by disallowing number restrictions.

Queries

We use variables from a countably infinite set V. A Boolean positive two-way regular path query (P2RPQ) is an expression q = ∃⃗x.ϕ, where ϕ is a positive formula (i.e., one using ∧ and ∨) over expressions T(s, t) or C(t), where T is a role, C is concept, and s and t are from ⃗x∪NI. A P2RPQ is a conjunctive two-way regular path query (C2RPQ) if it does not use disjunction. It is a union of conjunctive two-way regular path queries (UC2RPQ) if it is a disjunction of C2RPQs. 1 A (variable) assignment Z for I is a mapping V → ∆I . For x ∈ V, we set xI,Z := Z(x); for c ∈ NI, we set cI,Z := cI . T(s, t) evaluates to true under Z and I if (sI,Z , tI,Z ) ∈ T I . C(t) evaluates to true under Z and I if tI,Z ∈ C I . A P2RPQ q = ∃⃗x.ϕ is satisfied by I (written: I |= q) if there is an assignment Z (called match) such that ϕ evaluates to true under I and Z. A P2RPQ q is entailed by a KB K (written: K |= q) if every model of K satisfies q. If q uses only signature elements of K, we call it a query over K.

Simplifications

A P2RPQ is simplified if all its atoms are of the form T(x, y) where x and y are variables and T is built from role names using ∪, ◦, and ∗ . For any KB K and P2RPQ q, we can construct in polynomial time a KB K′ and simplified P2RPQ q′ such that K |= q iff K′ |= q′ . This justifies that from here on, we will focus on simplified queries.

Automata

For each atom T(x, y) of a simplified P2RPQ, T is a regular expression over NR. Every such expression can be represented by a nondeterministic finite automaton A = (Σ,Q, I, F, T) with an alphabet Σ ⊆ {P, P - |P ∈NR} of possibly inverted role names, a finite set Q of states, initial states I ⊆ Q, final states F ⊆ Q, and transitions T ⊆ Q × Σ × Q. 2 The size of A is polynomially bounded by T. In the following, we assume queries in automaton form, where the atoms T (x, y) have been replaced by the corresponding A(x, y). Given A = (Σ,Q, I, F, T), let A- = (Σ-,Q, F, I, T-) with Σ- = {P - | P ∈ Σ} be the corresponding reverse automaton 3 with initial and final states swapped and the state transitions flipped: (q′ ,R-, q) ∈ Tfor every (q,R, q′ ) ∈ T. Moreover, we obtain the automaton Aq,q′ = (Σ, Q, {q}, {q′ }, T) from A by setting the initial state to q and the final state to q′ .

3 A Little Bit of Model Theory

The "well-behavedness" of certain sublogics of ZOIQ can be conveniently characterised in model-theoretic terms.

Definition 1 (quasi-forest model, Calvanese et al., 2007) Let K be a KB. A model I of K is a quasi-forest model if:

• the domain ∆I of I is a forest, i.e., a prefix-closed subset of Roots × N∗ for some finite set Roots,
• Roots = {oI | o is an individual name in K}, and
• for every δ, δ′ ∈ ∆I with (δ, δ′ ) ∈ P I for some role name P ∈ NR \ {⊤}, either (i) {δ, δ′ } ∩ Roots ̸= ∅, or (ii) δ = δ′ , or (iii) δ is a child of δ′ , or (iv) δ′ is a child of δ.

A KB K has the quasi-forest model property (short: qfmp) if K is either unsatisfiable or it has a quasi-forest model. A DL L has the qfmp if every L KB K has the qfmp.

For such well-behaved KBs, tight and quite decent complexity bounds for satisfiability checking have been established.

1 Note that ∃⃗x. ∨i ϕi ≡ ∨i ∃⃗x.ϕi, so the order of disjunction and existential quantification is irrelevant.

2 The correspondence is such that (δ, δ′ ) ∈ T I iff there is a role path δ P1 --→ · · · Pk --→ δ′ in I such that A accepts P1 . . . Pk.

3 For convenience, we consider (P -)- identical to P.

Theorem 1 (Calvanese et al., 2009) Satisfiability checking of ZOIQ KBs having the qfmp is EXPTIME-complete even with binary encoding of number restrictions.

When it comes to query answering, a useful notion for relating interpretations to each other is via homomorphisms. For two interpretations I = (∆I , ·I ) and J = (∆J , ·J ), a function h : ∆I →∆J is a homomorphism from I to J if for all δ, δ′ ∈ ∆I we have δ ∈ AI ⇒ h(δ) ∈ AJ for all concept names A, and (δ, δ′ ) ∈ P I ⇒ (h(δ), h(δ′ )) ∈ P J for all role names P. If a homomorphism from I to J exists, we write I ▷ J . We note that I |= q and I ▷ J imply J |= q for every simplified P2RPQ q.

Definition 2 (qfhcp, Bourhis et al., 2014) A KB K has the quasi-forest homomorphism-cover property (short: qfhcp) if for every model I of K, there exists a quasi-forest model J of K with J ▷ I. A description logic L has the qfhcp if every L KB K has the qfhcp. We let tame ZOIQ denote the set of all ZOIQ KBs having the qfhcp.

Obviously, the qfhcp implies the qfmp. Note that unrestricted ZOIQ does not even have the qfmp. The most expressive syntactically defined sublogics of tame ZOIQ known today are ZIQ, ZOQ, and ZOI [Calvanese et al., 2009; Bonatti et al., 2008].

From the fact that the set of models for any P2RPQ is closed under homomorphisms now follows that for any tame ZOIQ KB with K ̸|= q, there must exist a quasi-forest model I, satisfying I |= K and I ̸|= q.

4 Annotating (Partial) QueryMatches

In the following, we consider a tame ZOIQ KB K and a simplified P2RPQ q over K in automaton form. We note that q can be rewritten into an equivalent disjunction ∨1≤i≤n qi of n (also simplified) C2RPQs, where n may be exponential in the size of q, but every single qi's size is polynomial. Let [q] denote {q1, . . . qn}. Then, testing K ̸|= q amounts to determining if K has a model I which is a simultaneous countermodel (i.e., I ̸|= qi) for all qi ∈ [q].

We now give an intuitive description of our technique to detect (or refute) matches of q. Given some model I of K, we iteratively, deterministically annotate all its domain elements δ with fresh concept names QM that indicate which "parts" M of some query qi match into I and how δ participates in these partial matches. To this end, we employ descriptions M of query parts which contain information about (i) the query variables matched (ii) (the existence of) paths realising certain state transitions in the query's automata and (iii) optionally, the "position" of the current δ in the query match by use of a marker · acting like an additional, distinguished query variable. In the annotation process, the QMs will be assigned to domain elements δ based on their local environment and known annotations QM′ for "smaller" partial queries to the same element δ or its direct (role) neighborhood. As an exception, non-localised query matches M not containing · will be "broadcast", i.e., uniformly attached to all domain elements. This way, in the annotation process, QMs for larger and larger partial queries are assigned, until finally (after reaching the unique fixpoint) also the full matches for any qi are recognised by annotations Qqi . This process will accurately detect partial and full query matches, if I is a quasi-forest model (which is sufficient for our purposes as K has the qfhcp). The annotation process is realised by virtue of a KB Kq, the size of which is exponential in q, but only polynomial in K. In the following, we will stepwise introduce the KB, interleaved with some necessary definitions.

Definition 3 (partial query) Consider some C2RPQ qi = {A1(x1, y1), . . . ,Am(xm, ym)}. 4 A partial query for qi and a set X ⊆ {x1, y1, . . . , xm, ym} of variables from qi is a set M consisting of

• all atoms A(x, y) from qi for which {x, y} ⊆ X,
• for every A(x, y) from qi with x ∈ X but y ̸∈ X, one of the atoms Aq,q′ (x, ·) or Aq,q′ (x, o) where q is initial in A,
• for every A(x, y) from qi with x ̸∈ X but y ∈ X, one of the atoms A-q,q′ (y, ·) or A-q,q′ (y, o) where q is final in A,
• in case X = ∅, exactly one atom of the form Aq,q′ (·, o) or A-q,q′(·, o) (called nominal-anchored path) or Aq,q′(·, ·) or A-q,q′ (·, ·) (called round trip) for some A from qi.

A partial query is called monodic, if |X| = 1. A partial query is called local if it contains · and global otherwise.

Nominal-Anchored Paths

First, we want to detect role paths that start in the to-beannotated individual, end in named individual oI , and realise state transitions in one of the query's automata. Let o be any individual name in K, let A± be either A or A- for any automaton A occurring in q with states q, q′ , q′′ . Then let Kq contain the axiom

and whenever A± has a transition (q, R, q′ ):

Round Trips

Next, we are concerned with paths which start and end in the to-be-annotated individual. Assuming an automaton A with states q, q′ , q′′ , q′′′ and transition set T as well as an individual name o, we add the axioms:

Initialising monodic partial queries

Next we determine domain elements to which separate query variables could possibly be mapped in a match.

Definition 4 We call a monodic partial query M original, if q = q′ for every Aq,q′ (x, ·) ∈ M and every A-q,q′ (x, ·) ∈ M. For M an original monodic partial query for q and {x}, the set PrecM of precondition concepts consists of:

4 In cases, we may equate a C2RPQ qi with the set of its atoms.

• Q{A q,q′ (·,o)} for each atom Aq,q′ (x, o) in M,
• Q{A-q,q′ (·,o)} for each atom A-q,q′ (x, o) in M,
• ⊔ q initial q′ final Q{A q,q′ (·,·)} for each atom A(x, x) in M.

Now we can initialise all original monodic partial queries M by adding the following axioms to Kq:

Updating partial queries

Partial queries can be updated by roundtrips: Let M be a partial query containing some A±q,q′(x, ·). Then we realise the update by adding the following axioms to Kq:

Furthermore, a partial query can "progress" when making a "step" in the model, moving from the considered δ to some role neighbour. In such a step, all the "unready" paths (corresponding to atoms with ·) must be updated in a synchronous manner. Given a partial query M for qi and nonempty X as well as a set {R1, . . . , Rk} of (possibly inverted) role names, assume M ′ can be obtained from M by replacing each atom of the form A±q,q′ (x, ·) by an atom A±q,q′′ (x, ·) such that A± has a transition (q′ ,R, q′′ ) for any R ∈ {R1, . . . ,Rk}. Then add the following axiom to the KB Kq:

Joining partial queries

When two partial queries corresponding to the same query qi "meet" in a domain element δ, they can - under certain circumstances - be "glued together" into a "bigger" partial query of qi.

Definition 5 (joinable, join) Let M1 be a partial query for qi and X1 and let M2 be a partial query for qi and X2. We call M1 and M2 joinable if

• X1 ̸= ∅, X2 ̸= ∅, X1 ∩ X2 = ∅, and
• for each A(x, y) ∈ qi \ (M1∪M2) with {x, y} ⊆X1∪X2, there are states q, q′ , q′′ of A with q initial and q′′ final,
• such that either {Aq,q′ (x, ·), A-q′′ ,q′ (y, ·)} ∈ M1∪M2 or {Aq,q′ (x, o), A-q′′ ,q′ (y, o)} ∈ M1 ∪ M2 for some o ∈ NI. For joinable M1 and M2, their join, denoted M1 ▷◁ M2, is the partial query obtained from M1 ∪M2 by replacing any pair of atoms Aq,q′ (x, ∗) and A-q′′ ,q′ (y, ∗) by A(x, y), where

∗ is either an individual name o or ·.

We implement the join operation for every pair M1, M2 of joinable partial queries for a qi ∈ [q] by extending Kq with:

Broadcasting global partial queries

Whenever a partial query M does not have any occurrences of ·, which would tie it to a specific element, it will be "broadcast" to all domain elements:

This concludes the definition of Kq. Revisiting our initial intuition of Kq's purpose of deterministically annotating a model I of K, the following lemma formalises this by singling out one unique annotated model I ∗ for every I.

Lemma 2 Let K be a ZOIQ KB and q a simplified P2RPQ. For every model I of K there exists a unique model I ∗ of K ∪ Kq which extends I and satisfies QI ∗ M ⊆ QJM for every QM in Kq and for every model J of K ∪Kq that extends I.

We will call models I ∗ from Lemma 2 Q-minimal. Note that for every model I of K, any concept membership δ ∈ QI ∗ M holding in the corresponding Q-minimal model I ∗ can be derived from concept and role memberships in I through a finite sequence of "applications" of axioms from Kq. 5

5 Reduction to Satisfiability

Now we establish technical results relating the presence of QM-annotations in models and the actual semantic satisfaction of the corresponding partial query M. Note that any partial query M can be seen as a (set representation of a) C2RPQ in automaton form, assuming · is just an ordinary variable.

Definition 6 ((tight) satisfaction of a partial query) Given an interpretation I, a domain element δ ∈ ∆I , and a partial query M, we say M is satisfied or holds in δ, written I, δ |=M, if there is a match Z for M in I with Z(·) = δ. M is satisfied or holds tightly in δ, written I, δ |=|=M, if Z is such that every A±q1,q2 (x, ·) ∈ M is realized by a path Z(x) ❀ δ not containing oI for any individual name o.

Note that |= and |=|= coincide whenever M is global or does not contain variables. Note also that, as a consequence of this definition, if M is global, then QM holds (tightly) everywhere or nowhere throughout the domain. With this notion in place, the next two lemmas can be seen as soundness and completeness results regarding the deduction calculus for (partial) query matches embodied by Kq.

Lemma 3 (soundness) Let I be a Q-minimal model of K ∪ Kq and let δ ∈ ∆I . Let M be any partial query for any C2RPQ qi ∈ [q]. Then δ ∈ QIM implies I, δ |= M.

Lemma 4 (completeness) Let I be a quasi-forest model of K ∪ Kq and let δ ∈ ∆I . Let M be any partial query for any C2RPQ qi ∈ [q]. Then I, δ |=|=M implies δ ∈ QIM .

Soundness is proven by induction over the length of the derivation for δ ∈ QIM . Completeness is shown by induction over the spread of the match for M, i.e., the number of variables (excluding ·) plus the sum of the lengths of all paths realising the query atoms.

Thanks to these correspondences, we can essentially rule out models with matches of any q1, . . . , qn by forcing the extensions of Qq1 , . . . ,Qqn to be empty. Therefore, let

We establish some syntactic and semantic properties of K¬q: Some easy calculations yield size bounds for K¬q, tameness is not affected by the reduction, and unsatisfiability of K¬q indeed coincides with query entailment.

Fact 5 (size of K¬q) The size of K¬q is single exponential in the total size of K and q. It is polynomial, if the number of atoms in q is bounded by a constant.

5 To see this, it may help to realise that all axioms of Kq can be easily expressed in monadic Datalog.

Lemma 6 If K is in tame ZOIQ then so is K¬q.

Proof. First note that K¬q is in ZOIQ. For tameness, consider a model I of K¬q. As I is a model of K and the latter is tame, there exists a quasi-forest model J of K and a homomorphism h : J → I. Now, we can construct a quasiforest model J ′ of K¬q by extending J , letting δ ∈ QJ ′ M if h(δ) ∈ QIM for all QM occurring in K. □

Theorem 7 Let K be a tame ZOIQ KB and let q be a simplified P2RPQ over K. Then K |= q if and only if K¬q is unsatisfiable.

Proof. For convenience, we show the equivalent statement: K ̸|= q if and only if K¬q satisfiable.

"only if": Assume K ̸|= q, that is there exists an I with I |= K and I ̸|= q. Consider I ∗ , the Q-minimal model of K∪Kq extending I. If some QI ∗ qi were nonempty, then there would be a query match of q into I by Lemma 3, contradicting our assumption. Therefore, I ∗ |= Qqi ⊑ ⊥ for all qi ∈ [q] and hence, I ∗ |= K¬q.

"if": Assume K¬q is satisfiable and hence has a model I. As K¬q has the qfmp thanks to Lemma 6, we can assume I to be a quasi-forest model. I |= Qqi ⊑ ⊥ implies emptiness of QIqi for every qi ∈ [q]. If I |= q held true, witnessed by I |= qi for some qi ∈ [q], Lemma 4 would require δ ∈ QIqi for all δ ∈ ∆I , leading to a contradiction. Hence I ̸|= q. On the other hand, I |= K¬q implies I |= K, therefore K ̸|= q. □

Based on this theorem, we can now prove our central result:

Theorem 8 The problem of checking entailment of simplified P2RPQs from tame ZOIQ KBs with binary number encoding is 2EXPTIME-complete. It is EXPTIME-complete if the number of atoms in the query is bounded.

Proof. By Theorem 7, entailment of a simplified C2RPQ q from a tame ZOIQ KB K can be reduced to checking unsatisfiability of K¬q, which can be computed in output-polynomial time and the size of which is exponential (polynomial, if number of atoms in q is bounded). By Theorem 1, (un)satisfiability of K¬q can be checked in EXPTIME in the size of K¬q, hence we obtain the desired 2EXPTIME and EXPTIME upper bounds. The matching lower bounds are well-known even for much weaker logics [Ortiz and Simkus, 2012]. □

6 Querying GC 2 Databases

We now consider the problem of P2RPQ entailment from GC 2 databases, i.e., sets of unary and binary ground facts in the presence of a sentence in the guarded two-variable fragment with counting quantifiers as defined by PrattHartmann (2007). We will show that there is a polytime query-entailment-preserving transformation from GC 2 databases to ZIQ KBs. This allows us to transfer the results from Theorem 8. Matching lower bounds follow from known results for much weaker logics and query formalisms (such as CQs over ALCI [Lutz, 2008]).

Definition 7 (GC 2 ; Pratt-Hartmann, 2007) For a signature S of nullary (N0), unary (NC), and binary (NR ∪ {≈})

predicates, 6 let GC 2 be the smallest set of formulae that contains all atoms over S using only variables from {x, y}, that is closed under Boolean combinations, and that contains

• all formulae ∃u.ϕ and ∀u.ϕ with u ∈ {x, y} whenever ϕ is a GC 2 formula with at most one free variable, and
• all formulae ∀u.(γ → ϕ) as well as Q u.(γ ∧ ϕ) and Q u.(γ) where γ is a binary atom (called "guard") containing both x and y, ϕ is a GC 2 formula, and Q is any of ∃, ∃⩽n, ∃=n, or ∃⩾n.

A GC 2 database DB is a theory {Φ} ∪ A consisting of a GC 2 sentence Φ and a finite set A of unary and binary ground facts over constants fromNI. 7 We denote by GC 2qef the set of GC 2 formulae which are quantifier-free and do not use ≈.

A P2RPQ over a GC 2 database is a P2RPQ where for every atom of the form C(t) holds C ∈ NC and for every atom of the form T(s, t), every subexpression of the form id(C) satisfies C ∈ NC. P2RPQ entailment from GC 2 databases is defined in the same way as for DLs.

For convenience, we make use of a special normal form for GC 2 introduced in the following.

Lemma 9 (normal form; Pratt-Hartmann, 2009) For any GC 2 sentence Φ, one can compute in polynomial time a GC 2 sentence NF(Φ) of the form

with α ∈ GC 2qef not using y, {E1, ... , Eℓ, F1, ... , Fm} ⊆ NR, {β1, ... , βℓ} ⊆ GC 2qef , and {n1, ... , nm} ⊆ N, such that (i) NF(Φ) |= Φ and (ii) every model of Φ with at least maxh nh elements can be extended to a model of NF(Φ).

Given a GC 2 database DB = {Φ} ∪ A, we let NF(DB) = {NF(Φ)} ∪A. Thanks to the previous lemma and the known property that models of GC 2 sentences are closed under disjoint self-union, the normal form can be shown to be queryentailment-preserving.

Lemma 10 For every P2RPQ q over a GC 2 database DB holds DB |= q if and only if NF(DB) |= q.

We next provide a query-entailment-preserving polynomial translation of GC 2 databases into ZIQ KBs.

Definition 8 Let Ψ be a GC 2 sentence in normal form as in Lemma 9. We define the ZIQ TBox TΨ by

where (introducing fresh concept names PropP and role names R≈ and REh,at):

6 As unary and binary predicates correspond to concept and role names, respectively, we use the same set symbols to denote them.

7 Note that ABoxes, as defined before, are syntactically and semantically identical to finite sets of unary and binary ground facts, so we consider the notions the same and use the same symbol A. Note also that by definition, Φ does not contain constants.

• T≈ = {⊤ ⊑ ⩽1R≈.⊤, ⊤ ⊑ ∃R≈.Self}
• Tps = {PropP ≡ ∃⊤.PropP | P ∈ N0}
• Tα = {⊤ ⊑ tr(α)}, where

where axEh maps atoms in βh to sets of GCIs as follows:

and trEh maps GC 2qef formulae to simple roles:

Given a GC 2 database DB = {Φ}∪A, we let KDB denote the ZIQ KB (TNF(Φ), A).

Intuitively, T≈ axiomatises equality, Tps introduces synchronised concept names PropP for every propositional symbol P from DB, since ZIQ does not allow for nullary predicates. Tα, TEh,βh , and TFi,ni implement the conjuncts fromNF(Φ).

Lemma 11 Let DB = {Φ} ∪A be a GC 2 database. Then the following hold:

1. KDB can be computed in polytime wrt. the size of DB.
2. KDB has the qfhcp.
3. Any model of KDB can be extended to one of NF(DB).
4. Any model of NF(DB) can be extended to one of KDB.
5. For any P2RPQ q over DB holds DB |= q iff KDB |= q.

Proof. Point 1 is obvious from the given translation. Point 2 is a direct consequence from the fact that KDB is a ZIQ KB.

For Point 3, we have to extend the model I by interpretations for all P ∈ N0: we map P to true exactly if PropP = ∆I . For Point 4, we have to extend the model I by interpretations for all PropP , R≈, and REh,at: we let PropIP = ∆I if P holds true in I and PropIP = ∅ otherwise; we let RI≈ = {(δ, δ) | δ ∈ ∆}; and we let RIEh,at = {(Z(x),Z(y)) | I,Z |= Eh(x, y) ∧ at}. Point 5 can be shown in two steps: by Lemma 10, the queries entailed by DB and by NF(DB) coincide. Then, as a consequence of the fact that by Point 3 and Point 4, the model sets of NF(DB) and KDB coincide on all unary and binary predicates occurring in DB, hence also the entailed queries coincide. □

Theorem 12 P2RPQ entailment from GC 2 databases is 2EXPTIME-complete. It is EXPTIME-complete if the number of query atoms is bounded by a constant.

Proof. Given a GC 2 database DB and a P2RPQ q over DB, we can compute KDB in polynomial time, and it is of polynomial size by Lemma 11, Point 1. Moreover, DB |= q can be checked by testing KDB |= q by Lemma 11, Point 5, which in turn can be checked in doubly exponential time (singly exponential if q is bounded) by Theorem 8, since KDB has the qfhcp by Lemma 11, Point 2. □

7 Conclusion

We have established tight complexity bounds for expressive querying in very expressive DLs under the assumption of succinct (i.e. binary) encoding of number restrictions. Arguing along the lines of Calvanese et al. (2009), we can leverage our findings to strengthen their results on query containment as well as the SR family as follows: 8

Theorem 13 (query containment) Testing query entailment K |= q′ ⊆ q is in 2EXPTIME with respect to the total size of q′ , q, and K (with binary encoding of number restrictions) if (i) K is in ZOQ or ZOI and q′ and q are P2RPQs over K, or (ii) K is in ZIQ, q′ is a conjunctive query and q is a P2RPQ over K. The complexity drops to EXPTIME if the number of atoms occurring in q is bounded by a constant.

Theorem 14 (SR family) Deciding K |= q and K |= q′ ⊆ q is in 3EXPTIME in the total size of q′ , q, K (with binary encoding of numbers) - and in 2EXPTIME if K's RBox is given by defining regular expressions for the non-simple roles - if (i) K is in SROQ or SROI and q′ , q are P2RPQs over K, or (ii) K is in SRIQ, q′ is a CQ and q is a P2RPQ over K. The complexities are in 2EXPTIME and in EXPTIME, respectively, if the number of atoms in q is bounded by a constant.

There are plenty of open questions left for future work. First, the results established here hold for arbitrary models, however, so far, very little is known about finite (model) query answering in DLs from the Z family. Second, while the extension of our query formalism by nestings in the sense of Bienvenu et al. (2014) seems straightforward without impacting complexities, our technique seems not readily extendable to capture more elaborate query languages [Rudolph and Kr¨otzsch, 2013; Bourhis et al., 2015; Reutter et al., 2017].

8 For space reasons, we have to assume the reader to be familiar with the notions used in these theorems.