We prove co-N2ExpTime-hardness for conjunctive query entailment in the description logic ALCOIF , thus improving the previously known 2ExpTime lower bound. The result transfers to OWL DL and OWL2 DL, of which ALCOIF is an important fragment. A matching upper bound remains open.
Due to its importance for ontology-based data access and data integration, conjunctive query (CQ) answering has developed into one of the most widely studied reasoning tasks in description logic (DL). Nevertheless, the precise complexity (and sometimes even decidability) of CQ answering in several important expressive DLs is still an open problem. In particular, this concerns fragments of the W3C-standardized OWL DL ontology language that comprise nominals, inverse roles, and number restrictions, a combination of expressive means that is notorious for interacting in intricate ways. In this paper, we concentrate on the basic such fragment ALCOIF in which number restrictions take the form of global functionality constraints.
Decidability of CQ answering in ALCOIF and its extension ALCOIQ with
qualified number restrictions has been shown only very recently [
We prove our result by a reduction of the tiling problem that requires to tile a torus
of size 22n 22n . Our construction combines elements of two existing hardness proofs,
but also requires the development of novel ideas. We follow the general strategy of the
proofs that show N2ExpTime-hardness of satisfiability in SROIQ [
An extended technical report including proofs and further details is available [
We assume standard notation for the syntax and semantics of ALCOIF knowledge
bases [
A domino system is a triple D = (T; H; V), where T = f1; : : : ; kg is a finite set of
tiles and H; V T T are horizontal and vertical matching relations. A tiling of m m
for a domino system D with initial condition c0 = ht10; : : : ; tn0i, ti0 2 T for 1 i n, is a
mapping t : f0; : : : ; m 1g f0; : : : ; m 1g ! T such that ht(i; j); t(i + 1 mod m; j)i 2 H,
ht(i; j); t(i; j + 1 mod m)i 2 V, and t(i; 0) = ti0 1 (0 i; j < m). There exists a domino
system D0 for which it is N2ExpTime-complete to decide, given an initial condition c0
of length n, whether D0 admits a tiling of 22n 22n with initial condition c0 [
Conjunctive Query Entailment in ALCOI F Our aim is to construct, for an initial condition c0 of length n, an AnLCOnIF -KB K0 and conjunctive query q0 such that K0 6j= q0 i D0 admits a tiling of 22 22 with initial condition c0.
Intuitively, the models of K0 that we are interested in have the form depicted in Figure 1: a torus of dimension 22n 22n , where the lower left corner is identified by the nominal o, the upper right corner by the nominal e, each horizontal dashed arrow denotes the role h, and each vertical dotted arrow the role v. We will install two counters that identify the vertical and horizontal position of torus nodes. To store the counter values, we use binary trees of (roughly) depth n below the torus nodes, where each 3 Complex concepts C in atoms C(x) are used w.l.o.g.; to eliminate them, we can replace C(x) with AC(x) for a fresh atomic concept AC and add C v AC to the TBox. fog 22n feg
2n of the 2n leaves store one bit of each counter (represented via concept names X and Y). The filled circles in Figure 1 denote true torus nodes, which are labeled by a tile later on, while the unfilled circles denote auxiliary nodes that will help us in properly incrementing the counters. This incrementation is the main di culty of the reduction, and it is achieved with the help of the query q0. As the details are intricate, we defer a discussion of the details until later, and first concentrate on the construction of K0.
The following concept inclusions (1) to (9) of K0 lay the foundation for enforcing
the torus structure with attached trees. Successors in trees are connected via the
composition of the roles r and r, from now on denoted by r ; r. This is needed in the query
construction later on, similar to the use of symmetric roles in [
A1 A2 A1
A1 :A1 :A2 A2 :A1 :A1 :A2
A1 A1 A2
A1 :A1 :A2 A2 :A1 :A1 :A2
L0 L1
L2 concept B u L0 identifies the true torus nodes.
B u L0 u MX u MY v feg
fog v B u L0 B u L0 v 9h:(W u 9r:(H u W u L0) u 9h:(B u L0)) B u L0 v 9v:(W u 9r:(V u W u L0) u 9v:(B u L0))
Li v 9r :9r:(Ai+1 u Li+1) u 9r :9r:(:Ai+1 u Li+1) i<n
Ai u L j v 8r :8r:(L j+1 ! Ai) :Ai u L j v 8r :8r:(L j+1 ! :Ai)
C v 8r:C u 8r :C 1 i j<n 1 i j<n for all C 2 fB; W; H; Vg > v 6 1h :> > v 6 1v :> Note that the concept names A1; : : : ; An implement a binary counter for the leafs of the trees, i.e., for counting the bit positions in the horizontal and vertical counters. In summary, the internal structure of the trees is as shown in Figure 2 where branching tree nodes have dark background and intermediate nodes have light background.
The next step is to make sure that the horizontal and vertical counter have value 0 at the origin and that MX is true at the root of a tree when the horizontal counter has reached the maximum value, and similarly for MY . We use 8(r ; r)n:C to denote the 2nquantifier prefixed 8r :8r: 8r :8r:C. Recall that the concept name X represents the truth value of bits of the horizontal counter, and likewise for Y and the vertical counter.
fog v 8(r ; r)n:(:X u :Y)
Ln v (X $ MX) u (Y $ MY ) Li 1 u 9r :9r:(Li u Ai u MX) u 9r :9r:(Li u :Ai u MX) v MX Li 1 u 9r :9r:(Li u Ai u MY ) u 9r :9r:(Li u :Ai u MY ) v MY 0<i n 0<i n Li 1 u 9r :9r:(Li u :MX) v :MX 0<i n
Li 1 u 9r :9r:(Li u :MY ) v :MY 0<i n The general strategy for updating the horizontal and vertical counter is as follows. We introduce additional concept names X0 and Y0, which represent the truth value of the bits of two additional binary counters, the ‘primed versions’ of the horizontal and vertical counter. Using K0, we ensure that, in black trees, the X-counter has the same value (1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13) (14) (15) as the X0-counter, and likewise for the Y- and Y0-counter. In white trees, we distinguish between horizontal incrementation indicated by the concept name H and vertical incrementation indicated by the concept name V: if the tree satisfies H, then the value of the X0-counter is the value of the X-counter incremented by one, while the values of the Y- and Y0-counter coincide; if the tree satisfies V, it is the other way around. The remaining job to be accomplished by the query q0 is then to ( ) ensure that the value of the X0-counter (resp. Y0-counter) in a (black or white) tree is identical to the value of the X-counter (resp. Y-counter) in its ‘successor trees’, i.e., in trees that can be reached by traveling a single step in the torus along the roles h or v. This behavior of the counters, with the exception of ( ), is implemented by the subsequent concept inclusions. To increment a counter, we use a concept name F to mark the bits that have to be flipped. Another concept name S , which is propagated down from the root to a single leaf, is used to mark the unique bit of the incremented counter such that (i) all bits to the right are flipped from 1 to 0, (ii) the bit itself is flipped from 0 to 1, and (iii) all bits to the left remain unchanged. As a special case, all bits flip when the maximum counter value has been reached. In the following, CIs (16) to (20) implement the proper marking by F and S , CIs (21) to (23) realize the actual incrementation of the X-counter to the X0-counter in (white) H-trees, and CI (24) ensures that the Y- and Y0-counters have the same value in H-trees and in black trees. We also need CIs (21) to (24) with H replaced by V, X by Y, X0 by Y0, Y by X, and Y0 by X0.
L0 u (:MX t :MY ) v S
L0 u (MX u MY ) v F u :S
Li 1 u F u :S v 8r :8r:(Li ! F u :S )
Li 1 u :F u :S v 8r :8r:(Li ! :F u :S ) H u Ln u F u :S v X u :X0
H u Ln u S v :X u X0 H u Ln u :F u :S v (X u X0) t (:X u :X0) (B t H) u Ln v (Y u Y0) t (:Y u :Y0)
Li 1 u S v 8r :8r:[Li ! (Ai u :F u :S ) t (:Ai u S )] t
8r :8r:[Li ! (Ai u S ) t (:Ai u F u :S )]
To enable the construction of a query q0 that enforces ( ), we add a further (single) r ;
rsuccessor to each leaf in each tree. At this extra node, which is marked with the concept
name Ln+1, the truth value of all concept names Ai, X, X0, Y, Y0 is complemented
compared to its predecessor Ln-node. We also introduce a marker concept Q that is true at
the intermediate node between each Ln-node and Ln+1-node. This is similar to what is
done in [
Ln v 9r :(Q u 9r:Ln+1) Ln u C v 8r :8r:(Ln+1 ! :C)
Ln u :C v 8r :8r:(Ln+1 ! C) for all C 2 fA1; : : : ; An; X; X0; Y; Y0g The construction of K0 is not yet finished. However, it will be more convenient to construct the remaining part along with the query q0. The query is assembled from 0<i n 0<i n 0<i n (16) (17) (18) (19) (20) (21) (22) (23) (24) (25) (26) :Ai Q;B v
Ai :Ai Q;B v v
Ai :Ai 1 Ai 1 v Ai 1 :Ai n n n n n n n n v0 Q;W :Ai Ai :Ai
v0 :Ai 1 Ai v0 Q;W 1 v0 Ai 1 :Ai two types of components: counting components and copying components. We start with presenting and explaining a simplified version of counting components, which are then refined in a second step. The final query q0 will contain one counting component for each bit of the counter A1; : : : ; An that counts the leaves of our trees. The simplified version of the counting component for Ai is shown as the topmost cycle in Figure 3, where, for the moment, every arrow should be interpreted as a role atom that uses the role name r. The goal is that matches of this query component should map (i) v to a Q-node of a black tree and v0 to the Q-node of a white successor tree such that the two predecessor Ln-nodes agree on the value of Ai or, symmetrically, (ii) v0 to a Qnode of a white tree and v to the Q-node of a black successor tree such that the two predecessor Ln-nodes agree on the value of Ai. By taking the union of all counting queries for A1; : : : ; An such that the variables v and v0 are shared, we thus link leaves of successor trees that represent the same bit position for the horizontal and vertical counter, which is the first important step towards enforcing ( ).
Due to the Q-concept at v and v0, each variable labeled with Ai or :Ai is matched to an Ln-node or an Ln+1-node. Ignoring the presence of the role names h and v in the torus and pretending that white trees are rooted directly on the torus, each match of the counting component gives rise to one of the two ‘foldings’ presented in Figure 3. These foldings are obtained by identifying variables that are matched to the same domain element, as indicated by the dotted lines. Intuitively, the two foldings correspond to the bit Ai being false (upper folding) and true (lower folding). For brevity, we omit the concept names Q; B; W in the foldings. Since the long sides of the counting component are of length 2n + 1 (counted in terms of compositions r ; r) and trees are of depth n, the two trees involved in a match cannot be further away than one step in the torus. Due to the use of B and W, they cannot be identical.
In the discussion of the simplified counting components above, we have neglected
the presence of the roles h and v in the torus that we need to ‘cross’ when matching
the query in the described way. Refining the counting queries to deal with these roles
is the major challenge in the current reduction, compared to the 2ExpTime lower bound
in [
Note that the meta role is symmetric, like the composition r ; r. The aim is that each meta-role in the refined counting query matches one r ; r-role composition that connects two successor nodes in a tree. To resolve the mismatch between the role composition r ; r of length two and the meta role of length 18, the meta role is designed such that the remaining parts can be folded away into ‘side chains’ that we will add to each tree, i.e., chains of roles that start at each tree node. There are five ways to achieve such a folding, one for each corresponding pair of r - and r-arrows in the left and right half of the meta role. For example, we can use the 3rd r -arrow and the 3rd r-arrow to match the r ; r-composition in the tree, and then have to fold away the prefix composition r ; v; r ; v before the 3rd r -arrow, the infix composition h; r ; h ; r ; r; h; r; h between the 3rd r -arrow and the 3rd r-arrow, and the postfix composition v; r; v ; r following the 3rd r-arrow. Observe that the infix composition is symmetric and thus can be folded into a chain. The postfix composition is the converse of the infix composition, which will allow us to leave a side chain that we have entered with the postfix composition using the prefix composition of the subsequent meta role. Similar foldings allow us to match the r ; r; h; r-compositions required to move up one level in a black tree and then cross via an h-edge to the root of a white successor tree, the r ; h; r ; rcompositions that allows us to cross from the root of a white tree to a black tree and then move down one level, and to perform the two remaining crossing with h replaced by v.
The scheme for adding side chains is shown in Figure 5, where intermediate tree nodes (lower node on the center line) receive di erent chains than branching tree nodes (upper node on the center line). These chains are added to every node in each tree with the exception of the roots of black trees, as those are directly on the torus and adding side chains would violate inverse functionality of h and v. Note that the side chains attached to branching tree nodes are precisely the possible postfix compositions mentioned above, while the side chains attached to intermediate tree nodes are foldings of what we called infix compositions above. The chains are generated by the following CIs, to be added to K0. We use the concept NB = (L0 u W) t F1 i n+1 Li to identify L1 AA12 1
1L0 L0 branching tree nodes and NI = 9r: F1 i n+1 Li to identify intermediate tree nodes.
NB v 9h:9r:9h :9r:9v:9r:9v :9r:> u 9v:9r:9v :9r:> u
9h :9r:9v:9r:9v :9r:> u 9v :9r:> (27) NI v 9v:9r :9v :9r :9h:9r :9h :9r :> u 9h:9r :9h :9r :> u
9v :9r :9h:9r :9h :9r :> u 9h :9r :> (28) In matches of the refined query, the endpoints of the two foldings shown in Figure 3 will match at the end of (possibly empty) side chains at the level n + 1, v and v0 will match at the end of the side chains between the levels n and n + 1, and the adjacent inner nodes labeled with :Ai resp. Ai will match at the end of the side chains at the level n. For this reason, we propagate all relevant concept names to the end of those chains. For C 2 fA1; : : : ; An; :A1; : : : ; :An; X; :X, Y; :Yg, C0 2 fQ; B; Wg, add the concept inclusions (Ln t Ln+1) u C v 8h:8r:8h :8r:8v:8r:8v :8r:C u 8v:8r:8v :8r:C u
8h :8r:8v:8r:8v :8r:C u 8v :8r:C Q u C0 v 8v:8r :8v :8r :8h:8r :8h :8r :C0 u 8h:8r :8h :8r :C0 u
8v :8r :8h:8r :8h :8r :C0 u 8h :8r :C0
We now define counting query parts in a more precise way. Note that each counting query consists of 4n + 4 meta roles. In the subsequent definition, qim; j is a meta role used in the counting query for Ai, where j ranges over 0; : : : ; 4n + 3. (29) (30) Definition 1. For all i, j with 1 i n and 0
j < 4n + 4, put with vi9;0 = v; vi9;2n+2 = v0. The counting query qc for the whole counter is qc := fB(v); Q(v); W(v0); Q(v0)g [ [ qic 1 i n Note that each counting query qic is a cycle as intended since vi;4n+4 = vi0;0. 0
As explained above, the overall counting query qc links a Q-node x1 of a tree to the Q-nodes x2 of its successor trees that represent the same bit position for the horizontal and vertical counters. To establish the central property ( ) in models of K0 that do not match the query q0 to be constructed, it thus remains to modify q0 such that it matches only if the truth assignment at the Ln-predecessor x10 of x1 to X0 and Y0 is not identical to the truth assignment at the Ln-predecessor x20 of x2 to X and Y. This is achieved by the second type of component queries in q0, the copying components.
To prepare for these components, let us distinguish two types of side chains in the tree nodes: the outgoing chains starting with h and v shown to the left in Figure 5 and the incoming chains starting with the inverses of h and v show to the right in Figure 5. As can be seen in Figure 6, when the query has a match, the incoming chains are used in a predecessor tree and the outgoing chains are used in a successor tree. We will distinguish the ends of incoming chains from the ends of the outgoing chains on the levels n and n + 1 using an additional concept P: (Ln t Ln+1) v 8h:8r:8h :8r:8v:8r:8v :8r:P u 8v:8r:8v :8r:P u 8h :8r:8v:8r:8v :8r::P u 8v :8r::P (31) The copying components take the form displayed in Figure 7, i.e., there are 8 such components in total. Each component is like the upper half of a counting component, except that the concept labels have changed to negated conjunctions. In Figure 7, the four copying components in each row take care of each possible truth assignment to X0 and Y0 for the predecessor and the corresponding assignment to X and Y for the successor. We need two queries per truth assignment to deal with the two possible ways in which a counting query can match for the variables v and v0: (a) v matches into a tree that satisfies B, and v0 into a successor tree that satisfies W; (b) v0 matches into a tree that satisfies W, and v into a successor tree that satisfies B; To explain in detail how the copying queries work, consider case (a). Due to the Qlabel in the counting queries, the variables v and v0 can only be matched to Q-nodes. Thus assume that v is matched to a Q-node x1 of a predecessor tree that satisfies B and v0 to a Q-node x2 of a successor tree that satisfies W. The relevant queries are those v v0 v0 v v v0 :(P uX0uY0)
:(:P uXuY) :(P uX0u:Y0) :(:P uXu:Y) :(P u:X0uY0) :(:P u:XuY) :(P u:X0u:Y0) :(:P u:Xu:Y) :(P uX0uY0) :(:P uXuY) :(P uX0u:Y0) :(:P uXu:Y) :(P u:X0uY0) :(:P u:XuY) :(P u:X0u:Y0) :(:P u:Xu:Y) v0 v v v0 v0
v v
v0 from the first row in Figure 7. Let u be the neighboring variable of v in the copying components, and u0 the neighboring variable of v0; thus, both u and u0 are labeled with negated conjunctions. Similar to the situation in Figure 6, u can only be matched to the ends of two outgoing chains (satisfying P): one chain is at level n and another one is at level n + 1. Let us refer to the ends of these chains as x10 and x100 respectively. Likewise, u0 can only be matched to one of the two ends x20 and x200 of incoming chains (satisfying :P) at the levels n and n + 1, respectively.
First assume that the truth assignment at x10 to X0 and Y0 is identical to the truth assignment at x20 to X and Y and thus there should be no match of the overall query q0. Take the corresponding counting component from the first row, e.g., the first one when X0, Y0, X, and Y are all interpreted as true. It can be seen that, in this situation, the matches with u 7! x10 or with u0 7! x20 are not possible because they violate the concept labels of u and respectively u0. The match u 7! x100 and u0 7! x200 is also not possible because the path from u to u0 is not long enough. Thus, there is no match of this component, whence no match of the overall query q0.
Conversely, assume that the truth assignment at x10 to X0 and Y0 is di erent from the truth assignment at x20 to X and Y, e.g., that x10 satisfies X0 but x20 does not satisfy X. Since by (26) the truth values of X0 and X are complemented at the level n + 1, x100 does not satisfy X0 and x200 satisfies X. Then the first two components from the first row have a match u 7! x100 and u0 7! x20 and the next two components have a match u 7! x10 and u0 7! x00. All components in the second row have a match due to the use of the concept 2 name P in the labels (note the swapped v; v0). Thus,the overall query q0 matches.
A formal definition of copying queries can be found in [
This finishes the construction of the query q0 and of the part of K0 that enforces the torus structure. It remains to encode tilings of the domino system D0: > v T1 t
t Tk Ti u 9h:T j v ?
Ti u T j v ? Tk u 9v:T` v ? 1 i < j
k hi; ji < H; hk; `i < V Finally, we enforce the initial condition c0 = ht10; : : : ; tn0i of the torus.
fog v Tt10 u 8h:(Tt20 u 8h:(Tt30 u 8h:(Tt40 u : : : 8h:Ttn0 : : :)))
More details regarding the correctness of the reduction can be found in [
We have shown that conjunctive query entailment in the Description Logic ALCOIF is hard for co-N2ExpTime. The challenging problem of finding a matching upper bound, or in fact any elementary upper bound, remains open.
Acknowledgments B. Glimm is supported by EPSRC grant EP/F065841/1, Y. Kazakov by EPSRC grant EP/G02085X, and C. Lutz by DFG SFB/TR 8 “Spatial Cognition”.