Temporal query languages are important for stream processing, and ontologies for stream reasoning. Temporal conjunctive queries (TCQs) have therefore been investigated recently together with description logic ontologies, and the knowledge we have about the combined complexities is rather complete. However, often the size of the queries and the ontology is negligible, and what costs is the data. We prove a new result on the data complexity of ontology-based TCQ answering and close the gap between co-NP and ExpTime for many description logics.
Introduction The temporal nature of data is important in many applications, and the Web offers more and more streaming sources and datasets. Ontologies play an important role in this context: by linking data from heterogeneous sources to the concepts and relations described in an ontology, the integration and automated processing of the data can be considerably enhanced. Queries formulated in the abstract vocabulary of the ontology can then be answered over all the linked datasets.
Medical domain ontologies written in description logics (DLs) may, for example, capture the facts that the varicella zoster virus (VZV) is a virus, that chickenpox is a VZV infection, and that a negative allergy test implies that no allergies are present, by concept inclusions : VZV v Virus; Chickenpox v VZVInfection; NegAllergyTest v :9AllergyTo. Here, Virus is a concept name that represents the set of all viruses, and AllergyTo is a role name, representing a binary relation connecting patients to allergies; 9AllergyTo refers to the domain of this relation. A possible data source storing patient data (e.g., allergy test results and findings) could look as follows:
1 2 3 neg pos neg
16:01:2011 06:01:1970 01:06:2015 PID
Chickenpox 13:08:2007
VZV-Infection 22:01:2010
VZV-Infection 01:11:2011
The data is then connected to the ontology by mappings [
Ontology-based query answering (OBQA) over the above knowledge can
then, for example, assist in finding appropriate participants for a clinical study,
by formulating the eligibility criteria as queries over the—usually linked and
heterogeneous—patient data. The following are examples of in- and exclusion
conditions for a recently proposed clinical trial:1 (i) the patient should have
been previously infected with VZV or previously vaccinated with VZV vaccine;
(ii) the patient should not be allergic to VZV vaccine. We focus on temporal
conjunctive queries (TCQs), which were originally proposed by [
^ : 9y:AllergyTo(x; y) ^ VZVVaccine(y)
We here use the temporal operator “some time in the past” (3P ) and consider
the symbols AllergyTo and VZVVaccine to be rigid, which means that their
interpretation does not change over time; that is, we assume someone having an
allergy to have this allergy for his whole life. The OBQA scenario outlined above
is similar to the classical one [
In contrast, so-called temporal DLs extend classical DLs by temporal
operators, which then occur within the ontology (see [
The combined and data complexity of TCQ entailment have been studied
for various DLs in the past [
In this paper, we first close the co-NP/ExpTime gap for the DL-LitekHrom— which allows for disjunctions as in the example—and prove that TCQ entailment 1 https://clinicaltrials.gov/ct2/show/NCT01953900 2 For some very expressive DLs, we have co-2-NExpTime-hardness/decidability. is in co-NP in data complexity, even with rigid roles. Then, we show that this also holds for much more expressive DLs, such as ALCHI. 2
Preliminaries
Description logics focus on individual names, which are interpreted as constants;
concepts, which are interpreted as sets; and roles, which are interpreted as
binary relations. Accordingly, DL signatures are based on three kinds of symbols:
individual names NI, concept names NC, and role names NR, all of which are
non-empty, pairwise disjoint sets. We focus on the DL DL-LitekHrom [
R; S ::= P j P ;
B; C ::= > j A j 9R;
D ::= B j :B where denotes the inverse role operator.
DL-LitekHrom axioms are the following kinds of expressions: concept inclusions (CIs) are of the form B v C, B v :C, or :B v C; role inclusions (RIs) of the form R v S; and assertions of the form B(a); :B(a); P (a; b); or :P (a; b):
A DL-LitekHrom ontology is a finite set of concept and role inclusions, and an ABox is a finite set of assertions. Together, an ontology O and an ABox A form a knowledge base (KB) K := O [ A, written K = hO; Ai.
We sometimes also refer to the ABox as fact base or simply as the data. Without loss of generality, we assume that, if the RI R v S is contained in O, then we also have 9R v 9S 2 O and 9R v 9S 2 O; and that O contains the trivial axioms 9R v 9R for all roles R occurring in O. The set of roles is denoted by NR . For a given KB K := O [ A, we denote by NI(K) and NI(A) the set of individual names that occur in K and A; by NC(O) and NR(O) the sets of concept and role names occurring in K; and by NR (O) the set of roles occurring in K. B(O) and C(O) denote the sets of all basic concepts and, respectively, concepts that can be built from the symbols in NC(O) and NR (O). We may also use the abbreviation (P ) := P for P 2 NR.
A DL interpretation I = ( I ; I ) consists of a non-empty set I , the domain of I, and an interpretation function I , which assigns to every A 2 NC a set AI I , to every P 2 NR a binary relation P I I I , and to every a 2 NI an element aI 2 I such that, for all a; b 2 NI with a 6= b, we have aI 6= bI (unique name assumption). The function is extended to all roles and concepts: P = f(y; x) j (x; y) 2 P g, >I = I , 9RI = fx 2 I j 9y 2 I ; (x; y) 2 RI g, (:D)I = I n DI . An interpretation I satisfies (or is a model of) an axiom , written I j= , if: = X v Y is a CI or RI, and XI Y I ; = (:)B(a) and aI 2 BI (aI 62 BI ); = (:)P (a; b) and (aI ; bI ) 2 P I ((aI ; bI ) 62 P I ). I satisfies (or is a model of) a KB K, written I j= K, if it satisfies all axioms contained in it. A KB K is consistent (or satisfiable) if it has a model, and it is inconsistent (or unsatisfiable) otherwise. K entails an axiom , written K j= , if all models of K also satisfy . This terminology and notation is extended to (single) axioms, ontologies, and ABoxes by regarding each as a (singleton) KB. We denote non-entailment by K 6j= .
In the temporal setting, we assume that some concept and role names are designated as being rigid (vs. flexible) as outlined in Section 1. If a concept (axiom) contains only rigid symbols, then we may call it a rigid concept (axiom). We denote by NRC NC the rigid concept and by NRR NR the rigid role names. Temporal Semantics. An infinite sequence I = (Ii)i 0 of interpretations Ii = ( ; Ii ) is a DL-LTL structure if it respects rigid names, that is: XIi = XIj for all X 2 NI [ NRC [ NRR and i; j 0: Observe that the interpretations in a DL-LTL structure share one domain (constant domain assumption). We may use that terminology in other settings in that we consider interpretations I1; : : : ; I` to respect rigid names if they agree on the interpretation of all rigid symbols. Temporal Knowledge Bases. A temporal knowledge base (TKB) is of the form K = hO; (Ai)0 i ni with an ontology O and a non-empty, finite sequence of ABoxes. We assume all concept and role names occurring in some ABox of a TKB to also occur in its ontology. NI(K) denotes the set of all individual names occurring in the TKB K. Note that every KB can be regarded as a TKB with an ABox sequence of length one.
A DL-LTL structure I = (Ii)i 0 over a domain is a model of a TKB K = hO; (Ai)0 i ni, written I j= K, if Ii j= O for all i 0 and Ii j= Ai for all i 2 [0; n]. A TKB is consistent (or satisfiable) if it has a model, and it is inconsistent (or unsatisfiable) otherwise.
Temporal Conjunctive Queries. Let NV be the set of variables, and NT := NI[NV be the set of terms. A conjunctive query (CQ) is of the form 9y1; : : : ; ym: , where y1; : : : ; ym 2 NV and is a (possibly empty) finite conjunction of concept atoms of the form A(t) and role atoms of the form R(s; t), where A 2 NC, R 2 NR and s; t 2 NT. The set of temporal conjunctive queries (TCQs) is defined as follows, where ' is a CQ: ; ::= ' j : j ^ j #F j #P j U j S A TCQ is a CQ literal if it is of the form (:)' with ' being a CQ; it is positive if = ', and otherwise negative.
We denote the set of individuals occurring in a TCQ by NI( ). As in propositional LTL, we may use abbreviations true3 and false. The empty conjunction and disjunction are interpreted as true and false, respectively.
As usual, the semantics is defined in a model-theoretic way, based on the notion of homomorphisms. A mapping : NT(') ! I is a homomorphism of a CQ ' into an interpretation I = ( I ; I ) if (a) = aI for all a 2 NI('), (t) 2 AI for all concept atoms A(t) in ', and ( (s); (t)) 2 RI for all role atoms R(s; t) in '. I satisfies (or is a model of) ', written I j= ', if there is such a homomorphism. For a given DL-LTL structure I = (Ii)i 0, an i 0, and TCQ , the satisfaction relation I; i j= is defined by induction on the 3 For instance, true may denote a fix TCQ ' _ :', where ' is an arbitrary CQ.
TCQ 0 CQ ' :
^ #F #P
U S
Condition for I; i j= 0 Ii j= ' W; i 6j= I; i j= and I; i j= I; i + 1 j= i > 0 and I; i 1 j= there is a k i, such that I; k j= and, for all j, i j < k, we have I; j j= there is a k, 0 k i, such that I; k j= and, for all j, k < j i, we have I; j j= structure of as specified in Figure 1. I is a model of w.r.t. a TKB K if I j= K and I; n j= . A TCQ is satisfiable w.r.t. a TKB K if it has a model w.r.t. K; and is entailed by a TKB K, written K j= , if every model of K is also a model of w.r.t. K. We denote the fact that I; i j= and K j= do not hold by I; i 6j= and K 6j= . Observe that a model of a TCQ must satisfy the query at the current time point n, which is different for propositional LTL if n > 0.
Without loss of generality, we assume that the CQs contained in a TCQ use disjoint variables and denote by Q the set of exactly those CQs.4 We further assume that TCQs contain only individual names that occur in the ABoxes, and only concept and role names that occur in the ontology, and that all CQs contained in TCQs are connected (i.e., the corresponding Gaifman graph is connected); it is easy to show that this is without loss of generality. Solving TCQ Satisfiability. The TCQ satisfiability problem can be split into two separate ones: one in propositional LTL and one or several “atemporal” ones in DL [4, Lemma 4.7]. The former tests the satisfiability of the propositional abstraction of the given TCQ at n, which is obtained from by replacing the CQs '1; : : : ; 'm 2 Q by propositional variables p1; : : : ; pm, respectively. The idea is that the worlds w0; w1; : : : in the LTL model characterize the satisfaction of the CQs from Q in the respective DL interpretations I0; I1; : : : such that, to obtain Ii, we only have to check the satisfiability of the conjunction of CQ literals induced by wi w.r.t. the atemporal KB hO; Aii, where Ai = ; for i > n. From the latter it can be seen that, assuming k to be the number of different worlds occurring in the LTL model, it is sufficient to look for n + 1 + k corresponding DL interpretations. More precisely, the problems are linked by a set W = fW1; : : : ; Wkg 2fp1;:::;pmg, which collects all worlds occurring in the LTL model, and a mapping : [0; n] ! [1; k] that maps time points to indexes from W and points out the first n + 1 worlds, which have to reflect the knowledge given in the respective ABoxes. The DL part is defined as r-satisfiability ; the set W is r-satisfiable w.r.t. and a TKB K iff there are interpretations I0; : : : ; In, J1; : : : ; Jk as follows: 4 If the variables were not disjoint, we could simply rename them. – the interpretations share the same domain and respect rigid names, – the interpretations are models of O, – Ji is a model of i := Vpj2Wi 'j ^ Vpj2Wi :'j for all i 2 [1; k], – Ii is a model of Ai and (i) for all i 2 [0; n].
Observe that, regarding data complexity, W and can be guessed in constant and
linear time, respectively. [4, Lem. 4.12] show that the LTL satisfiability problem
w.r.t. a given W and can be decided in polynomial time. However, regarding
r-satisfiability, [
Characterizing r-Satisfiablility We regard a TCQ , a TKB K = hO; (Ai)0 i ni in DL-LitekHrom, a set W 2fp1;:::;pmg such that W = fW1; : : : ; Wkg, and a mapping : [0; n] ! [1; k], as described in the previous section. The goal is to propose a characterization of rsatisfiability of W w.r.t. and K which, in contrast to existing characterizations, is tailored to DL-LitekHrom and shows that the r-satisfiability problem is in NP.
Observe that the functions of the shared domain in the definition of
rsatisfiability are mainly two: (i) to synchronize the interpretation of rigid
symbols regarding the named individuals; (ii) to guarantee that the satisfiability
of the conjunctions i, i 2 [1; k], which is represented by the respective
interpretation Ji, is not contradicted by the interpretation of the rigid names
in the other interpretations, especially in no Ii with i 2 [0; n]. The idea is
to look for similar interpretations I0; : : : ; In; J1; : : : ; Jk; but to not require a
shared domain: based on K, W, and , we specify a polynomial amount of
additional data—that hence can be guessed in polynomial time—, which captures
knowledge restricting the interpretation of the individual and rigid names and
simulates the shared domain; the additional data then allows us to check the
conditions for r-satisfiability for each of the interpretations independently of the
other interpretations—nondeterministically, in polynomial time. Without loss of
generality, we can restrict our focus to certain canonical interpretations, based
on the standard chase [
Definition 1 (Canonical Interpretation). Let K = hO; Ai be a consistent DL-LitekHrom knowledge base. For all A 2 NC and P 2 NR, define: A0 := fa j A(a) 2 Ag; P 0 := f(a; b) j P (a; b) 2 Ag [
f(a; uaP ) j 9P (a) 2 Ag [ f(uaP ; a) j 9P (a) 2 Ag: Then, iterate over all i 0: for all X 2 NC [ NR define Xi+1 := Xi; apply one of the following rules for all A 2 NC, P 2 NR, R; S 2 NR , and B; C 2 B(O); and increment i; (d; e) 2 (P )i denotes the fact that (e; d) 2 P i, and d 2 (9R)i denotes the existence of an element e such that (d; e) 2 Ri: – If B v A 2 O and e 2 Bi, then add e to Ai+1. – If B v 9R 2 O and e 2 Bi: if e 2 NI(A), then add (e; ueR) to Ri+1; if e = u%, then add (e; u%R) to Ri+1. – If 9R v A 2 O, (d; e) 2 Ri, then add d to Ai+1. – If R v S 2 O and (d; e) 2 Ri, then add (d; e) to Si+1. – If :B v C 2 O, e 62 Bi, e 62 Ci, and every other rule (i.e., for a CI without negation) that applies to e or a tuple containing e has been applied in a step j < i, then add e to Bi+1 or Ci+1.
The set uIK collects the above introduced new elements.
A canonical interpretation IK for K is then defined as follows based on such a sequence of rule applications, for all a 2 NI(A), A 2 NC, and P 2 NR: IK := NI(A) [ uIK ; aIK := a;
AIK :=
P IK := 1 [ A ;
i i=0 1 [ P i: i=0 Note that the assumptions in Section 2 about the additional axioms in the ontology ensure that, whenever there is a named individual a 2 (9R)i for some i 0, then a has an R-successor of the form uaR in the corresponding canonical interpretation, and similar for unnamed elements. We denote the restriction of a canonical interpretation I to a named individual a and its unnamed successors by Ija. If K is consistent, then there is a canonical interpretation for K that is a model of K. We denote the set of all those canonical models by IK.
In what follows, we specify the additional data to overtake the Functions
(i) and (ii). Specifically, we define a set of ABoxes containing assertions that
(i) (largely) fix the interpretations on the named individuals (i.e., relations to
unnamed successors are not fully taken into account yet), and (ii) ensure both
that the positive CQ literals are satisfied as required and that the negative CQ
literals are not satisfied if they must not. For simplicity, for i 2 [1; k], we define
An+i := ; and extend such that (n + i) := i. For the synchronization of the
named individuals, we use name-ABoxes, which are similar to the ABox types
defined for DL-LitehHorn in [
Second, for all i 2 [0; n + k], define Qi := f'j j pj 2 W (i)g. Let the set NIaux NI contain an individual name aix for each i 2 [0; n + k] and each variable x occurring in a CQ in Qi. Note that, because of our assumption that the CQs in have no variables in common, each aix 2 NIaux can be unambiguously associated to a CQ containing x. Then, AQi denotes the ABox obtained from Qi by instantiating all variables with the corresponding names from Naux. We use I these ABoxes to ensure that the positive CQ literals are satisfied as required.
While the former is similarly done in [
Definition 3 (Type). A basic type is a set B C(O) such that B 2 B iff :B 62 B for all B 2 B(O); given such a basic type, the corresponding set of assertions is defined as AB(a) := fD(a) j D 2 Bg. The basic type of an individual name a in an interpretation I is the set BT(a; I) := fD 2 C(O) j a 2 DI g.
A type is a triple (B; M; Q) with a basic type B, a set M S'2Q 2NT(') of term sets, and a set Q Q of CQs. The type of an individual name a in a canonical interpretation I is the triple T(a; I) := (BT(a; I); M; Q) where Q Q contains exactly the CQs that are satisfied in Ija, and M contains all sets S of terms for which there are a CQ ' 2 Q and a partial homomorphism : NT(') ! Ija of ' into Ija with a 2 range( ) and dom( ) = S.
A temporal type is a set of types.
We assume every temporal type to be an ordered set and use i to refer to the i-th type in . We denote the set of all temporal types by T.
It is left to specify the prototypical tree ABoxes of unnamed successors for a given temporal type . We first construct ABoxes for the types and, in a second step, ensure that the conditions specified by the types are satisfied in them, respectively. These ABoxes (A i )1 i j j, initially empty, are constructed iteratively, based on canonical interpretations, amongst others for these ABoxes. During the iteration, we therefore assume that these interpretations are (nondeterministically) extended correspondingly (i.e., to cover the new elements of the ABoxes). Let s = j j. For all i 2 [1; s], consider some I i 2 IhO;A i [ABi (b)i; b is a fresh individual name and Bi the basic type in i. Our procedure takes the sequence (I i )1 i s as input. It then repeatedly iterates over the (extended) interpretations and extends the ABoxes (A i )1 i j j until nothing changes any more.
Example 1. We consider an ontology containing the inclusions :A v B; :B v C; A v 9R; C v 9S; R v R0, where only R0 is rigid. Let further j j = 3 and the input canonical interpretations for 1; 2; 3 be as follows.
A R b ubR0 ubR ubR0
C S b
A R A R A R ubS ubR0 ubR ubRR ubRRR A 1 is obtained from I 1 by introducing names representing the unnamed elements, flexible roles get a superscript. All names and the rigid assertions from A 1 are then added to the other ABoxes, and the interpretations I 2 and I 3 are extended correspondingly. The above A 2 is then obtained from this I 2 , Note that all elements that are no instances of A or C instantiate B, R0 is dotted. After one iteration over the interpretations, the ABoxes A i for i 2 [1; 3] are: abR0 abR1
A assumed to be as below. Then, again, all names and rigid assertions from A 2 are added to the other ABoxes, the interpretations are extended, and the above A 3 is obtained from the extended I 3 , depicted below, where c = abR1 .
C S b ubS abR0
abS2 ubR0
R A R A ucRR ucR
b abR1
A R A R A R ubR ubRR ubRRR Note that we do not depict all R0-successors; according to Definition 1, all elements instantiating 9R must have such successors. We lastly show I 1 and I 3 extended for the above A 3 , where d = abR3 , e = abR1R3 , and f = abR3R3 . Observe that we assume that I 3 interprets udR in the same way as ubRR, both udRR and ufR according to ubRRR, and ueR according to ucRR.
abR0
abS2 ubR0
ubR b
R abR1
A R abR3 abR1R3
abR3R3 abR1R3R3 abR3R3R3 abR0
abS2
A R A R A R ucRR ueR
ubR0 R A R A ucR R A
R abR1 abR1R3
In order to ensure that the size of the tree-ABoxes is finite, we specify a termination criterion based on the maximal size m := maxfj'j j ' 2 Q g of a single of the CQs: we stop the introduction of new elements a%%0!R with j%j; j!j > m if those would, thereafter, occur in a subtree (of depth > m) with root a%%0 that would be a copy of an already existing subtree of depth m with root a%. This approach is correct if we extend the ABoxes in a breadth-first fashion and, especially, regard all of the canonical interpretations before extending the trees one level deeper.
We now specify the procedure TreeABox, which takes , the interpretation sequence (I i )1 i s, and b as input: – For each domain element ub%R of I i , introduce an individual name ab%R if R 2 NRR, and otherwise ab%Ri ; we assume that such individual names and role names containing superscripts do not occur in K. Similarly, for each domain element uc%R of I i such that c = ab 2 Ntree, introduce a new I individual name ab %R if R 2 NRR and otherwise ab %Ri .
Let R := NRR [ fRi j R 2 NR n NRR; 1 i sg. The set NItree collects the new individual names, but (*) a name a is only added if there are no names a%, and a in A such that = %%0; = 0 with j 0j > m; and, for all ! 2 Rm, a%! 2 NItree iff a ! 2 NItree, and a%! and a ! have the same basic type in any of the interpretations I ` , ` 2 [1; s]. For the next step, we capture this relation using the function : uI i ! NItree: for the above elements ub%, define (ub%R) := ab%R(i) and, for the others, define (uc%R) := ab %R(i) . Observe that this function may map several elements to the same name; as it is the case for ubRR and udR in Example 1, where we have (ubRR) = abR3R3 and (udR) = abR3R3 . In these cases, we assume that the unnamed successors of elements from Ntree, such as udR, are interpreted in the same way as the
I original unnamed elements, such as ubRR, for which was defined first (i.e., this must have happened when a was introduced, hence udR did not yet exist); and that the successors of the former are interpreted in the same way as the corresponding successors of the latter, and so on. – For every a 2 NItree introduced in the previous step, let u R 2 uI i be one of the elements for which a was created. Add the following assertions to A i : for every B 2 B(O) such that u R 2 BI i , the assertion B(a); for every S 2 NR such that ( ; u R) 2 SI i , the assertion S( ; a); for every S 2 NR such that (u ; u R) 2 SI i , the assertion S( (u ); a). Add all of the individual names and the rigid assertions added to A i also to all other A j , j 2 [1; s].5 – For every a 2 Ntree and B 2 B(O) such that a 2 BI i , further add the
I assertion B(a) to A i . Again, add the rigid assertions to all A j , j 2 [1; s]. The procedure outputs the sequence (A i )1 i s. Regarding the last item, note that it covers those names that were introduced for unnamed elements in other canonical interpretations. For them, we only have to explicitly capture the nondeterminism, w.r.t. basic concepts. All relations on the corresponding named individuals are completely determined by the assertions added in the item before (i.e., including those added in other iteration steps, maybe for some I j with j 6= i). As mentioned above, we second have to ensure that the ABox created for a type also satisfies the conditions specified by it.
Definition 4 (Tree-ABox). An ABox A produced by TreeABox given a name b 2 NI as input is a tree-ABox for a type i = (B; M; Q) if: – hO; A [ AB(b)i is consistent; – for all ' 2 Q , ' 2 Q iff hO; A [ AB(b)i j= '; – for all S 2 S'2Q 2NT('), S 2 M iff there are a CQ ' 2 Q and a partial homomorphism : NT(') ! NI(A) of ' into A with b 2 range( ), S = dom( ). Because of (*), the sizes of the tree-ABoxes are finite, and they are independent of the data: given v := maxfjNT(')j j ' 2 Q g, the maximal number of terms occurring in one of the CQs, and t 2jB(O)j+jQ j+v jQ j, the number of possible types, the depth of how far we specify the prototypical trees is bounded by d := jB(O)jt jNR (O)jt m + m; this follows from the facts that the names in Ntree I 5 All names can be added, for example, by assuming > to be rigid. are built from elements of NR (O), sometimes with subscripts from [1; t], and that we consider these names in t different interpretations.
Finally, the additional data is a tuple as follows, polynomial in the data: ((A0i)0 i n+k; (Ta;i)a2NI(K)[NIaux;; (A ;i) 0 i n+k
2T; ); where 0 i j j – A0i is an name-ABox for NI(K) [ NIaux for all i 2 [0; n + k], and all A0i contain the same rigid assertions; – Ta;i is a type for all a 2 NI(K) [ Naux and i 2 [0; n + k], and Ta(;1i) = BT(a; A0i).
I – (A j )1 j j j is the result of applying TreeABox to , some sequence of corresponding canonical interpretations, and a fresh name b for all 2 T; and A i is a tree-ABox for i for all i 2 [1; j j] if there is a name a 2 NI(K) [ NIaux such that = S0 j n+kfTa;j g.
For names a; b 2 NI and a type i, let A i [b=a] be the ABox obtained from a tree-ABox A i by replacing every b by a, also within individual names. For a tuple t t as above, we define the ABox Atree;i for i 2 [0; n+k] as the set that contains, for all a 2 NI(K)[NIautx, all assertions from A j [b=a], where = fTa;i j 0 i n+kg and j = Ta;i. Atree denotes the ABox that contains only the rigid assertions t from Atree;i, for all i 2 [0; n + k], and all names occurring in these ABoxes6; by construction, all of the latter ABoxes agree on those.
Lemma 1. W is r-satisfiable w.r.t. and K iff there is a tuple t = ((A0i)0 i n+k; (Ta;i)a2NI(K)[NIaux;; (A ) 2T) 0 i n+k as specified above such that, for all i 2 [0; n + k]:
t (C1) KRi := hO; A0i [ Ai [ AQ (i) [ Atree;ii is consistent and,
i (C2) for all pj 2 W (i), we have KR 6j= 'j .
Proof. ()) As outlined in Section 2, we can consider the n+k +1 interpretations from the definition of r-satisfiability integrated within a single interpretation if we rename the flexible symbols accordingly. The advantage of this approach is that we can, w.l.o.g., assume that this interpretation is a canonical interpretation, which is not possible with the single interpretations from the definition of rsatisfiability because of the shared domain. Hence, for every i 2 [0; n + k + 1] and every flexible name X in NC(O) [ NR(O), we introduce a fresh name X(i) called the i-th copy of X. If X is a more complex expressions (an axiom, CQ, or conjunction of CQ literals), X(i) is obtained by replacing every occurrence of a flexible name by its i-th copy. By [4, Lem. 4.14], W is r-satisfiable w.r.t. and K iff the conjunction W; of CQ literals has a model I w.r.t. hOW; ; Ai, where: W; :=
^ 1 i k (n+1+i) i ^
^ 0 i n ((i)i); (i) := OW; := f (i) j 6 As above, this can be ensured, for example, by assuming > to be rigid. For simplicity, we often focus on some i 2 [0; n + k] and consider the i-th copies of concept and role names as the (original) flexible names and disregard all other copies (but not the rigid names); in the following, we refer to those parts of I, in which the signature is smaller and renamed, as Ii. Similarly, we consider T(a; Ii) to be the type of a in I for i 2 [0; n + k], and may refer to the set of all these types as the temporal type of a in I.
We then can define the components of the required tuple t for i 2 [0; n + k] and c 2 NI(K) [ NIaux easily: Tc;i := T(c; Ii) and
A0i := f(:)B(a) j a 2 NI(K) [ NIaux; B 2 B(O); a 2 BIi (a 62 BIi )g [ f(:)R(a; b) j a; b 2 NI(K); R 2 NR(O); (a; b) 2 RIi ((a; b) 62 RIi )g: For all 2 T, we choose an arbitrary a 2 NI(K) [ NIaux with temporal type in I; for each i 2 [1; j j], define I i to be some Ijja with i = T(a; Ij ); and then define (A i )1 i j j := TreeABox( ; (I i )1 i j j; a); if there is no such element a, the ABoxes are empty. We can assume the latter algorithm to iterate only once over the types because the interpretations of the new names in all the interpretations are given already, by the interpretations of the elements for which they were introduced, respectively (i.e., we do not have to extend interpretations).
It is easy to see that the tuple is as required—that is, Ii represents the model of KRi—if ( ) we assume I to be such that (1) the trees of unnamed successors for two names a; b 2 NI(K) [ Naux that have the same temporal type in I are
I isomorphic w.r.t. the rigid symbols and that (2) it interprets those successors t the same in Ii and Ij if T(a; Ii) = T(a; Ij ). This is the case because Atree;i then is trivially satisfied for all i 2 [0; n + k]: the interpretations that can be selected for the construction of a prototypical ABox A then all are isomorphic; that is, the construction neither depends on the name chosen as prototype for the temporal type nor on the indexes i whose interpretation Ii is chosen as prototype for a type. We lastly show that ( ) is a valid assumption. The proof is by contradiction. We hence assume that such a given model I cannot be simplified in the described way without loosing the property that it satisfies both the KB and the conjunction of CQ literals. Let J be a corresponding adaptation of such a model I, constructed as follows: – For every temporal type for which there is an individual name a such that is the temporal type of a in I, and for every j 2 [1; j j], select one index ij 2 [0; n + k] such that j = T(a; Iij ), and let A ;j be the (possibly infinite) set of assertions representing Iij on all unnamed successors of a. That is, A ;j covers all the successors contained in I, but it only describes I w.r.t. the rigid names and the ij -th copies of flexible names. – Adapt I as follows. For every a 2 NI(K) [ NIaux with temporal type in I, replace all unnamed successors by copies of the elements occurring in A ;j (for an arbitrary j 2 [1; j j]). For every i 2 [0; n + k], the interpretation of the i-th copies of names on these elements in J is then given by the corresponding flexible assertions in the one set A ;j for which we have j = T(a; Ii). The interpretation of the rigid names is also given by these ABoxes since they all agree on those names. As with I, we use interpretations Ji to refer to J on the rigid names and on the i-th copies; that is, we consider the i-th copies as the (original) flexible names and disregard all other copies. – The construction of J maintains the types, meaning that T(a; Ji) = T(a; Ii) for all a 2 NI(K) [ Naux, i 2 [0; n + k]. Let (B; M; Q) := T(a; Ii), (B0; M0; Q0) :=
I T(a; Ji). Note that, to replace the unnamed successors of a in I, we chose unnamed successors of some b 2 NI(K) [ Naux of the same temporal type as a in I; I and that the interpretation in Ji on a and its unnamed successors is given by the one on b and its unnamed successors in some Ij with T(b; Ij ) = T(a; Ii). Clearly, for every homomorphism of some ' 2 Q0 into Jija, there is a corresponding one into Ijjb if a does not occur in ', by the definition of Ji. This especially holds because the interpretation of the rigid symbols on a and its unnamed successors in the whole interpretation J is fully determined by the interpretation of the rigid symbols in Ijjb. If a occurs in ', then the definition of T(a; Ii) yields fag 2 M, and T(b; Ij ) = T(a; Ii) hence implies a = b by the definition of T(b; Ij ). The construction of Jija then, as before, yields Q0 Q. For the other direction, we consider a homomorphism of some ' 2 Q into Ii. But then we also have one of ' into Ij which, in turn, yields a corresponding one into Ji. M = M0 follows by analogous arguments. We show B = B0. Since we do not adapt the interpretation of the concept and role names w.r.t. only named individuals, it is left to focus on basic concepts of the form 9R. The only critical case is thus the one where there is an element uaR in I but not in J and a has no named R-successor (in both I and J ) either; that is, there is no element ubR in I, but b has a named R-successor (again in both I and J ) by BT(a; Ii) = BT(b; Ij ). However, note that we assume the ontology to contain all CIs of the form 9R v 9R. Hence, the element ubR must exist in I by Definition 1. By construction, we thus get that uaR exists in J , which contradicts the assumption. The case where an element uaR exists in J but not in I is not critical w.r.t. possible changes of the basic type.
Since we do not adapt the interpretation of the concept and role names w.r.t. only named elements, J j= A. Regarding the named elements, J also satisfies OW; since the adaptation retains the basic types. Regarding an unnamed element e, observe that it is valid to argument based on the single interpretations Ji, i 2 [0; n + k], instead of on J as a whole because the ontology contains no axioms where different kinds of copies occur in and Ji represents the interpretation of rigid names in J . The interpretation of e in such a Ji corresponds to the interpretation of an isomorphic element in some Ij , j 2 [0; n + k]. But we have I j= OW; , and OW; contains all copies (i.e., also the j-th) of all axioms in O. So Ji satisfies all axioms in O, which yields J j= OW; . J also satisfies all CQ literals '(i) satisfied in I. This is clear if only named individuals are considered because I and J agree on the interpretation of concept and role names w.r.t. only named individuals and the basic types are maintained. For the other cases, observe that we can argument based on single interpretations Ii=Ji, again, since the copies of the CQs only contain one kind of copies of names, and all these interpretations for I/J agree on the rigid symbols. We consider the case where there is a homomorphism that maps to maximally one named individual. All the unnamed elements in the range must form a tree structure with a named individual a 2 NI(K) [ Naux as root. Assuming T(a; Ii) = (B; M; Q), we must
I have ' 2 Q by Definition 3. From T(a; Ii) = T(a; Ji), we get that '(i) also in J is satisfied based on a and its unnamed successors. If there is a homomorphism mapping to both several named and unnamed elements, then a corresponding homomorphism 0 into J can be obtained based on the type. By Definition 3, for all a 2 (NI(K) [ Naux) \ range( ), there is a set of terms Va in T(a; Ii)(2)
I containing exactly the terms t 2 NT(') with (t) = a or (t) being an unnamed successor of a. From T(a; Ji) = T(a; Ii), we get Va 2 T(a; Ji)(2), which means that there must be a corresponding partial homomorphism a of ' into Ji, again by Definition 3. Now, we define 0: (i) 0(t) := (t) if (t) 2 NI(K [ NIaux). (ii) 0(t) := a(t) for all a 2 (NI(K) [ NIaux) \ range( ) and t 2 Va. Regarding the negative CQ literals, we proceed by contradiction and assume that J j= '(ji) for some pj 2 W (i). Again, we can consider single interpretations Ii=Ji. Since we do not adapt the interpretation of the names on only named elements the corresponding homomorphism must map to unnamed elements. It can neither map to only unnamed elements and maximally to one named element: the arguments correspond to those given above for the corresponding case for the positive CQ literals if Ii and Ji and I and J are switched, respectively. The same holds for the case where maps to several named and to unnamed elements.
(() We regard a tuple t that satisfies the conditions from Lemma 1 and construct interpretations I0; : : : ; In, J1; : : : ; Jk as required based on the KBs in Condition (C1), which contain all the necessary information (i.e., KRi yields Ii for i 2 [0; n] and Ji for i 2 [n + 1; n + k]): we have the name-ABoxes for the named t individuals in the TKB, and Atree;i for all i 2 [0; n + k] for those successors (up to some “depth” d0 d) of the latter individuals that must exist given O. The shared domain of our interpretations contains all of the names occurring in these KBs and additional unnamed elements, to include the required successors of depths greater than d0. The idea is to inductively introduce elements by continuing the repetition we have given the construction of the tree-ABoxes.
The ontology and the ABoxes Ai for i 2 [0; n + k] are clearly satisfied by the respective interpretations, since the KBs KRi are consistent and our interpretations are completely defined based on canonical ones (i.e., the ones used to cont struct the ABoxes Atree;i; these ABoxes describe the interpretations completely in the sense that they capture all the necessary rigid knowledge and nondeterministic decisions). The additional ABoxes AQ (i) ensure that the positive CQ literals are satisfied as required. By contradiction, it can easily be shown that no negative CQ literal is satisfied. By (C2), a corresponding homomorphism must map to unnamed elements and, since we untangle the interpretations during the construction of Attree;i to depth 2m, it cannot map to elements in NI(K) [ NIaux. This yields a contradiction to (C2) because there are isomorphic named elements for all those maps to, since the repeating trees are of depth m. tu
Regarding complexity: W and can be guessed in polynomial time, and the LTL satisfiability testing w.r.t. a given W and can be done in polynomial time Theorem 1. TCQ entailment regarding a TKB in DL-LitekHrom is in co-NP.
The expressivity of TCQs allows to reduce TCQ entailment in much more
expressive DLs to TCQ entailment in DL-LitekHrom [