Many types of temporalised description logics (DLs) have been suggested and investigated in the past 15 years. We refer the reader to the survey papers and monograph [9, 14, 3, 16], where the history of the development of both interval and point-based temporal extensions of DLs is discussed in full detail. Temporal operators can be applied in various ways in order to introduce a temporal dimension to a DL. In particular, they can be used as constructors for concepts, roles, TBox and ABox axioms (such concepts, roles or axioms are called temporalised). Alternatively, one may declare a certain concept, role or axiom to be regarded as rigid in the sense that its interpretation does not change in time|usually, the rigidity can be expressed if temporal operators are allowed to be applied to the respective construct. A number of complexity results have been obtained for di erent combinations of temporal operators and DLs. For instance, the following is known for combinations of ALC with the linear-time temporal logic LT L: the satis ability problem for the temporal ALC is
1. undecidable if temporalised concepts with rigid axioms and roles are allowed
in the language (actually, a single rigid role is enough); see [
In other words, as long as one wants to express the temporal behaviour of only axioms and concepts (but not roles), then the resulting combination is likely to be decidable. As soon as the combination allows reasoning about the temporal behaviour of binary relations it becomes undecidable, unless we limit the means to describe the temporal behaviour of concepts. Furthermore, we notice that better computational behaviour is exhibited in cases where rigid axioms are used instead of more general temporalised ones.
In this paper, we are interested in the scenario where axioms are rigid,
concepts are temporalised and roles may be rigid or local (i.e., can change
arbitrarily). To regain decidability in this case one has to restrict either the temporal [
Temporal extensions of various dialects of DL-Lite have also been
studied [
In this paper, we consider another temporal extension TDL-Liteb3ool of the
logic DL-LitebNool. The logic TDL-Liteb3ool weakens TDL-Litebool of [
TDL-Liteb3ool: a Simple Temporal Description Logic
We begin by de ning the description logic TDL-Liteb3ool as a temporalisation of
DL-LitebNool [
The language of TDL-Liteb3ool contains object names a0; a1; : : : , concept names A0; A1; : : : , local role names P0; P1; : : : and rigid role names G0; G1; : : : ; roles R, basic concepts B and concepts C; D are de ned as follows:
R
B C; D ::= ::= ::=
Pi ? B j j j
Pi Ai :C j j j
j Gi q R; C u D
Gi ; j 3C; where q 1 is a natural number. A TDL-Liteb3ool TBox T consists of concept inclusions of the form C v D, and an ABox A of the assertions of the form: nB(a), nR(a; b), 2B(a) and 2R(a; b), where B is a basic concept, R a role, a, b object names and n denotes the sequence of n next-time operators , for n 0. The TBox and ABox together form the knowledge base (KB) K = (T ; A). A TDL-Liteb3ool interpretation I is a function on natural numbers N: I(n) =
I ; a0I ; : : : ; A0I(n); : : : ; P0I(n); : : : ; G0I(n); : : : ; where I is a non-empty set, the domain of I, aiI 2 I , AiI(n) I and PiI(n); GiI(n) I I , for all i and all n 2 N. Furthermore, aiI 6= ajI for i 6= j (which means that we adopt the unique name assumption) and GI(n) = GI(m), i i for all n; m 2 N. The role and concept constructs are interpreted in I as follows: for each moment of time n 2 N, (Ri )I(n) = (y; x) 2
I
I j (x; y) 2 RI(n) ; i ( q R)I(n) = x 2
I j ]fy j (x; y) 2 RI(n)g
?I(n) = ;; q ; (:C)I(n) =
I n CI(n); (C u D)I(n) = CI(n) \ DI(n); k>n where ]X is the cardinality of X; note that the 3 is interpreted in the strong sense, i.e., it does not include the present. We will use standard abbreviations such as C1 t C2 = :(:C1 u :C2), > = :?; 9R = ( 1 R) and 2C = :3:C. The satisfaction relation j= is de ned as follows: (3C)I(n) = [
CI(k); I j= C v D
nB(a) I j=
I j= 2B(a)
nR(a; b) I j=
I j= 2R(a; b) i i i i i
CI(n)
DI(n) for all n
0; aI 2 BI(n); aI 2 BI(n) for all n > 0; (aI ; bI ) 2 RI(n); (aI ; bI ) 2 RI(n) for all n > 0: We say an interpretation I is a model of a KB K if I j= for all in K. In this case we also say that K is consistent and we write I j= K. A concept A (role R) is satis able w.r.t. K if there exists a model I of K and n 0 such that AI(n) 6= ; (RI(n) 6= ;).
Note that TDL-Liteb3ool is not a simple fusion of the two component logics, DL-LitebNool and LT L. Indeed, let K = (f39R v ?; 9R v 39Rg; f9R(a)g). It 3 is easy to see that K is not satis able in TDL-Litebool. However, it is satis able both in DL-LitebNool (if we substitute the temporal concepts by fresh DL-LitebNool concepts) and in LT L (by substituting 9R concepts with fresh atomic propositions). 3
Satis ability of TDL-Liteb3ool KBs is NP-complete To prove the NP complexity result we rst establish in Section 3.1 a relation between TDL-Liteb3ool and the one-variable fragment QT L1 of rst-order temporal logic. This will allow us to polynomially reduce the satis ability problem in TDL-Liteb3ool to that in TDL-Lite03, a language that has neither rigid roles nor role assertions. Next, in Section 3.2, we show that a TDL-Lite03 KB K is satis able i there exists a quasimodel for it. Then we show that if there is a quasimodel for K then there exists an ultimately periodic quasimodel for it such that both the length of the pre x and the length of the period are polynomial in the length of K. Finally, in Section 3.3, we describe an algorithm that checks (in non-deterministic polynomial time) the existence of an ultimately periodic quasimodel for a given TDL-Lite03 KB.
TDL-Liteb3ool in the context of First-Order Temporal Logic For a TDL-Liteb3ool KB K = (T ; A), let ob(A) be the set of all object names occurring in A. Let role (K) be the set of all (local and rigid) role names, together with their inverses, occurring in K, and grole (K) the set of rigid role names, together with their inverses, occurring in K. For R 2 role (K), let QRK be the set of natural numbers containing 1 and all the numerical parameters q for which q R occurs in K. Denote by ev(K) the set of all concepts of the form 3C occurring in K and, nally, let NK = fn j nB(a) 2 A or nR(a; b) 2 Ag; without loss of generality, we assume that NK is non-empty.
With every object name a 2 ob(A) we associate the individual constant a of QT L1, the one variable fragment of rst-order temporal logic over (N; <), and with every concept name A the unary predicate A(x) from the signature of QT L1. For each R 2 role (K), we also introduce jQRKj fresh unary predicates EqR(x), for q 2 QRK. Intuitively, for each n 0, E1R(x) and E1R (x) represent the domain and range of R at moment n (i.e., E1R(x) and E1R (x) are interpreted by the sets of points with at least one R-successor and at least one R-predecessor at moment n, respectively), while EqR(x) and EqR (x) represent the sets of points with at least q distinct R-successors and at least q distinct R-predecessors at moment n.
By induction on the construction of a TDL-Liteb3ool concept C we de ne the QT L1- formula C :
? = ?; ( q R) = EqR(x); (C1 u C2) = C1 (x) ^ C2 (x);
(A) = A(x); (:C) = :C (x); (3C) = 3C (x); and then extend this translation to TDL-Liteb3ool TBoxes T :
T =
^ C1vC22T
2+8x (C1 (x) ! C2 (x)); where 2+' = ' ^ 2'. The following formulas express some natural properties of the role domains and ranges. For R 2 role (K), we need two QT L1-sentences: R = q;q02QR; q0>q
K q0>q00>q for no q002QRK "R = 9x E1R(x) ! 9x inv(E1R)(x); ^ 8x Eq0 R(x) ! EqR(x) ; (1) (2) where inv(E1R) is the predicate E1P (x) if R = P and E1P (x) if R = P . Sentence (1) says that if the domain of R is non-empty then its range is nonempty either.
Without loss of generality we may assume that if R is a rigid role and A contains nR(a; b) or 2R(a; b) then it also contains both R(a; b) and 2R(a; b). Then we de ne `temporal slices' of the ABox A by taking:
A2 = An =
R(a; b) j 2R(a; b) 2 A or 2inv(R)(b; a) 2 A ; R(a; b) j nR(a; b) 2 A or ninv(R)(b; a) 2 A [
R(a; b) j n > 0 and either 2R(a; b) 2 A or 2inv(R)(b; a) 2 A : The QT L1 translation of the ABox A is de ned as follows:
A =
^ nB(ai)2A nB (ai) ^
^ R(a;b)2An nEqR;a;An R(a) ^ ^
2EqR;a;A2 R(a); R(a;b)2A2 where, for a role R, a 2 ob(A) and any ABox A0, qR;a;A0 = max(f0g [ fq 2 QRK j R(a; ai) 2 A0; 1 i q & ai1 6= ai2 if i1 6= i2g): Finally, we set Kz = T ^ ^ 2+ "R ^ R ^ ^ R2role (K) T 2grole (K) q2QTK ^2+8x EqT (x) $ 2EqT (x) ^ A : Observe that the length of Kz is polynomial in the length of K. It can be shown (for details see [7, Theorem 2 and Corollary 3]) that we have: Theorem 1. A TDL-Liteb3ool KB K is satis able i the QT L1-sentence Kz is satis able.
Denote by TDL-Lite03 the fragment of TDL-Liteb3ool without rigid roles and ABox assertions of the form 2R(a; b) or nR(a; b). By Theorem 1, this fragment is of the same complexity as TDL-Liteb3ool: Lemma 1. Given a TDL-Liteb3ool KB K one can construct (in polynomial time) a TDL-Lite03 KB K0 such that K and K0 are equisatis able.
Proof. Let A0 be the part of A that contains no assertions of the form 2R(a; b) or nR(a; b). Then we set K0 = (T [ T 0; A0 [ A0), where T 0 = 2( q T ) v ( q T ); ( q T ) v 2( q T ) j q 2 QTK; T 2 grole (K) ; A0 =f n( qR;a;An R)(a) j R(a; b) 2 Ang [ f2( qR;a;A2 R)(a) j R(a; b) 2 A2g: Clearly, Kz = (K0)z. Then the claim immediately follows from Theorem 1. q In this section, we de ne a notion of a quasimodel for a TDL-Lite03 KB and show that a TDL-Lite03 KB is satis able i there is an ultimately periodical quasimodel with the length of both the pre x and period bounded by a polynomial function in the length of K. It will follow then that the satis ability problem for TDL-Lite03, and thus for TDL-Liteb3ool, is in NP.
Let K = (T ; A) be a TDL-Lite03 KB. We introduce, for every concept of the form 3C, a fresh concept name FC , the surrogate of 3C, and then, for a concept D, denote by D the result of replacing each 3C in D with the surrogate FC . For a TDL-Lite03 TBox T , denote by T the DL-LitebNool TBox obtained by replacing every concept C in T with C.
Let cl(K) be the closure under negation of all concepts occurring in T together with the 9R, for R 2 role (K), and the B, for nB(a) 2 A or 2B(a) 2 A. A type for K is a subset t of cl(K) such that { C u D 2 t i C; D 2 t, for every C u D 2 cl(K); { :C 2 t i C 62 t, for every C 2 cl(K).
A type t for K is realisable if the concept dC2t C is satis able w.r.t. T .
A function r mapping N to types for K is called a coherent and saturated run for K if the following conditions are satis ed: (real) r(i) is realisable, for all i 0; (coh) for all i 0 and 3C 2 ev(K), if C 2 r(i) then 3C 2 r(j), for all j with 0 j < i; (sat) for all i 0 and 3C 2 ev(K), if 3C 2 r(i) then there is j > i such that
C 2 r(j).
A witness for K is a pair of the form (r; ), where r is a coherent and saturated run for K, N and j j 1.
Given a run r and a nite sequence s = (s(0); : : : ; s(n)) of types for K, we set: r<i = (r(0); : : : ; r(i 1)); r i = (r(i); r(i + 1); : : : ); s! = (s(0); : : : ; s(n); s(0); : : : ; s(n); : : : ); s r = (s(0); : : : ; s(n); r(0); r(1); : : : );
We say that a type t for K is stutter-invariant if :3C 2 t implies :C 2 t, for each 3C 2 ev(K).
A quasimodel for K is a triple Q = hW; K; Li, where W is a set of witnesses for K and K; L are natural numbers with 0 K L such that: (runs) W = (ra; ;) j a 2 ob(A) [ (rR; fiRg) j R 2 , for some role (K); (stuttr) r(K) and the r(i), for i L, are stutter-invariant, for each (r; ) 2 W ; (obj) if nB(a) 2 A then B 2 ra(n); if 2B(a) 2 A then B 2 ra(i) for all i > 0; (role) for all i 0 and R 2 role (K), if 9R 2 r(i), for some (r; ) 2 W , then (rR; fiRg) 2 W , 9R 2 rR(iR) and either i iR < K or K iR < L. Theorem 2. A TDL-Lite03 KB K is satis able i there exists a quasimodel Q = hW; K; Li for K such that L max NK + jev(K)j (jrole (K)j + 2) + 3. Proof. ()) Suppose I j= K. For m
0, let Fm =
m with RI(i) 6= ; : Lemma 2. For all n; v 0, there exists m such that n for every role R 2 F0, either R 2 Fm+v+1 or R 2= Fm+1. m Proof. If a role R is non-empty in nitely often then R 2 Fm+v+1, for any m. So we have to consider only those roles that are non-empty nitely many times. Let
FG = R 2 role (K) j there is i 0 such that R 2= Fi : For R 2 FG\F0, let iR = min i j R 2= Fi+1 (i.e., iR is the last moment when R is non-empty). If maxfiR j R 2 FGg n + v jF0j, we take m = max(fng [ fiR j R 2 FGg). Clearly, FG \ Fm+1 = ; (so all roles in FG are empty after m). Otherwise, FG \ F0 6= ; and without loss of generality we may assume that FG \ F0 = fR1; : : : ; Rsg and iR1 iR2 iRs . If iR1 > n + v, we take m = n; then FG\F0 Fm+v+1 (all roles in FG\F0 are non-empty after m+v). Otherwise, iR1 n + v and iRs > n + v jF0j, whence iRs iR1 > (v 1) jF0j. Let j0 be the smallest j, 1 j < s, such that iRj n and iRj+1 iRj > v (it exists as s jF0j) and set m = iRj0 . We then have R1; : : : ; Rj0 2= Fm+1 and Rj0+1; : : : ; Rs 2 Fm+v+1. q N M N + V KjF0ajndsucVh t=hajte,vf(oKr)je.veBryy rLoelmemRa22,Ft0h,eerietheexrisRts 2MFKwitohr
Let N = max N for each R 2 FK , and iR = maxfi j RI(i) 6= ;g, for each R K2 jFR0In(i)F=M+;g1,. R 2= FM+1, where K = M + V + 1. We then set iR = minfi 6 Clearly, for each R 2 F0, either iR M or iR K. For d 2 I, denote rd : i 7! fC 2 cl(K) j d 2 CI(i)g (it evidently is a coherent and saturated run). For each R 2 F0, we x some dR 2 (9R)I(iR) and set rR = rdR . Let
W = (rR; fiRg) j R 2 F0 [ (raI ; ;) j a 2 ob(A) : Clearly, both (runs) and (obj) hold. We also have 9R 2 r(i) i 9R 2 rR(iR) and (rR; fiRg) 2 W , for all (r; ) 2 W and i 0.
We now transform W by expanding and pruning runs in such a way that the r(i) are never thrown out, for (r; ) 2 W and i 2 .
Lemma 3. For each coherent and saturated run r,
jfi j r(i) is not stutter-invariantgj jev(K)j.
Proof. Suppose there are 0 i1 < < in such that n > jev(K)j and r(i1); : : : ; r(in) are not stutter-invariant, i.e., for each 1 j n, there are 3Cj 2 ev(K) with :3Cj; Cj 2 r(ij). Then there is 3C 2 ev(K) such that :3C; C 2 r(ij) and :3C; C 2 r(ij0 ) for some 0 ij < ij0 . As C 2 r(ij0 ), we obtain, by (coh), 3C 2 r(ij), contrary to :3C 2 r(ij). q
Step 1. By Lemma 3, for each (r; ) 2 W , there is jr, M < jr K, such that r(jr) is stutter-invariant. Set r0 = r<jr r(jr) : : : r(jr) r jr ;
| K j{rztimes } 0 = fi j i 2 ; i jrg [ fi + K jr j i 2 ; i > jrg: It should be clear that r0 is a coherent and saturated run. Denote by W 0 the set of all (r0; 0) constructed as above. Clearly, r0(K) is stutter-invariant, for each (r0; 0) 2 W 0. It is easy to see that, for each R 2 F0, we have (rR0; fi0Rg) 2 W 0 and either i0R M or i0R K.
Step 2. For (r0; 0) 2 W 0, let 0 = fi > K j r0(i) not stutter-invariantg. By Lemma 3, j 0j jev(K)j. We prune the run r0, if 0 [ 0 6= ;, by removing all stutter-invariant r0(i) with K < i < max( 0 [ 0). Denote the resulting run by r00. It should be clear that r00 is coherent and saturated. Set 00 = fi j i 2 0; i
Kg [ fK + jfj 2 0 [ 0 j j igj j i 2 0; i > Kg: Let W 00 be the set of all witnesses (r00; 00) constructed as above and L = K + V + 2. It follows that, for each (r00; 00) 2 W 00, all the types r00(i) are stutterinvariant, for i L, and thus (stuttr) holds. It is also easy to see that, for each R 2 F0, we have (rR00 ; fi0R0 g) 2 W 00 and K i0R0 < L, if R 2 FK , and i0R0 M , if R 2= FM+1. Therefore, we have (role). So, Q = hW 00; K; Li is as required.
(() Let Q = hW; K; Li be a quasimodel for K. We construct a model for Kz which, by Theorem 1, is enough to show that K is satis able. Let R = ra j (ra; ;) 2 W
[ rR<K (rR(K))i iR rRK j (rR; fiRg) 2 W; i > iR rRi j (rR; fiRg) 2 W; 0
iR i [
K : Clearly, each r 2 R is a coherent and saturated run for K. Moreover, if we have (rR; fiRg) 2 W and iR < K then there is r0 2 R with 9R 2 r0(i), for all i, 0 i iR. And if (rR; fiRg) 2 W and iR K then there is r0 2 R with 9R 2 r0(i), for all i 0. As follows from (role), for each R 2 , we have either iR K and iR K or iR = iR < K. So, for all i 0 and r 2 R, if 9R
We construct a rst-order temporal model M based on the domain D = R by taking aM = ra, for each a 2 ob(A), and (B )M;i = fr 2 R j B 2 r(i)g, for each B 2 cl(K) and i 0. It should be clear that (M; 0) j= Kz. q Theorem 3. If there is a quasimodel Q = hW; K; Li for K then there is an ultimately periodical quasimodel Q0 = hW 0; K; Li, that is, there is P jev(K)j such that r0(i + P ) = r0(i), for all i > L and (r0; 0) 2 W 0.
Proof. We begin the proof with the following observation: Lemma 4. Let r be a coherent and saturated run and let l 0 be such that every r(i) is stutter-invariant, i l. Then there are i1; : : : ; ijev(K)j l such that r0 = r l r(i1) : : : r(ijev(K)j) ! is a coherent and saturated run. Proof. First we show that r(l) \ ev(K) = r(j) \ ev(K); for all j > l: Assume there is j > l and 3C 2 r(l) such that 3C 62 r(j). As r(j) is stutterinvariant, we have C 62 r(j) and, by (coh), 3C 62 r(j 1). By repeating this argument su ciently many times, we obtain 3C 62 r(l), contrary to our assumption. The converse direction|i.e., for each j > l, if 3C 2 r(j) then 3C 2 r(l)| follows immediately from (coh).
For each 3C 2 ev(K), we can select an i, i l, such that C 2 r(i) whenever 3C 2 r(l). Let i1; : : : ; ijev(K)j be all such i. It remains to show that r0 is coherent and saturated.
For coherency, suppose that C 2 r0(i), for i 0. By (coh) for r, we have 3C 2 r0(j), for each 0 j < i such that j l. It remains to consider j with l < j < i. It follows that r0(i) = r(ik), for some 1 k jev(K)j, from which, by (coh) for r, 3C 2 r(l) = r0(l) and, by (3), 3C 2 r0(j).
For saturation of r0, suppose 3C 2 r0(i), for i 0. If 3C 2 r(l) then C 2 r(ik) for 1 k jev(K)j and, by the construction of r0, there is j > i such that r0(j) = r(ik). Thus C 2 r0(j). If 3C 62 r(l) then, by (3), i < l, from which 3C 2 r(i). By (sat) of r, there is j > i with C 2 r(j) and, by (3), j l. Thus C 2 r(j) = r0(j). q As shown in Section 3.1, there is a polynomial-time reduction of the satis ability problem for TDL-Liteb3ool KBs to the satis ability problem for TDL-Lite03 KBs. So it su ces to present an NP decision algorithm for the latter problem.
Our algorithm, given a TDL-Lite03 KB K = (T ; A), guesses the `pre x' of length L + 1 and the period of length P of an ultimately periodical quasimodel Q0 = hW 0; K; Li for K as in Theorem 3, and then checks whether conditions (runs), (stuttr), (obj) in Section 3.2 hold and whether the types in positions L + 1 and L + P + 1 of the pre x coincide for every run.
More precisely, rst we guess and store numbers K, L and P such that K L, L max NK + jev(K)j (jrole (K)j + 2) + 3 and P jev(K)j. Then we guess a set role (K) and numbers fiR < L j R 2 g. For every R 2 , we also guess a sequence rR of length L + P + 2 of types for K and, for every a 2 ob(K), a sequence ra of length L + P + 2 of types for K.
Let W0 = f(rR; fiRg) j R 2 g [ f(ra; ;) j a 2 ob(K)g. The set W0 can be regarded as a nite representation of the witnesses W 0 from Q0. Now we check that the following conditions hold: 1. r(K) and the r(i), for L i L + P + 1, are stutter-invariant, for each (r; ) 2 W0; 2. if nB(a) 2 A then B 2 ra(n); if 2B(a) 2 A then B 2 ra(i), for all 0 < i L + P + 1; 3. for all i L + P + 1 and R 2 role (K), if 9R 2 r(i), for some (r; ) 2 W0, then (rR; fiRg) 2 W0, 9R 2 rR(iR) and either i iR < K or K iR < L; The algorithm returns `yes' i all the conditions above are satis ed.
The presented algorithm is sound: indeed, if conditions 1{7 are satis ed we can construct an ultimately periodical quasimodel for K which, by Theorem 2, means that K is satis able. The algorithm is also complete: if K is satis able then, by Theorems 2 and 3, there exists an ultimately periodical quasimodel Q = hW 0; K; Li with period P and K, L, P bounded by polynomial functions in jKj as above; then W0 consisting of the pre xes of length L + P + 2 of runs in W 0 satis es conditions 1{7 and thus the algorithm returns `yes.'
Finally, it is easy to see that L, K, P and W0 can be constructed and
conditions 1{7 checked by a non-deterministic polynomial-time algorithm in jKj. In
particular, condition 5 can be veri ed by calling, for each r with (r; ) 2 W0
and i L + P + 1, a DL-LitebNool satis ability checking algorithm for the concept
dC2r(i) C w.r.t. the TBox T , which can be done in NP [
Then, by Lemma 1 and because TDL-Liteb3ool `contains' propositional logic, we obtain the following: Theorem 4. The satis ability problem for TDL-Liteb3ool KBs is NP-complete. Now we show NP-hardness of satis ability in the fragment TDL-Litec3ore of TDL-Liteb3ool that allows only concept inclusions of the form A1 v A2, A1 v :A2, 3A1 v A2 or A1 v 3A2, where A1 and A2 are concept names.
Lemma 5. The satis ability problem for TDL-Litec3ore KBs is NP-hard. Proof. We prove this by reduction of the graph 3-colourability (3-Col) problem, which is formulated as follows: given a graph G = (V; E), decide whether there is an assignment of colours f1; 2; 3g to vertices V such that no two vertices ai; aj 2 V sharing the same edge, (ai; aj ) 2 E, have the same colour. Let Ai, for Ai 2 V , Xi, for 0 i 3, and V , V 0 be concept names and a an object name. Consider the KB KG = (TG; fV (a)g), where TG consists of the following axioms: V v 3Ai; Ai v :Aj ; V v :V 0; 3X3 v X2;
Ai v X3;
for all Ai 2 V; for all (Ai; Aj ) 2 E; 3X0 v V 0; 3X2 v X1; 3X1 v X0: It is easy to see that KG is satis able i G is 3-colourable. Indeed, if G is 3colourable, then we take a colouring function c : V ! f1; 2; 3g and de ne I by setting I = fwg, aI = w, aI 2 AiI(n) i c(Ai) = n, for all Ai 2 V , aI 2 V I(n) i n = 0, V 0I(n) = ;, for all n 0, and aI 2 XiI(n) i i < n. It should be clear that I j= KG. For the converse direction, observe that if KG is satis able then, for all Ai 2 V , there is ni 2 f1; 2; 3g such that aI 2 AI(ni) and aI 62 AI(ni) i j whenever (Ai; Aj ) 2 E. It is readily seen that c : Ai 7! ni, for Ai 2 V , is a colouring function. q
As a consequence of Lemma 5 and Theorem 4 we obtain: Theorem 5. The satis ability problem for TDL-Litec3ore KBs is NP-complete. 4
The NP complexity result for TDL-Liteb3ool is encouraging in view of possible
applications of this logic for reasoning about temporal conceptual data models [
The logic TDL-Liteb3ool presented in this paper combines a much simpler DL
DL-LitebNool (ALCQI used in [