Introduction

The DL-Lite family of description logics has recently been proposed and investigated in [5][6][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 official 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-Lite HN 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 values, 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-Lite A [8] is that the range restrictions for attributes can be local (and not only global as in DL-Lite A ). Indeed, DL-Lite HN A α has a possibility to express concept inclusion axioms of the form C ∀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 expressive 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 conceptual 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 satisfiability 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 reasoning 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-Lite N A bool , DL-Lite N A horn and DL-Lite N A core .

2 The Description Logic DL-Lite HN A bool

The language of DL-Lite HN A bool contains object names a 0 , a 1 , . . ., value names v 1 , v 2 , . . ., concept names A 0 , A 1 , . . ., role names P 0 , P 1 , . . ., attribute names U 0 , U 1 , . . ., and datatype names T 0 , T 1 , . . .. Complex roles R and concepts C are defined below:

R ::= P i | P − i , B ::= | ⊥ | A i | ≥ q R | ≥ q U i C ::= B | ¬C | C 1 C 2 ,

where q is a positive integer. The concepts of the form B are called basic concepts.

A DL-Lite HN A bool TBox, T , is a finite set of concept, role, attribute and datatype inclusion axioms of the form:

C 1 C 2 , C ∀U. T, R 1 R 2 , U U , T T , T T ⊥,

and an ABox, A, is a finite set of assertions of the form:

A k (a i ), ¬A k (a i ), P k (a i , a j ), ¬P k (a i , a j ), U k (a i , v j ) and T k (v j ).

We standardly abbreviate ≥ 1 R and ≥ 1 U by ∃R and ∃U , respectively. Absence of an attribute (i.e., C ∀U. ⊥) can be expressed as C ∃U ⊥.

Together, a TBox T and an ABox A constitute the DL-Lite HN A bool 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 {P k , P − k | P k ∈ role(K)}.

Semantics. As usual in description logic, an interpretation, I = (∆ I , • I ), consists of a nonempty domain ∆ I and an interpretation function • I . The interpretation domain ∆ I is the union of two non-empty disjoint sets: the domain of objects ∆ I O and the domain of values ∆ I V . We assume that all interpretations agree on the semantics assigned to each datatype T i , as well as on each constant v i . In particular,

T I i = val(T i ) ⊆ ∆ I V isI k ⊆ ∆ I O × ∆ I V .

We adopt here the unique name assumption (UNA): a I i = a I j , for all i = j. The role and concept constructs are interpreted in I in the standard way:

(P − k ) I = {(y, x) ∈ ∆ I O × ∆ I O | (x, y) ∈ P I k }, (inverse role)I = ∆ I O ,

(domain of objects)

⊥ I = ∅,

(the empty set)

(≥ q R) I = x ∈ ∆ I O | {y | (x, y) ∈ R I } ≥ q ,

(at least q R-successors)

(≥ q U ) I = x ∈ ∆ I O | {v | (x, v) ∈ U I } ≥ q ,

(at least q U -attributes)

(∀U. T ) I = x ∈ ∆ I O | ∀v. (x, v) ∈ U I → v ∈ T I , (attribute value restriction) (¬C) I = ∆ I O \ C I , (not in C) (C 1 C 2 ) I = C I 1 ∩ C I 2 ,

(both in C1 and in C2)

where X is the cardinality of X. The satisfaction relation |= is also standard:

I |= C 1 C 2 iff C I 1 ⊆ C I 2 , I |= R 1 R 2 iff R I 1 ⊆ R I 2 , I |= T 1 T 2 iff T I 1 ⊆ T I 2 , I |= U 1 U 2 iff U I 1 ⊆ U I 2 , I |= T 1 T 2 ⊥ iff T I 1 ∩ T I 2 = ∅, I |= P k (a i , a j ) iff (a I i , a I j ) ∈ P I k , I |= A k (a i ) iff a I i ∈ A I k , I |= ¬P k (a i , a j ) iff (a I i , a I j ) / ∈ P I k I |= ¬A k (a i ) iff a I i / ∈ A I k , I |= U k (a i , v j ) iff (a I i , v I j ) ∈ U I k , I |= T k (v j ) iff v I j ∈ T I k .

A KB K = (T , A) is said to be satisfiable (or consistent) if there is an interpretation, 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).

Fragments of DL-Lite HN A bool

We consider various syntactical restrictions on the language of DL-Lite HN A bool 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 definitions. A TBox T will be called a Krom TBox1 if its concept inclusions are restricted to:

B 1 B 2 , B 1 ¬B 2 and ¬B 1 B 2 ,(Krom)

(here and below all the B i and B are basic concepts). T will be called a Horn TBox if its concept inclusions are restricted to:

k B k B.(Horn)

Finally, we call T a core TBox if its concept inclusions are restricted to: As shown in [3], reasoning in DL-Lite HN α is already rather costly (ExpTimecomplete) 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

B 1 B 2 and B 1 B 2 ⊥. (core) As B 1 ¬B 2 is equivalent to B 1 B 2 ⊥,(R) = P − k if R = P k and inv (R) = P k if R = P − k .

Given a TBox T we denote by * T the reflexive and transitive closure of the relation

{(R, R ), (inv(R), inv(R )) | R R ∈ T }. We say that R ≡ * T R iff R * T R and R * T R. Say that R is a proper sub-role of R in T if R * T R and R * T R . A proper sub-role R of R is said to be a direct sub-role of R if there is no other proper sub-role R of R such that R is a proper sub-role of R ; 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 restriction on DL-Lite HN α 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 ), R ∈dsub T (R) rank (R , T ) , rank (R, A) = max {0}∪{n | R i (a, a i ) ∈ A, R i * T R, for distinct a 1 , . . . , a n } .

Consider the languages obtained from DL-Lite HN α by imposing one of the following 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-Lite HN core NLogSpace [3] NLogSpace [Th.1] DL-Lite HN horn PTime [3] PTime [Th.1] DL-Lite HN krom NLogSpace [3] ≥NP [Th.2] NLogSpace [Th.1] ExpTime [3] DL-Lite HN bool NP [3] NP [Th.1] DL-Lite HN A core NLogSpace [Th.3] NLogSpace [Th.3] DL-Lite HN A horn PTime [Th.3] PTime [Th.3] DL-Lite HN A krom NP [Th.4] ≥NP [Th.2] NP [Th.4] ExpTime DL-Lite HN A bool NP [Th.3] NP [Th.3] DL-Lite N A core NLogSpace [Th.3] DL-Lite N A horn PTime [Th.3] DL-Lite N A krom NA NA NA NP [Th. 4] DL-Lite N 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 example, allow for the specialization of functional roles:

KB K = (T , A) with T = {≥ 2 R ⊥, R 1 R 2 , R 2 R}, and A = {R(a, b), R 1 (a 1 , b 1 ), R 2 (a 2 , b 2 )}

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-Lite HN A α . Table 1 summarizes the obtained complexity results (with numerical parameters q coded in binary).

3 Reasoning in DL-Lite HN α In this section, we investigate the complexity of deciding KB satisfiability in languages DL-Lite HN α under the restrictions (inter1) and (inter2), respectively. We adapt the proof presented in [3], where a DL-Lite HN bool KB K = (T , A) is encoded into a sentence K ‡e in the one-variable first-order logic QL 1 . We use a slightly longer but simpler encoding. Every a i ∈ ob(A) is associated to the individual constant a i of QL 1 , and every concept name A i to the unary predicate A i (x). For each concept ≥ q R in K we introduce a fresh unary predicate E q R(x).

For each role name P k ∈ role ± (K), two individual constants dp k and dp − k are introduced, as representatives of the objects in the domain and range of P k , respectively. The encoding C * of a concept C is defined inductively:

⊥ * = ⊥, (A i ) * = A i (x), (≥ q R) * = E q R(x), * = , (¬C) * = ¬C * (x), (C 1 C 2 ) * = C * 1 (x) ∧ C * 2 (x).

The QL 1 sentence encoding the knowledge base K is defined as follows:

K ‡e = ∀x T * (x) ∧ T R (x) ∧ R∈role ± (K) R (x) ∧ δ R (x) ∧ A ‡e .

Formulas T * (x), the δ R (x), for R ∈ role ± (K), and T R (x) encode the TBox T :

T * (x) = C 1 C 2 ∈T C * 1 (x) → C * 2 (x) , δR(x) = q,q ∈Q R T , q >q E q R(x) → EqR(x) , T R (x) = R * T R q∈Q R T EqR(x) → EqR (x) ,

where Q R T contains 1, all q such that ≥ q R occurs in T and all Q R T , for R * T R. Sentence A ‡e encodes the ABox A:

A ‡e = A k (ai)∈A A k (a i ) ∧ ¬A k (ai)∈A ¬A k (a i ) ∧ a,a ∈ob(A) R * T R, R (a,a )∈A E q e R,a R(a) ∧ ¬P k (ai,aj )∈A R(ai,aj )∈A, R * T P k ⊥,

where q e R,a is the maximum number in Q R T such that there are q e R,a many distinct a i with R i (a, a i ) ∈ A and R i * 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) = E 1 R(x) → inv (E 1 R(dr)), where inv (E 1 R(dr)) is E 1 P − k (dp − k ) if R = P k and E 1 P k (dp k ) if R = P − k . Lemma 1. A DL-Lite HN bool knowledge base under restriction (inter2) is satisfi- able iff the QL 1 -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-Lite HN bool interpretation I, from M, the minimal Herbrand model of K ‡e . We denote the interpretations of unary predicates P and constants a of QL 1 in M by P M and a M , respectively. Let D = ob(A) ∪ {dp k , dp − k | P k ∈ role(K)} be the domain of M. Then I = (∆ I , • I ) is defined inductively: ∆ I = ∞ m=0 W m , such that W 0 is the set D 0 = ob(A), and for every a i ∈ ob(A), a I i = a M i . Each set W m+1 , m ≥ 0, is constructed by adding to W m fresh copies of certain elements from D \ ob(A). The extensions A I k of concept names A k are defined by taking

A I k = {w ∈ ∆ I | M |= A * k [cp(w)]},(1)

where cp(w) is the element d ∈ D of which w is a copy. The interpretation for each role P k , is defined inductively as

P I k = ∞ m=0 P m k , where P m k ⊆ W m × W m ,

along with the construction of ∆ I . The initial interpretation for each role name P k is defined as follows:

P 0 k = {(a M i , a M j ) ∈ W 0 × W 0 | R(a i , a j ) ∈ A and R * T P k }.(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 ∈ Q R T | M |= E q R[d]} . The actual R-rank r m (R, w) of a point w ∈ ∆ I at step m is r m (R, w) = {w ∈ W m+1 | (w, w ) ∈ P m+1 k }, if R = P k , {w ∈ W m+1 | (w , w) ∈ P m+1 k }, if R = P − k .

Assume that W m and P m k , m ≥ 0, have been already defined. Let W m+1 = ∅ and P m+1 k = ∅, for each role name P k . If we had r m (R, w) = r(R, cp(w)), for each role R and w ∈ W m , 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 R -ranks, for all R * T R . At this point we adapt the construction in [3] to obtain the interpretation I we are intending. For each P k ∈ role(K), we consider two sets of defects in P m k :

Λ m k = {w ∈ W m \ W m−1 | r m (P k , w) < r(P k , cp(w))} and Λ m− k = {w ∈ W m \ W m−1 | r m (P − k , w) < r(P − k , 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, R ) ∈ E iff R is a proper sub-role of R . 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 P k in Rep * T , and extend in that way W m and P m k to W m+1 and P m+1 k , respectively.

(Λ m k ) Let w ∈ Λ m k , q = r(P k , cp(w)) − r m (P k , w), d = cp(w). There is q ≥ q > 0 with M |= E q P k [d]. Then, M |= E 1 P k [d] and M |= E 1 P − k [dp − k ].

In this case we take q fresh copies w 1 , . . . , w q of dp − k , add them to W m+1 and for each 1 We need to show that, for all w ∈ ∆ I and all ≥ q R in T ,

≤ i ≤ q, set cp(w i ) = dp − k ,(a 1 ) if ≥ q R occurs positively in T then M |= E q R[cp(w)] implies w ∈ (≥ q R) I ; (a 2 ) if ≥ q R occurs negatively in T then w∈(≥ q R) I implies M |= E q R[cp(w)]. Consider first w ∈ W 0 . It should be clear that actual R-rank of w r 0 (R, w) ≤ rank(R, A) + R ∈dsub T (R) rank(R , T )

and so, by (inter2), the total number of R-successors before we cure the defects 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 r m (R, w) ≥ r(R, cp(w)) after curing the defects of R, both (a 1 ) and (a 2 ) hold. Otherwise, we have ubound(R,

T ) + 1 ∈ Q R T and so, by (inter2), max Q R T > rank(R, T ) + rank(R, A), whence r 0 (R, w) < max Q R T . So, as r(R, cp(w)) ≤ lbound(R, T ) and lbound(R, T ) < ubound(R, T ) < max Q R

T , after curing the defect, we will have r m (R, w) = r(R, cp(w)), for all m > 0, and both (a 1 ) and (a 2 ) hold. The case with w ∈ W m0 \ W m0−1 , for m 0 > 0 is similar, only now

r m0 (R, w) ≤ 1 + R ∈dsub T (R) rank(R , T ).

Finally, we show that I |= ϕ for each ϕ ∈ K. For ϕ = A k (a i ), ϕ = ¬A k (a i ) the claim is by the definition of A I k . For ϕ = ¬P k (a i , a j ), we have (a i , a j ) ∈ P I k iff (a i , a j ) ∈ P 0 k iff R(a i , a j ) ∈ A and R * T P k . By induction on the structure of concepts and (a 1 ) and (a 2 ), one can show that

I |= C 1 C 2 whenever M |= ∀x(C * 1 (x) → C * 2 (x)), for each ϕ = C 1 C 2 . Finally, I |= ϕ holds by definition in case ϕ = R 1 R 2 ∈ T .

Theorem 1. Under restriction (inter2), checking KB satisfiability is NPcomplete in DL-Lite HN bool , PTime-complete in DL-Lite HN horn and NLogSpacecomplete in both DL-Lite HN krom and DL-Lite HN core .

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-Lite HN 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 v i and w and object names o, r, g, b and the x i , for each vertex v i ∈ V :

T ={≥ (|V | + 4) w ⊥} ∪ {v i w, B 1 ∃v i , B 2 ∃v − i ⊥ | v i ∈ V } ∪ {∃v − i ∃v − j ⊥ | (v i , v j ) ∈ E}, A ={B 1 (o), w(o, r), w(o, g), w(o, b)} ∪ {w(o, x i ), B 2 (x i ) | v i ∈ V }.

It can be shown that K is satisfiable iff G is 3-colorable.

Reasoning with Attributes

In this section we study the effect of extending DL-Lite with attributes. In particular, 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-Lite N A bool , PTime-complete in DL-Lite N A

horn and NLogSpace-complete in DL-Lite N A core . Under restriction (inter2), checking KB satisfiability is NP-complete in DL-Lite HN A bool , PTime-complete in DL-Lite HN A horn and NLogSpace-complete in DL-Lite HN A core .

Proof. (Sketch) We encode a DL-Lite HN A α KB K = (T , A) in a QL 1 sentence K ‡a 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 Q U T of natural numbers for all occurrences of ≥ q U (including sub-attributes). We need a unary predicate E q U (x), for each attribute name U and q ∈ Q U T , 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 ) * = E q U (x)

and (∀U.T ) * = U T (x).

The QL 1 sentence encoding the KB K is defined as follows:

K ‡a = K ‡e ∧ ∀x T U (x) ∧ U ∈att(K) δ U (x) ∧ α 1 U (x) ∧ α 2 U (x) ∧ A ‡a ∧ A ‡ 2 a ,

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:

A ‡ 2 a = U k (ai,vj )∈A datatype T U T (a i ) → T v j ∧ T (vj )∈A T v j ,

where T v j is a propositional variable for each datatype T and each v j ∈ val (A). The two additional formulas, α 1 U (x) and α 2 U (x), capturing datatype inclusions and disjointness constraints are:

α 1 U (x) = T T ∈T U T (x) → U T (x) , α 2 U (x) = T T ⊥∈T U T (x) ∧ U T (x) ∧ E 1 U (x) → ⊥ ∧ v∈val(A) T v ∧ T v → ⊥ .

We would like to note here that the formula α 2 U (x) for disjoint datatypes demonstrates a subtle interaction between attribute range constraints ∀U.T and minimal cardinality constraints ∃U .

We show that K is satisfiable iff the QL 1 -sentence K ‡a is satisfiable. For (⇐), let M |= K ‡a . We construct a model I = (∆ I O ∪ ∆ I V , • I ) of K similarly to the way we proved Lemma 1 but this time datatypes will have to be taken into account: let ∆ I O be defined inductively as before and ∆ I O = 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 r 0 (R, w) of w ∈ ∆ I O 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 ∈ ∆ I O and q = r(U, cp(w)) − r 0 (U, w) > 0. Take q fresh elements v 1 , . . . , v q , add those fresh values to V , add pairs (w, v 1 ), . . . , (w, v q ) to U 0 and add v 1 , . . . , v q 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 v j cannot be added to two disjoint datatypes T and T because of formula α 2 U (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 immediately 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 straightforward because α 2 U (x) is not a binary clause. In this case we note that K ‡a is still a universal one-variable Horn formula and therefore, K ‡a is satisfiable 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

(B 1 (x) ∧ • • • ∧ B k (x) → H(x))

) and then checking whether the negative clauses of K ‡a (i.e., clauses of he form ∀x

(B 1 (x) ∧ • • • ∧ B k (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-Lite N A krom , and so, in DL-Lite HN A krom even under (inter) and (inter2).

Proof. (Sketch) The proof exploits the ternary disjointness formula α 2 U (x) in K ‡a . In fact, if T T ⊥ ∈ T then the following concept inclusion, although not in the syntax of DL-Lite N A krom , is a logical consequence of T (cf. α 2 U (x)):

∀U.T ∀U.T ∃U ⊥.

Using such ternary intersections one can encode 3SAT. Let ϕ = m i=1 C i be a 3CNF, where the C i are ternary clauses over variables p 1 , . . . , p n . Now, suppose p j 1 i ∨ ¬p j 2 i ∨ p j 3 i is the ith clause of ϕ. It is equivalent to ¬p j 1 i ∧ p j 2 i ∧ ¬p j 3 i → ⊥ and so, can be encoded as follows:

T 1 i T 2 i ⊥, ¬A j 1 i ∀U i .T 1 i , A j 2 i ∀U i .T 2 i , ¬A j 3 i ∃U i ,

where the A 1 , . . . , A n are concept names for the variables p 1 , . . . , p n , and U i is an attribute and T 1 i and T 2 i are datatypes for the ith clause (note that Krom concept inclusions of the form ¬B B 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.

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 complexity rises from NLogSpace to NP.

Second, we consider weak syntactic restrictions on interaction between cardinality 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 inclusions. 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.