While query answering with Description Logics (DLs) is now well-developed, this is
much less the case for reasoning services that support ontology engineering and target
query answering as an application. In ontology versioning, for example, one would
like to know whether two versions of an ontology give the same answers to all queries
formulated over a given vocabulary of interest, which means that they can be safely
replaced in an application [
If the data is not known or changes frequently, it is not KBs that should be compared,
but TBoxes. Given a pair = ( 1; 2) specifying a relevant signature 1 for ABoxes
and 2 for queries, we say that a TBox T1 -Q-entails a TBox T2 if, for every
1ABox A, the KB (T1; A) 2-Q-entails (T2; A). T1 and T2 are -Q-inseparable if
they -Q-entail each other. Applications include data-oriented TBox versioning, TBox
modularization and TBox forgetting [
Most important choices for Q are conjunctive queries (CQs) and unions thereof
(UCQs); we also consider the practically relevant classes of rooted CQs (rCQs) and
UCQs (rUCQs), in which every variable is connected to an answer variable. So far,
CQentailment has been studied for Horn DL KBs [
This paper makes a first breakthrough into understanding query entailment and
inseparability in these cases, with the main results summarized in Figures 1 and 2 (those
marked with (?) are from [
ALC to ALC undecidable
? undecidable 2EXPTIME
ALC to Horn-ALC ?
Queries
CQ UCQ 2EXPTIME =EXPTIME(?) rCQ rUCQ
ALC to ALC undecidable
? undecidable ?
ALC to
Horn-ALC
?
=2EXPTIME
=EXPTIME =EXPTIME
decidability of subsumption-based entailment between ALC TBoxes [
Undecidability of CQ-Entailment for ALC KBs Here we sketch the construction showing that the problem whether an E L KB -CQ entails an ALC KB is undecidable. The proof is by reduction of the undecidable N M tiling problem: given a finite set T of tile types T with four colours up(T ), down(T ), left(T ) and right(T ), a tile type I 2 T, and two colours W (for wall) and C (for ceiling), decide whether there exist N; M 2 N such that the N M grid can be tiled using T in such a way that (1; 1) is covered by a tile of type I; every (N; i), for i M , is covered by a tile of type T with right(T ) = W ; and every (i; M ), for i N , is covered by a tile of type T with up(T ) = C. Given an instance of this problem, we first describe a KB K2 = (T2; fA(a)g) that uses (among others) three concept names Tk, k = 0; 1; 2, for each tile type T 2 T. If a point x in a model I of K2 is in Tk and right(T ) = left(T 0), then x has an R-successor in Tk0 . Thus, branches of I define (possibly infinite) horizontal rows of tilings with T. If a branch contains a point y 2 Tk with right(T ) = W , then this y can be the last point in the row, which is indicated by an R-successor z 2 Row of y. In turn, z has R-successors in all T(k+1) mod 3 that can be possible beginnings of the next row of tiles. To coordinate the up and down colours between the rows—which will be done by the CQs separating K1 and K2— we make every x 2 Tk, starting from the second row, an instance of all T(0k 1) mod 3 with down(T ) = up(T 0). The row started by z 2 Row can be the last one in the tiling, in which case we require that each of its tiles T has up(T ) = C. After the point in Row indicating the end of the final row, we add an R-successor in End for the end of tiling. The beginning of the first row is indicated by a P -successor in Start of the ABox element a, after which we add an R-successor in I0 for the given initial tile type I; see the lowest branch in the figure below. To generate a tree with all possible branches described above, we only require E L axioms of the form E v D and E v 9S:D. hl T0 SRtoawrt
T0
T0 T1
Row T0N1 Start IT01.1.2.
T1
Row ∨ T2End
T1
Row
Row
T1 TNM-1 T0N1M-2... RowIl End Row EndT2 ∨ T2 hr
Row Ir T21M
T11M-1...
T1NT2MN-M1... End
The existence of a tiling of some N M grid for the given instance can be checked by Boolean CQs qn that require an R-path from Start to End going through Tk- or Row-points: 9x(Start(x0) ^ Vn
i=0 R(xi; xi+1) ^ Vin=1 Bi(xi) ^ End(xn+1)), where Bi 2 fRowg [ fTk j T 2 T; k = 0; 1; 2g. The key trick is—using an axiom of the form D v E t E0—to ensure that the Row-point before the final row of the tiling has two alternative continuations: one as described above, and the other one having just a single R-successor in End where _ indicates an or-node. This or-node gives two models of K2 denoted Il and Ir in the picture. If K2 j= qn, then qn holds in both of tahnedmh,ra(nxdnso1)thaerree ianrsetahnocmesomofoBrpnhis1m,swhel h:aqvne !BnIl1 a=nd ThNr:Mqn ! Ir. As hl(xn 1) 1 1 in the picture, and so up(T NM 1) = down(T NM ). By repeating this argument until x0, we see that the colours between horizontal rows match and the rows are of the same length. (For this trick to work, we have to make the first Row-point in every branch an instance of Start.) In fact, an instance of the N M -tiling problem has a positive answer iff there exists qn such that K2 j= qn. It is to be noted that to construct T2 with the properties described above, one needs quite a few auxiliary concept names.
Let K1 = (T1; fA(a)g) be an E L KB with the following canonical model:
Start; 0 Start; 0 Start; 0 a A
P
End; 0 End; 0 End; 0 End; 0 End; 0 End; 0 where 0 = fRowg [ fTk j T 2 T; k = 0; 1; 2g. Note that the vertical R-successors of the Start-points are not instances of any concept name, and so K1 does not satisfy any query of the form qn. On the other hand, K2 j= q implies K1 j= q, for every -CQ q without a subquery of the form qn and = sig(K1). Therefore, K1 -CQ entails K2 iff there exists no tiling as specified above. 3
We have made first steps towards understanding query entailment and inseparability for KBs and TBoxes in expressive DLs. From a theoretical viewpoint, it would be of interest to solve the open problems in Figures 1 and 2, and also consider other expressive DLs such as DL-LitebHool or ALCI. For example, our undecidability proof goes through for DL-LitebHool , but the other cases remain open. From a practical viewpoint, our modeltheoretic criteria for query entailment are a good starting point for developing algorithms for approximations of query entailment based on simulations. Our undecidability and complexity results also indicate that rUCQ-entailment is more amenable to practical algorithms than, say, CQ-entailment and can be used as an approximation of the latter.