DL-Lite with Attributes and Sub-Roles (Extended Abstract) A. Artale,1 A. Ibáñez Garcı́a,1 R. Kontchakov,2 and V. Ryzhikov1 1 2 KRDB Research Centre Dept. of Comp. Science and Inf. Sys. Free University of Bozen-Bolzano, Italy Birkbeck College, London, UK {lastname }@inf.unibz.it roman@dcs.bbk.ac.uk 1 Introduction The DL-Lite family of description logics has recently been proposed and investi- gated in [5–7] and later extended in [1, 8, 3]. The relevance of the DL-Lite family is witnessed by the fact that it forms the basis of OWL 2 QL, one of the three profiles of OWL 2 (http://www.w3.org/TR/owl2-profiles/). According to the offi- cial W3C profiles document, the purpose of OWL 2 QL is to be the language of choice for applications that use very large amounts of data. This paper extends the DL-Lite languages of [3] by relaxing the restriction on the interaction between cardinality constraints (N ) and role inclusions (or hierarchies, H). We also introduce a new family of languages, DL-LiteHN α A , α ∈ {core, krom, horn, bool}, extending DL-Lite with attributes (A). The notion of attributes, borrowed from conceptual modeling formalisms, introduces a distinction between (abstract) objects and application domain val- ues, and consequently, between concepts (sets of objects) and datatypes (sets of values), and between roles (relating objects to objects) and attributes (relating objects to values). The advantage of the presented languages over DL-LiteA [8] is that the range restrictions for attributes can be local (and not only global as in DL-LiteA ). Indeed, DL-LiteHN α A has a possibility to express concept inclusion axioms of the form C v ∀U.T , for an attribute U and its datatype T . In this way, we allow re-use of the very same attribute associated to different concepts with different range restrictions. For example, we can say that employees’ salary is of type Integer, researchers’ salary is in the range 35,000–70,000 (enumeration type) and professors’ salary in the range 55,000–100,000—while both researchers and professors are employees. Note that local attributes are strictly more expres- sive than global ones. For example, concept disjointness (or unsatisfiability) can be inferred just from datatype disjointness for the same (existentially qualified) attribute. Since DL-Lite languages have been proved useful in capturing concep- tual data models [8, 4, 2], the extension with attributes, as presented here, will generalize their use even further. We aim at establishing computational complexity of knowledge base satisfi- ability in these new DLs. In particular we prove the following results: 1. We can relax the restrictions presented in [3] limiting the interaction between sub-roles and number restrictions without increasing the complexity of rea- soning as far as the problem is limited to TBox satisfiability checking. As for KB satisfiability, the presence of the ABox should be taken into account if we want to preserve the complexity results. 2. The introduction of local range restrictions for attributes is for free for the languages DL-LiteN A NA NA bool , DL-Litehorn and DL-Litecore . 2 The Description Logic DL-LiteHN bool A The language of DL-LiteHN bool A contains object names a0 , a1 , . . ., value names v1 , v2 , . . ., concept names A0 , A1 , . . ., role names P0 , P1 , . . ., attribute names U0 , U1 , . . ., and datatype names T0 , T1 , . . .. Complex roles R and concepts C are defined below: R ::= Pi | Pi− , B ::= > | ⊥ | Ai | ≥ q R | ≥ q Ui C ::= B | ¬C | C1 u C2 , where q is a positive integer. The concepts of the form B are called basic concepts. A DL-LiteHN bool A TBox, T , is a finite set of concept, role, attribute and datatype inclusion axioms of the form: C1 v C2 , C v ∀U. T, R1 v R2 , U v U 0, T v T 0, T u T 0 v ⊥, and an ABox, A, is a finite set of assertions of the form: Ak (ai ), ¬Ak (ai ), Pk (ai , aj ), ¬Pk (ai , aj ), Uk (ai , vj ) and Tk (vj ). We standardly abbreviate ≥ 1 R and ≥ 1 U by ∃R and ∃U , respectively. Absence of an attribute (i.e., C v ∀U. ⊥) can be expressed as C u ∃U v ⊥. Together, a TBox T and an ABox A constitute the DL-LiteHN bool A knowledge base (KB) K = (T , A). In the following, we denote by role(K) and att(K) the sets of role and attribute names occurring in K, respectively; role ± (K) denotes the set {Pk , Pk− | Pk ∈ role(K)}. Semantics. As usual in description logic, an interpretation, I = (∆I , ·I ), con- sists of a nonempty domain ∆I and an interpretation function ·I . The interpre- tation domain ∆I is the union of two non-empty disjoint sets: the domain of objects ∆IO and the domain of values ∆IV . We assume that all interpretations agree on the semantics assigned to each datatype Ti , as well as on each constant vi . In particular, TiI = val(Ti ) ⊆ ∆IV is the set of values of datatype Ti , and each vi is interpreted as one specific value, denoted val(vi ), i.e., viI = val(vi ) ∈ val(Ti ). Furthermore, ·I assigns to each object name ai an element aIi ∈ ∆IO , to each concept name Ak a subset AIk ⊆ ∆IO of the domain of objects, to each role name Pk a binary relation PkI ⊆ ∆IO × ∆IO over the domain of objects, and to each attribute name Uk a binary relation UkI ⊆ ∆IO × ∆IV . We adopt here the unique name assumption (UNA): aIi 6= aIj , for all i 6= j. The role and concept constructs are interpreted in I in the standard way: (Pk− )I = {(y, x) ∈ ∆IO × ∆IO | (x, y) ∈ PkI }, (inverse role) I > = ∆IO , (domain of objects) I ⊥ = ∅, (the empty set) I = x ∈ ∆IO | ]{y | (x, y) ∈ RI } ≥ q ,  (≥ q R) (at least q R-successors) I = x ∈ ∆IO | ]{v | (x, v) ∈ U I } ≥ q ,  (≥ q U ) (at least q U -attributes) I = x ∈ ∆IO | ∀v. (x, v) ∈ U I → v ∈ T I ,  (∀U. T ) (attribute value restriction) I (¬C) = ∆IO \ C I , (not in C) I (C1 u C2 ) = C1I ∩ C2I , (both in C1 and in C2 ) where ]X is the cardinality of X. The satisfaction relation |= is also standard: I |= C1 v C2 iff C1I ⊆ C2I , I |= R1 v R2 iff R1I ⊆ R2I , I |= T1 v T2 iff T1I ⊆ T2I , I |= U1 v U2 iff U1I ⊆ U2I , I |= T1 u T2 v ⊥ iff T1I ∩ T2I = ∅, I |= Pk (ai , aj ) iff (aIi , aIj ) ∈ PkI , I |= Ak (ai ) iff aIi ∈ AIk , I |= ¬Pk (ai , aj ) iff (aIi , aIj ) ∈ / PkI I |= ¬Ak (ai ) iff aIi ∈ / AIk , I |= Uk (ai , vj ) iff (aIi , vjI ) ∈ UkI , I |= Tk (vj ) iff vjI ∈ TkI . A KB K = (T , A) is said to be satisfiable (or consistent) if there is an interpre- tation, I, satisfying all the members of T and A. In this case we write I |= K (as well as I |= T and I |= A) and say that I is a model of K (of T and A). 2.1 Fragments of DL-LiteHN bool A We consider various syntactical restrictions on the language of DL-LiteHN bool A along two axes: (i) the Boolean operators (bool ) on concepts, (ii) the role and attribute inclusions (H). Similarly to classical logic, we adopt the following def- initions. A TBox T will be called a Krom TBox 1 if its concept inclusions are restricted to: B1 v B2 , B1 v ¬B2 and ¬B1 v B2 , (Krom) (here and below all the Bi and B are basic concepts). T will be called a Horn TBox if its concept inclusions are restricted to: l Bk v B. (Horn) k Finally, we call T a core TBox if its concept inclusions are restricted to: B1 v B2 and B1 u B2 v ⊥. (core) 1 The Krom fragment of first-order logic consists of all formulas in prenex normal form whose quantifier-free part is a conjunction of binary clauses. As B1 v ¬B2 is equivalent to B1 u B2 v ⊥, core TBoxes can be regarded as sitting in the intersection of Krom and Horn TBoxes. In this paper we study the following logics, for α ∈ {core, krom, horn, bool}: DL-LiteHN A HN A krom , DL-Litehorn , DL-Litecore HN A are the fragments of DL-LiteHN bool A with Krom, Horn, and core TBoxes, respectively; DL-LiteHN α is the fragment of DL-LiteHN α A without attributes and datatypes; DL-LiteN α A is the fragment of DL-LiteHN α A without role and attribute inclu- sions. As shown in [3], reasoning in DL-LiteHN α is already rather costly (ExpTime- complete) due to the interaction between role inclusions and number restrictions. However, both of these constructs turn out to be useful for the purposes of conceptual modeling. By limiting their interplay one can get languages with a better computational properties [8, 3]. Before presenting such limitations we need to introduce some notation. For a role R, let inv (R) = Pk− if R = Pk and inv (R) = Pk if R = Pk− . Given a TBox T we denote by v∗T the reflexive and transitive closure of the relation {(R, R0 ), (inv(R), inv(R0 )) | R v R0 ∈ T }. We say that R ≡∗T R0 iff R v∗T R0 and R0 v∗T R. Say that R0 is a proper sub-role of R in T if R0 v∗T R and R 6v∗T R0 . A proper sub-role R0 of R is said to be a direct sub-role of R if there is no other proper sub-role R00 of R such that R0 is a proper sub-role of R00 ; the set of direct sub-roles of R is denoted as dsub T (R). The language DL-Lite(HN α ) [3] is the result of imposing the following syntactic HN restriction on DL-Liteα TBoxes T : (inter) if R has a proper sub-role in T then T contains no negative occurrences of number restrictions ≥ q R or ≥ q inv (R) with q ≥ 2 (an occurrence of a concept on the right-hand (left-hand) side of a concept inclusion is called negative if it is in the scope of an odd (even) number of negations ¬; otherwise it is called positive). We will formulate two alternative versions of restriction (inter). Definition 1. Given a TBox T and a role R ∈ role ± (T ), we define the following parameters:  ubound (R, T ) = min {∞} ∪ {q − 1 | q ≥ 2 and ≥ q R occurs negatively in T } ,  lbound (R, T ) = max {0} ∪ {q | ≥ q R occurs positively in T } , rank (R, T ) = max lbound (R, T ), R0 ∈dsub T (R) rank (R0 , T ) , P  rank (R, A) = max {0}∪{n | Ri (a, ai ) ∈ A, Ri v∗T R, for distinct a1 , . . . , an } .  Consider the languages obtained from DL-LiteHN α by imposing one of the fol- lowing two restrictions: (inter1) for every R ∈ role ± (T ), if R has a proper sub-role in T then ubound (R, T ) ≥ rank (R, T ); (inter2) for every R ∈ role ± (T ), if R has a proper sub-role in T then ubound (R, T ) ≥ rank (R, T ) + max{1, rank (R, A)}. language (inter) [3] (inter1) (inter2) non-restrict. DL-LiteHN core NLogSpace [3] NLogSpace [Th.1] DL-LiteHN horn PTime [3] PTime [Th.1] DL-LiteHN NLogSpace [3] ≥NP [Th.2] NLogSpace [Th.1] ExpTime [3] krom HN DL-Litebool NP [3] NP [Th.1] DL-LiteHN core A NLogSpace [Th.3] NLogSpace [Th.3] DL-LiteHN horn A PTime [Th.3] PTime [Th.3] DL-LiteHN A NP [Th.4] ≥NP [Th.2] NP [Th.4] ExpTime krom HN A DL-Litebool NP [Th.3] NP [Th.3] DL-LiteN A core NLogSpace [Th.3] DL-LiteN A horn PTime [Th.3] DL-LiteN A NA NA NA NP [Th. 4] krom DL-LiteN A bool NP [Th.3] Table 1: Complexity of DL-Lite logics (NA = Non-Applicable). These new restrictions are in some way weaker than (inter) and, for ex- ample, allow for the specialization of functional roles: KB K = (T , A) with T = {≥ 2 R v ⊥, R1 v R2 , R2 v R}, and A = {R(a, b), R1 (a1 , b1 ), R2 (a2 , b2 )} does not satisfy (inter), but it satisfies both (inter1) and (inter2). Finally, the above restrictions can also be applied to sub-attributes in the languages DL-LiteHN α A . Table 1 summarizes the obtained complexity results (with numer- ical parameters q coded in binary). 3 Reasoning in DL-LiteHN α In this section, we investigate the complexity of deciding KB satisfiability in languages DL-LiteHNα under the restrictions (inter1) and (inter2), respectively. We adapt the proof presented in [3], where a DL-LiteHN bool KB K = (T , A) is encoded into a sentence K‡e in the one-variable first-order logic QL1 . We use a slightly longer but simpler encoding. Every ai ∈ ob(A) is associated to the individual constant ai of QL1 , and every concept name Ai to the unary predicate Ai (x). For each concept ≥ q R in K we introduce a fresh unary predicate Eq R(x). For each role name Pk ∈ role ± (K), two individual constants dpk and dp− k are introduced, as representatives of the objects in the domain and range of Pk , respectively. The encoding C ∗ of a concept C is defined inductively: ⊥∗ = ⊥, (Ai )∗ = Ai (x), (≥ q R)∗ = Eq R(x), >∗ = >, (¬C)∗ = ¬C ∗ (x), (C1 u C2 )∗ = C1∗ (x) ∧ C2∗ (x). The QL1 sentence encoding the knowledge base K is defined as follows: ^ K ‡e ∀x T ∗ (x) ∧ T R (x) ∧ ∧ A‡e .   = R (x) ∧ δR (x) R∈role ± (K) Formulas T ∗ (x), the δR (x), for R ∈ role± (K), and T R (x) encode the TBox T : ^ ^ T ∗ (x) = C1∗ (x) → C2∗ (x) ,   δR (x) = Eq0 R(x) → Eq R(x) , C1 vC2 ∈T q,q 0 ∈QR T, q 0 >q ^ ^ T R (x) = Eq R(x) → Eq R0 (x) ,  Rv∗ 0 R T R q∈QT 0 0 ∗ where QR R T contains 1, all q such that ≥ q R occurs in T and all QT , for R vT R. ‡e Sentence A encodes the ABox A: ^ ^ ^ ^ A‡e = Ak (ai ) ∧ ¬Ak (ai ) ∧ EqR,a e R(a) ∧ ⊥, Ak (ai )∈A ¬Ak (ai )∈A a,a0 ∈ob(A) ¬Pk (ai ,aj )∈A R 0 v∗ 0 0 T R, R (a,a )∈A R(ai ,aj )∈A, Rv∗ T Pk e where qR,a is the maximum number in QR e T such that there are qR,a many distinct ai with Ri (a, ai ) ∈ A and Ri v∗T R. For each R ∈ role ± (K), we also need the following formula expressing the fact that the range of R is not empty whenever its domain is non-empty: R (x) = E1 R(x) → inv (E1 R(dr)), where inv (E1 R(dr)) is E1 Pk− (dp− − k ) if R = Pk and E1 Pk (dpk ) if R = Pk . Lemma 1. A DL-LiteHN bool knowledge base under restriction (inter2) is satisfi- able iff the QL1 -sentence K‡e is satisfiable. Proof. (Sketch) The only challenging direction is (⇐). To prove it, we adapt the proofs of Theorem 5.2 and Lemma 5.14 in [3]. The idea of the proof is to construct a DL-LiteHN ‡e bool interpretation I, from M, the minimal Herbrand model of K . We 1 denote the interpretations of unary predicates P and constants a of QL in M by P M and aM , respectively. Let D = ob(A) ∪ {dpk , dp− k | Pk ∈ Srole(K)} be the ∞ domain of M. Then I = (∆I , ·I ) is defined inductively: ∆I = m=0 Wm , such I that W0 is the set D0 = ob(A), and for every ai ∈ ob(A), ai = aM i . Each set Wm+1 , m ≥ 0, is constructed by adding to Wm fresh copies of certain elements from D \ ob(A). The extensions AIk of concept names Ak are defined by taking AIk = {w ∈ ∆I | M |= A∗k [cp(w)]}, (1) where cp(w) is the element d ∈ D of which w is a copy. S∞ The interpretation for each role Pk , is defined inductively as PkI = m=0 Pkm , where Pkm ⊆ Wm × Wm , along with the construction of ∆I . The initial interpre- tation for each role name Pk is defined as follows: ∗ Pk0 = {(aM M i , aj ) ∈ W0 × W0 | R(ai , aj ) ∈ A and R vT Pk }. (2) For every R ∈ role ± (K), the required R-rank r(R,  d) of d ∈ D is defined by taking r(R, d) = max {0} ∪ {q ∈ QR T | M |= Eq R[d]} . The actual R-rank rm (R, w) of a point w ∈ ∆I at step m is ( ]{w0 ∈ Wm+1 | (w, w0 ) ∈ Pkm+1 }, if R = Pk , rm (R, w) = ]{w0 ∈ Wm+1 | (w0 , w) ∈ Pkm+1 }, if R = Pk− . Assume that Wm and Pkm , m ≥ 0, have been already defined. Let Wm+1 = ∅ and Pkm+1 = ∅, for each role name Pk . If we had rm (R, w) = r(R, cp(w)), for each role R and w ∈ Wm , then the interpretation we need would be constructed. However, the actual rank of some points could still be smaller than the required rank. We cure these defects by adding R-successors for them. Note that the ‘curing’ process for a given w and R, not only increases the actual R-rank of w, but also all its R0 -ranks, for all R v∗T R0 . At this point we adapt the construction in [3] to obtain the interpretation I we are intending. For each Pk ∈ role(K), we consider two sets of defects in Pkm : Λmk = {w ∈ Wm \ Wm−1 | rm (Pk , w) < r(Pk , cp(w))} and Λm−k = {w ∈ W m \ W m−1 | rm (Pk− , w) < r(Pk− , cp(w))}. In each equivalence class [R] = {S | S ≡∗T R} we select a single role, a representative. Let G = (Rep ∗T , E) be a directed graph such that Rep ∗T is the set of representatives and (R, R0 ) ∈ E iff R is a proper sub-role of R0 . Clearly, G is a directed acyclic graph and so, by a topological sort, one can assign to each representative a unique number smaller than the number of all its descendants in G. We use the ascending total order induced on G when choosing an element Pk in Rep ∗T , and extend in that way Wm and Pkm to Wm+1 and Pkm+1 , respectively. 0 (Λm m k ) Let w ∈ Λk , q = r(Pk , cp(w)) − rm (Pk , w), d = cp(w). There is q ≥ q > 0 − − with M |= Eq0 Pk [d]. Then, M |= E1 Pk [d] and M |= E1 Pk [dpk ]. In this case we take q fresh copies w10 , . . . , wq0 of dp−k , add them to Wm+1 and for each 1 ≤ i ≤ q, set cp(wi0 ) = dp−k , add the pairs (w, wi0 ) to each Pjm+1 with Pk v∗T Pj and the pairs (wi0 , w) to each Pjm+1 with Pk− v∗T Pj (note that by adding pairs to Pjm+1 we change its the actual rank); m− − − (Λk ) This rule is the mirror image of (Λm k ): Pk and dpk are replaced with Pk and dpk , respectively. We need to show that, for all w ∈ ∆I and all ≥ q R in T , (a1 ) if ≥ q R occurs positively in T then M |= Eq R[cp(w)] implies w ∈ (≥ q R)I ; (a2 ) if ≥ q R occurs negatively in T then w∈(≥ q R)I implies M |= Eq R[cp(w)]. Consider first w ∈ W0 . It should be clear that actual R-rank of w r0 (R, w) ≤ rank(R, A) + R0 ∈dsubT (R) rank(R0 , T ) P and so, by (inter2), the total number of R-successors before we cure the de- fects does not exceed ubound(R, T ). If ubound(R, T ) = ∞ then there are no negative occurrences of ≥ q R with q ≥ 2 and, although may have rm (R, w) ≥ r(R, cp(w)) after curing the defects of R, both (a1 ) and (a2 ) hold. Otherwise, we have ubound(R, T ) + 1 ∈ QR R T and so, by (inter2), max QT > rank(R, T ) + R rank(R, A), whence r0 (R, w) < max QT . So, as r(R, cp(w)) ≤ lbound(R, T ) and lbound(R, T ) < ubound(R, T ) < max QR T , after curing the defect, we will have rm (R, w) = r(R, cp(w)), for all m > 0, and both (a1 ) and (a2 ) hold. The case with w ∈ Wm0 \ Wm0 −1 , for m0 > 0 is similar, only now rm0 (R, w) ≤ 1 + R0 ∈dsubT (R) rank(R0 , T ). P Finally, we show that I |= ϕ for each ϕ ∈ K. For ϕ = Ak (ai ), ϕ = ¬Ak (ai ) the claim is by the definition of AIk . For ϕ = ¬Pk (ai , aj ), we have (ai , aj ) ∈ PkI iff (ai , aj ) ∈ Pk0 iff R(ai , aj ) ∈ A and R v∗T Pk . By induction on the structure of concepts and (a1 ) and (a2 ), one can show that I |= C1 v C2 whenever M |= ∀x(C1∗ (x) → C2∗ (x)), for each ϕ = C1 v C2 . Finally, I |= ϕ holds by definition in case ϕ = R1 v R2 ∈ T . Theorem 1. Under restriction (inter2), checking KB satisfiability is NP- complete in DL-LiteHN HN bool , PTime-complete in DL-Litehorn and NLogSpace- HN HN complete in both DL-Litekrom and DL-Litecore . We now consider the case where the restriction (inter1) is imposed on the interaction between sub-roles and number restrictions. In presence of an ABox, (inter2) restricts the number of R-successors in the ABox, which appears to be a strong constraint on the instances of the ABox. On the other hand, the less restrictive condition (inter1), which does not impose any bound on R-successors in the ABox, does not come for free, as shown by the following theorem: Theorem 2. Under restriction (inter1), checking KB satisfiability is NP-hard even in DL-LiteHN core . Proof. We show that graph 3-colorability can be reduced to KB satisfiability. Let G = (V, E) be a graph with vertices V and edges E and {r, g, b} be three colors. Consider the following KB K = (T , A) with role names vi and w and object names o, r, g, b and the xi , for each vertex vi ∈ V : T ={≥ (|V | + 4) w v ⊥} ∪ {vi v w, B1 v ∃vi , B2 u ∃vi− v ⊥ | vi ∈ V } ∪ {∃vi− u ∃vj− v ⊥ | (vi , vj ) ∈ E}, A ={B1 (o), w(o, r), w(o, g), w(o, b)} ∪ {w(o, xi ), B2 (xi ) | vi ∈ V }. It can be shown that K is satisfiable iff G is 3-colorable. 4 Reasoning with Attributes In this section we study the effect of extending DL-Lite with attributes. In par- ticular, we show that for the Bool, Horn and core cases the addition of attributes does not change the complexity of KB satisfiability. Theorem 3. KB satisfiability is NP-complete in DL-LiteN A bool , PTime-complete NA NA in DL-Litehorn and NLogSpace-complete in DL-Litecore . Under restriction (inter2), checking KB satisfiability is NP-complete in DL-LiteHN A HN A bool , PTime-complete in DL-Litehorn and NLogSpace-complete in HN A DL-Litecore . Proof. (Sketch) We encode a DL-LiteHN α A KB K = (T , A) in a QL1 sentence ‡a K in a way similar to the translation used in Lemma 1. Denote by val (A) the set of all value names that occur in A. Similarly to roles, we define the sets QU T of natural numbers for all occurrences of ≥ q U (including sub-attributes). We need a unary predicate Eq U (x), for each attribute name U and q ∈ QUT , denoting the set of objects with at least q values of attribute U . We also need, for each attribute name U and each datatype T , a unary predicates U T (x), denoting all objects that may have attribute U values only of datatype T . Following this intuition, we extend ·∗ by the following two statements: (≥ q U )∗ = Eq U (x) and (∀U.T )∗ = U T (x). The QL1 sentence encoding the KB K is defined as follows: ^ 2 K‡a = K‡e ∧ ∀x T U (x) ∧ 1 2 ∧ A ‡a ∧ A ‡a ,   δU (x) ∧ αU (x) ∧ αU (x) U ∈att(K) where K‡e is as before, T U (x), δU (x) and A‡a are similar to T R (x), δR (x) and A‡e , but rephrased for attributes and their inclusions. The new types of ABox assertions require the following formula: 2 ^ ^ ^ A‡a =  U T (ai ) → T vj ∧ T vj , Uk (ai ,vj )∈A datatype T T (vj )∈A where T vj is a propositional variable for each datatype T and each vj ∈ val (A). 1 2 The two additional formulas, αU (x) and αU (x), capturing datatype inclusions and disjointness constraints are: ^ 1 U T (x) → U T 0 (x) ,  αU (x) = T vT 0 ∈T ^  ^ 2 U T (x) ∧ U T 0 (x) ∧ E1 U (x) → ⊥ ∧ T v ∧ T 0v → ⊥ .   αU (x) = T uT 0 v⊥∈T v∈val(A) 2 We would like to note here that the formula αU (x) for disjoint datatypes demon- strates a subtle interaction between attribute range constraints ∀U.T and mini- mal cardinality constraints ∃U . We show that K is satisfiable iff the QL1 -sentence K‡a is satisfiable. For (⇐), let M |= K‡a . We construct a model I = (∆IO ∪ ∆IV , ·I ) of K similarly to the way we proved Lemma 1 but this time datatypes will have to be taken into account: let ∆IO be defined inductively as before and ∆IO = val (A) ∪ V . The set V will be constructed starting from val (A) in order to ‘cure’ the attribute successors as follows. For each datatype T and each attribute U , let T 0 = {v ∈ val (A) | M |= T v} and U 0 = {(a, v) | U (a, v) ∈ A}. For every attribute U ∈ att(K), we can define the required U -rank r(U, d) of d ∈ D and the actual U -rank r0 (R, w) of w ∈ ∆IO as before, treating U as a role name (the only difference is that there will be only one step, and so, the actual rank is needed only for step 0). We can also consider the equivalence relation induced by the sub-attribute relation in T , then we can choose representatives and a linear order on them respecting the sub-attribute relation of T . We can start from the smaller attributes and ‘cure’ their defects. Let w ∈ ∆IO and q = r(U, cp(w)) − r0 (U, w) > 0. Take q fresh elements v1 , . . . , vq , add those fresh values to V , add pairs (w, v1 ), . . . , (w, vq ) to U 0 and add v1 , . . . , vq to T 0 for each datatype T with M |= U T [cp(w)]. Let U I and T I be the resulting relations. Now, it can be shown that if M |= K‡a then I |= ϕ for every ϕ ∈ K. We only note here that fresh values vj cannot be added to two disjoint datatypes T and T 0 because of formula αU 2 (x). Now, given a KB with a Bool or Horn TBox, K‡a is a universal one-variable formula or a universal one-variable Horn formula, respectively, which immedi- ately gives the NP and PTime upper complexity bounds for the Bool and Horn fragments. The NLogSpace upper bound for KBs with core TBoxes is not so 2 straightforward because αU (x) is not a binary clause. In this case we note that K is still a universal one-variable Horn formula and therefore, K‡a is satisfiable ‡a iff it is true in the ‘minimal’ model. The minimal model can be constructed in the bottom-to-top fashion by using only positive clauses of K‡a (i.e., clauses of the form ∀x (B1 (x) ∧ · · · ∧ Bk (x) → H(x))) and then checking whether the negative clauses of K‡a (i.e., clauses of he form ∀x (B1 (x) ∧ · · · ∧ Bk (x) → ⊥)) hold in the constructed model. By inspection of the structure of K‡a , one can see that all its positive clauses are in fact binary, and therefore, whether an atom is true in its minimal model or not can be checked in NLogSpace. It is of interest to note that the complexity of KB satisfiability increases in the case of Krom TBoxes: Theorem 4. KB satisfiability is NP-complete in DL-LiteN A krom , and so, in HN A DL-Litekrom even under (inter) and (inter2). 2 Proof. (Sketch) The proof exploits the ternary disjointness formula αU (x) in K‡a . In fact, if T u T 0 v ⊥ ∈ T then the following concept inclusion, although not in the syntax of DL-LiteN A 2 krom , is a logical consequence of T (cf. αU (x)): ∀U.T u ∀U.T 0 u ∃U v ⊥. Vm Using such ternary intersections one can encode 3SAT. Let ϕ = i=1 Ci be a 3CNF, where the Ci are ternary clauses over variables p1 , . . . , pn . Now, suppose pji1 ∨ ¬pji2 ∨ pji3 is the ith clause of ϕ. It is equivalent to ¬pji1 ∧ pji2 ∧ ¬pji3 → ⊥ and so, can be encoded as follows: Ti1 u Ti2 v ⊥, ¬Aji1 v ∀Ui .Ti1 , Aji2 v ∀Ui .Ti2 , ¬Aji3 v ∃Ui , where the A1 , . . . , An are concept names for the variables p1 , . . . , pn , and Ui is an attribute and Ti1 and Ti2 are datatypes for the ith clause (note that Krom concept inclusions of the form ¬B v B 0 are required, which is not allowed in the core TBoxes). Let T consist of all such inclusions for clauses in ϕ. It can be seen that ϕ is satisfiable iff T is satisfiable. 5 Conclusions We studied two different extensions of the DL-Lite logics. First, local attributes allow to use the same attribute associated to different concepts with different datatype range restrictions. We showed that the extension with attributes is harmless with the only notable exception of the Krom fragment, where the com- plexity rises from NLogSpace to NP. Second, we consider weak syntactic restrictions on interaction between cardi- nality constraints and role inclusions and study their impact on the complexity of satisfiability. For example, under (inter) [3], roles with sub-roles cannot have maximum cardinality constraints. We present two alternative restrictions, which coincide without ABoxes, and show that the complexity of TBox satisfiability under them coincides with the complexity of TBox satisfiability without role in- clusions. However, if we want to preserve complexity of KB reasoning, condition (inter2) imposes a bound on the number R-successors in the ABox. Indeed, under the weaker condition (inter1) complexity of KB satisfiability rises to at least NP (even for the core fragment). As a future work, we intend to fill the gaps in Table 1 and, in particular, to see whether the NP-hardness results have a matching upper bound. We are also working on query answering in the languages with attributes. References 1. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. DL-Lite in the light of first-order logic. In Proc. of the 22nd Nat. Conf. on Artificial Intelligence (AAAI 2007), pages 361–366, 2007. 2. A. Artale, D. Calvanese, and A. Ibáñez-Garcı́a. Full satisfiability of UML class diagrams. In Proc. of the 29th International Conference on Conceptual Modeling (ER-10), 2010. 3. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. The DL-Lite family and relations. J. of Artificial Intelligence Research, 36:1–69, 2009. 4. A. Artale, R. Kontchakov, V. Ryzhikov, and M. Zakharyaschev. Complexity of reasoning over temporal data models. In Proc. of the 29th International Conference on Conceptual Modeling (ER-10), 2010. 5. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. DL-Lite: Tractable description logics for ontologies. In Proc. of the 20th Nat. Conf. on Artificial Intelligence (AAAI 2005), pages 602–607, 2005. 6. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Data com- plexity of query answering in description logics. In Proc. of the 10th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 2006), pages 260–270, 2006. 7. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Inconsis- tency tolerance in P2P data integration: An epistemic logic approach. Information Systems, 33(4):360–384, 2008. 8. A. Poggi, D. Lembo, D. Calvanese, G. De Giacomo, M. Lenzerini, and R. Rosati. Linking Data to Ontologies. J. on Data Semantics, X:133–173, 2008.