Finite Model Reasoning in DL-Lite with Cardinality Constraints? (Preliminary Results) Yazmı́n Ibáñez-Garcı́a KRDB Research Centre Free University of Bozen-Bolzano, Italy ibanezgarcia@inf.unibz.it 1 Introduction The relationship of description logics (DLs) and conceptual modelling has been extensively studied in the literature [5, 4, 1]. One of the advantages of using de- scription logics as modelling languages is that along with their capability of representing knowledge they provide also reasoning services. More precisely, a conceptual model can be represented by a DL ontology (TBox), and standard reasoning services (e.g., satisfiability and subsumption) allow to verify some properties of the conceptual model (e.g., consistency) and infer relations between concepts (IS-A relationships between classes or entities) that are not explicitly expressed. In order to use DLs effectively for conceptual modelling we need to ensure (1) that the chosen DL language is expressive enough to capture faith- fully the intended semantics of traditional modelling languages (e.g., UML class diagrams, ER schema), and (2) that the complexity of reasoning in the chosen DL is acceptable (e.g., tractable). Regarding (1), it is worth noticing that the domain of interest in most applications is finite, therefore, reasoning on concep- tual models should be understood as reasoning w.r.t. finite models. The latter is not the usual assumption in DLs mainly because traditional description logics enjoy the finite model property (FMP), and hence there is no need to distinguish between reasoning w.r.t. arbitrary models, and w.r.t. finite ones. Notably, ALC (one of the traditional DLs) is not expressive enough for capturing cardinality constraints. In DLs cardinality constraints are expressed by (qualified) number restrictions. ALCQI –which extends ALC with qualified number restrictions and inverse roles– captures the semantics of UML class diagrams [4]. However, this extension of ALC does not enjoy the FMP any more. One drawback for the use of ALCQI is the complexity of reasoning: finite satisfiability of ALCQI knowledge bases is ExpTime-complete [11]. The high complexity of reasoning makes ALCQI not very attractive for the conceptual modelling task; specially because no optimized algorithms for finite model reasoning exist. As an alterna- tive, members of the DL-Lite-family of description logics including unqualified ? We would like to thank the anonymous reviewers, as well as Alessandro Artale, André Hernich, and Vı́ctor Gutiérrez-Basulto for valuable remarks to improve the final version of this paper. number restrictions [2] capture relevant modelling features [1]. However, little has been done in the study of the complexity of reasoning w.r.t. finite models in DL-Lite [13]. A consideration around the use of number restrictions (qualified or unqualified) regards their semantics: on the DL side, number restrictions, in- tended for possible infinite model semantics, constraint the numbers of objects that are related to a certain object; while cardinality constraints in conceptual modelling, intended for finite model semantics, establish relationships among the cardinality of classes/entities. The purpose of this paper is to bring attention to finite model reasoning in description logics from a model theoretical view point. We adapt existing techniques [6] and show that the complexity of finite model reasoning in the Horn fragment of DL-Lite is tractable when only global functionality constraints are considered. While this result seems to be an almost straightforward con- sequence of existing results [13]; the approach taken in this paper leads to a deeper understanding of the structural properties of finite models for DL-Lite knowledge bases. We also observe that when allowing the use of arbitrary cardi- nality constraints, finite satisfiability becomes harder than arbitrary reasoning in DL-LiteNhorn . In Section 5 we provide an intuition for an upper bound on the complexity of finite model reasoning in DL-LiteN horn . The results and observa- tions presented in this paper shall serve as the foundation for future work on the finite model theory in light weight description logics [2, 3]. 2 Preliminaries DL-Lite syntax and semantics The language of DL-LiteN horn contains individ- ual names a0 , a1 , . . ., concept names A0 , A1 , . . ., role names P0 , P1 , . . ..Complex roles R, and concepts B are built according to the following syntax rule: R ::= Pi | Pi− , B ::= ⊥ | Ai | ≥ n R, where n in number restrictions (≥ n R) is a positive integer. We call existentials those number restrictions with n = 1, denoted also by ∃R. A DL-LiteN horn -TBox T is a finite set of axioms of the form B1 u · · · u Bk v B, k ≥ 0, where by definition the empty conjunction is >. We also consider the sublogic DL-LiteF horn , which of all number restrictions only allows for existentials, and those with n = 2 occurring only in concept inclusions of the form ≥ 2 R v ⊥, which are called global functionality constraints, and are denoted by (funct R). An ABox A is a finite set of assertions of the form: A(ai ) or P (ai , aj ). Together, a TBox T and an ABox A constitute a DL-LiteF horn knowledge base(KB) K = (T , A). We use ind (A) to denote the set of individual names occurring in A; role(K) the set of role names in K, and role ± (K) the set of roles {Pk , Pk− | Pk ∈ role(K)}. For a role R ∈ role ± (K), R− = Pk if R = Pk− , and R− = Pk− if R = Pk . Finally, concepts(K) denotes the set of basic concepts occurring in K, and concepts(T ), for those occurring in T . An interpretation I = (∆I , ·I ) consists of a non-empty domain ∆I , and an interpretation function ·I that assigns to each individual name ai an element aIi ∈ ∆I ; to each concept name Aj a subset AIj ⊆ ∆I , and to each role name Pk , a binary relation PkI ⊆ ∆I × ∆I . The interpretation function is extended to concepts and roles as follows: (Pk− )I = {(e, d) ∈ ∆I × ∆I | (d, e) ∈ PkI }; (inverse role) I I > = ∆ ; (Top) ⊥I = ∅; (Bottom) I I I I (≥ n R) = {d ∈ ∆ | ]{e ∈ ∆ | (d, e) ∈ R } ≥ n}; (number rest.) I (Bi u Bj ) = BiI ∩ BjI ; (conjunction) where d ] denotes the cardinality of a set. An interpretation I satisfies d a TBox axiom k Bk v B iff ( k Bk )I ⊆ B I , in that case we write I |= k Bk v B; d similarly, I |= (funct R) iff whenever both (d, e) ∈ RI and (d, e0 ) ∈ RI , then e = e0 . For ABox assertions we have that I |= A(ai ) iff aIi ∈ AI ; and I |= Pk (ai , aj ) iff (aIi , aIj ) ∈ PkI . A knowledge base K = (T , A) is satisfiable (or consistent) if there is an interpretation I, satisfying every axiom in T and every assertion in A. In this case we write I |= K (as well as I |= T , and I |= A), and we say that I is a model of K (and of T and A). If I is finite (i.e., its domain is finite) we say that a K (as well as T and A) is finitely satisfiable. The type of d in I is the set tI (d) = {B | d ∈ B I }, where B is a DL-LiteN horn -concept. The set of all types of I, is types(I) = {tI (d) | d ∈ ∆I }. We consider standard reasoning tasks. Specifically, satisfiability and subsumption. Let L ∈ {DL-LiteF N horn , DL-Litehorn }. The satisfiability problem consists on deciding, given an L-KB K, whether K is satisfiable; while the subsumption problem amounts to decide, given an L-TBox T and L-concepts C1 and C2 , whether T |= C1 v C2 , i.e., whether C1I ⊆ C2I in every model I of T . 3 Model Theoretical Characterizations Lutz et. al., [10] provide a model theoretical characterization of DL-Litehorn (without number restrictions) based on (equi)simulation, a weaker notion of the classical (bi)simulation [7]. In order to capture the counting capability of DL-LiteNhorn we extend this notion similarly to the graded-bisimulation in [12]. For a DL-LiteN I horn interpretation I, an object d ∈ ∆ , and a role R, R-succI (d) = {e ∈ ∆I | (d, e) ∈ RI } is the set of R-successors of d in I. Let I1 = (∆I1 , ·I1 ) and I2 = (∆I2 , ·I2 ) be two DL-LiteN horn interpretations. A graded equisimulation(or g-equisimulation) between I1 and I2 is a relation ρ ⊆ ∆I1 × ∆I2 that satisfies the following properties: (atom) for every concept name A, if (d, e) ∈ ρ then d ∈ AI1 iff e ∈ AI2 ; (role) for every role R, if (d, e) ∈ ρ, then the following hold: (i) for every finite set S ⊆ R-succI1 (d), there exists a finite set S 0 ⊆ R-succI2 (e), such that ]S = ]S 0 ; and (ii) for every finite set S ⊆ R-succI2 (e), there exists a finite set S 0 ⊆ R-succI1 (d), such that ]S = ]S 0 .1 ρ is called global if and only if (i) for every d ∈ ∆I1 there is some e ∈ ∆I2 with (d, e) ∈ ρ, (ii) for every e ∈ ∆I2 there is some d ∈ ∆I1 with (d, e) ∈ ρ. We write (I1 , d) ≈ (I2 , e) if there exists a g-equisimulation ρ between I1 and I2 such that (d, e) ∈ ρ. Finally, we say that I1 is g-equisimilar to I2 , denoted as I1 ≈ I2 , if there is a global g-equisimulation ρ between I1 and I2 . Lemma 1. Let T be a DL-LiteN N horn TBox, C a DL-Litehorn concept; and I1 N and I2 be two DL-Litehorn interpretations over the signature of T and C. The following statements hold: (a) DL-LiteN horn concepts are invariant under g-equisimulations: (I1 , d) ≈ (I2 , e) implies d ∈ C I1 iff e ∈ C I2 . (b) DL-LiteN horn TBoxes are invariant under global g-equisimulations: if I1 ≈ I2 then I1 |= T iff I2 |= T . (c) Every model of a DL-LiteN horn TBox is g-equisimilar to a tree-shaped model. Canonical Models We use a standard characterization of unrestricted en- tailment in terms of canonical models [8]. A canonical interpretation for a DL-LiteN horn KB K = (T , A) is constructed by (i) expanding the set of indi- vidual names in A with an additional set of individuals {dR | R ∈ role ± (T )} that serve as witness of existentials, and (ii) expanding the extensions of concept and role names as required by T . A role R is called generating in K if there exist a ∈ ind (A) and R0 , . . . , Rn = R such that the following conditions hold: (agen) K |= ∃R0 (a) but R0 (a, b) 6∈ A for all b ∈ ind (A) (written a ; dR− ). 0 (rgen) For i < n, T |= ∃Ri− v ∃Ri+1 and Ri− 6= Ri+1 (written dR− ; dR− ). i i+1 Definition 1. Let K = (T , A) be a DL-LiteN horn KB. The canonical interpreta- tion IK = (∆IK , ·IK ) of K is defined as follows: ∆IK = ind (A) ∪ {dR | R− is generating in K}; aIK = a for every a ∈ ind (A); AIK = {a ∈ ind (A) | K |= A(a)} ∪ {dR ∈ ∆IK | T |= ∃R v A}; K P I = {(ai , aj ) ∈ ind (A) × ind (A) | P (ai , aj ) ∈ A}∪ {(a, dP − ) | a ; dP − } ∪ {(dP , a) | a ; dP }∪ {(dS , dP − ) | dS ; dP − } ∪ {(dP , dS ) | dS ; dP }. The canonical interpretation IK of a given KB K can be computed in polynomial time on the size of K [8], and serves as a finite compact representation of every model of K. However, IK is not itself in general a model of K, as the following example shows: 1 Clearly, if both R-succI1 (d) and R-succI2 (e) are finite, these conditions are equiva- lent to ]R-succI1 (d) = ]R-succI2 (e). Example 1. Let K = (T , A), where T = {∃S v ∃P1 , ∃P1− v ∃P2 , ∃P2− v ∃P1 , ∃P2− v ∃P3− , ∃P3 v ∃S − (funct P1− ), (funct P2− ), (funct S), B v ∃P1 }, and A = {B(a)}. The canonical interpretation IK , depicted in Figure 1, clearly violates the func- tionality of P1− and hence is not a model of K. In general, IK cannot be a model of K since it is finite, and DL-LiteN horn does not enjoy the finite model property (FMP). A standard way to construct a (canonical) model from IK is to unravel it into a forest-shaped interpretation UK [2, 8]. We omit the definition of UK here and focus only in its properties: Lemma 2. Let K be a DL-LiteN horn knowledge base, and UK the unravelling of the canonical interpretation IK , then the following hold: (p1) K is satisfiable iff UK |= K. (p2) For every DL-LiteN horn TBox axiom ϕ, K |= ϕ iff UK |= ϕ. 4 Finite Model Reasoning in DL-LiteF horn In this section, we study finite model reasoning in DL-LiteFhorn . Notably, the FMP it is already lost when considering only functionality constraints. Let us take the following DL-LiteF horn KB to illustrate this: K0 = (T ∪ {B u ∃P2− v ⊥}, A) (1) with T and A from Example 1. It is not hard to see that K0 is satisfiable only by infinite models. Intuitively, in every model I of K0 , there is an infinite sequence of objects connected by P1 and P2 starting from aI : since a is an instance of B, aI has a P1 -successor, d1 , and from ∃P1− v ∃P2 , d1 has a P2 successor different from aI (from B u ∃P2− v ⊥), say d2 , from ∃P2− v ∃P1 , d2 has a P1 -successor, d3 , different from d1 , (since P1− is functional), and d3 has a P2 -successor, d4 , different from d2 (since P2− is functional). These arguments can be used repeatedly to see that indeed an infinite number of objects are needed to satisfy the constraints in K0 . In order to provide a method for reasoning in DL-LiteF horn w.r.t. finite models, we follow the approach taken by Cosmadakis et. al., [6] for characterizing finite implication of unary inclusion dependencies (UINDS) and functionality depen- dencies in databases. Given a DL-LiteF horn -KB K = (T , A), we show that it is possible to ‘enrich’ T in such a way that it explicitly contains concept inclusions and functionality constraints that hold in every finite model of T . We adapt the idea behind the axiomatization presented by Cosmadakis et. al., [6], and define a closure of a given TBox T in terms of arbitrary reasoning. Differently from what is done by Rosati [13], we do not exclude disjointness axioms of the form B1 u . . . u Bk v ⊥ from T for defining such a closure. To simplify the presentation we consider an extension of DL-LiteF horn with axioms of the form Bi ≥ Bj , with the following intended semantics for finite models: a finite interpretation I satisfies Bi ≥ Bj if and only if ](Bj )I ≥ ](Bj )I . Definition 2. For a given DL-LiteF horn TBox T , finClosure(T ) denotes the min- imal set of axioms satisfying the following conditions: 1. T ⊆ finClosure(T ); 2. For every pair of basic concepts B1 , B2 occurring in T . If finClosure(T ) |= B1 v B2 , then B2 ≥ B1 ∈ finClosure(T ); 3. if (funct R) ∈ finClosure(T ) then ∃R ≥ ∃R− ∈ finClosure(T ); 4. if {B1 ≥ B2 , B2 ≥ B3 } ⊆ finClosure(T ) then B1 ≥ B3 ∈ finClosure(T ); 5. if {(funct R), ∃R− ≥ ∃R} ⊆ finClosure(T ) then (funct R− ) ∈ finClosure(T ); 6. if finClosure(T ) |= B1 v B2 , and B1 ≥ B2 ∈ finClosure(T ) then B2 v B1 ∈ finClosure(T ). From 1, it follows that every model of finClosure(T ) is also a model of T . Since TBox reasoning in DL-LiteF horn is PTime-complete [2], the following holds: Proposition 1. finClosure(T ) can be computed in polynomial time on the size of T . (1)-(4) in Definition 2 are based in logical consequences and are therefore sound w.r.t. arbitrary models. (5) and (6), on the other hand, are not sound w.r.t. infinite models, but a simple counting argument shows that they are sound w.r.t. finite models. Hence, we have the following result: Lemma 3. Let T be a DL-LiteF horn -TBox. Then, the following hold: d d (a) if finClosure(T ) |= k Bk v B then T |=fin k Bk v B; (b) if (funct R) ∈ finClosure(T ) then T |=fin (funct R). Moreover, the introduction of axioms of the form Bi ≥ Bj , induces a directed graph (V, E), with V the set of concepts occurring in T and (Bi , Bj ) ∈ E iff Bi ≥ Bj ∈ finClosure(T ). The implications w.r.t. finite models can be better understood by observing the structure of (V, E). Example 2 (finClosure). Consider the TBox T from Example 1. finClosure(T ) contains (among others) the axioms T1 = {∃P2 v ∃P1− , ∃P1 v ∃P2− , (funct P1 ), (funct P2 )}. Figure 2 shows a portion of the graph induced by finClosure(T ). The dashed lines represent ‘≥’ inferred by concept inclusions, and the solid lines are ‘≥’ introduced by functionality assertions (rules 2–4). From a solid (dashed) edge (Bi , Bj ) belonging to a cycle, it is inferred a solid (dashed) edge (Bj , Bi ) (rules 5–6). In the example, from the edge (dP1 , d− P2 ), corresponding to the axiom ∃P2− v ∃P1 , it is inferred that ∃P1 v ∃P2− ∈ finClosure(T ). Analogously, from the solid line labelled with P1− , corresponding to (funct P1− ) it is inferred that (funct P1 ). If there is an unsatisfiable concept Bi , this is reflected by an axiom of the form ⊥ ≥ Bi . Let us consider K0 from (1). We have that from the ‘cycle rules’, ∃P1 v ∃P2− ∈ finClosure(T 0 ). Hence, finClosure(T 0 ) |= {∃P1 v ∃P2− , B v ∃P1 , B u ∃P2− v ⊥}, which implies that finClosure(T 0 ) |= B v ⊥, and then, by rule 1, ⊥ ≥ B ∈ finClosure(T 0 ) (see Figure 3). This means that in every finite model I of T 0 , ]B I = 0. An inconsistency w.r.t. finite models is then derived from the ABox assertion B(a). P1 S d P1 d P1 dS dS P1 P1 B dS a d P1 S d P3 P2 P1 d P2 d P2 B P2 d P2 d P3 P3 d P3 Fig. 1: IK with K = (T , A) Fig. 2: finClosure(T ) P1 S d P1 d P1 dS dS P1 dS d P3 P1 d P2 d P2 B d P1 d P2 d P2 d P1 P2 S P2 P2 d P3 ? d P3 P3 Fig. 3: finClosure(T 0 ) Fig. 4: ITb P1 d' P2 P2 P3 P3 P1 d P3 d P3 P1 P2 S S dS dS Fig. 5: UTb S dS P2 P1 P2 d' d P3 P3 P1 P3 Fig. 6: ITf We proceed to prove that finClosure is complete. More precisely, we show the following: Lemma 4. Let T be a DL-LiteF F horn -TBox, and ϕ a DL-Litehorn axiom on the signature of T , i.e., ϕ is either a concept inclusion or a functionality constraint. If T |=fin ϕ then finClosure(T ) |= ϕ. Proof. We shall show that finClosure(T ) 6|= ϕ implies T 6|=fin ϕ. In what follows, we fix a DL-LiteF horn -TBox T , and set T = finClosure(T ). Then, by Lemma 2- b (p2), it suffices to show that UTb 6|= ϕ implies T 6|=fin ϕ, where UTb is the un- ravelling of a canonical interpretation ITb that depends on ϕ. Specifically, if ϕ = C v B, then the ‘root’ of UTb is an object d ∈ C UTb \ B UTb . On the other hand, if ϕ = (funct R), then UTb is rooted at an object d with two different R-successors e and e0 . Let us consider the case ϕ = C v B. We construct a finite model ITf of T such that UTb 6|= C v B implies ITf 6|= C v B. But first, we introduce some useful notation. For any two concepts B1 , B2 , we write B1 vTb B2 whenever Tb |= B1 v B2 ; and B1 ≡Tb B2 , if additionally B2 vTb B1 . Since ≡Tb is an equivalence relation, the set of concepts E = {∃R | R ∈ role ± (Tb )} can be partitioned into equivalence classes w.r.t. ≡Tb . Then, [∃R] ∈ E/ ≡Tb denotes the following equivalence class of concepts: [∃R] = {Bi ∈ E | Bi ≡Tb ∃R}. Before moving forward with the definition of ITf , we observe that the canonical interpretation ITb constructed as in Definition 1 may introduce multiple witnesses for a given existential. We set ds = d0s whenever ∃S ≡Tb ∃S 0 . Therefore, domain of the canonical interpretation ITb contains exactly one element dS for each class [∃S] ∈ E/ ≡Tb (e.g., as in Figure 4). R We write [∃Si ] −→ [∃Sj ] iff ∃Si vTb ∃R and ∃R− ∈ [∃Sj ]. Analogously, ∃Si ≥Tb ∃Sj denotes that ∃Si ≥ ∃Sj ∈ Tb . We observe that ≥Tb induces a coarser partition on E. For a concept ∃Si ∈ E, the cluster of ∃Si is the set C(∃Si ) = {∃Sj ∈ E | ∃Si ≥Tb ∃Sj and ∃Sj ≥Tb ∃Si }. In particular, for every two concepts ∃Si , ∃Sj ∈ E, if ∃Si ≡Tb ∃Sj then ∃Si ∈ C(Sj ); but the implication on the other direction does not hold. Intu- itively, if ∃Si , ∃Sj belong to the same cluster, then their extensions have the same cardinality in every finite model of Tb , and of T . Further, we use [∃Si ]  [∃Sj ] to denote the fact that there exist concepts ∃R ∈ [∃Si ] and ∃R0 ∈ [∃Sj ] such that ∃R ≥Tb ∃R0 , but ∃R0 6≥Tb ∃R, i.e., ∃R0 6∈ C(∃R). For example, in the TBox T from Example 2, [∃P1− ]  [∃S]. Notably, ∃P1− ≥Tb ∃S, but ∃S 6∈ C(∃P1− ) = {∃P1 , ∃P1− , ∃P2 , ∃P2− }. It is also the case that [∃P1− ] 6 [∃P2 ], since C(∃P1− ) = C(∃P2 ). For constructing the domain of the desired finite model ITf , we define the set of finite paths of ITb . σ = (dS0 · · · dSk ) ∈ finpaths(ITb ) iff σ satisfies the following conditions: R 1. [∃Si ] −→ [∃S 0 ], for some role R, such that : (a) (funct R− ) ∈ Tb , (b) [∃Si+1 ] ∈ C(∃S 0 ), and (c) ∃R 6∈ [∃Si+1 ] 2. [∃Si+1 ]  [∃Si ] Intuitively, by condition (1a) a path (σ · d− R ) can be ‘reused’ as a witness of an existential ∃R, whenever the inverse of R is not functional, otherwise a new object (σ 0 ·d− R ) is needed as a witness. Condition (1b) ensures that whenever such a witness path (σ ·dS 0 ) belongs to finpaths(ITb ), then also witnesses (σ ·dRi +1 ) for each class [∃Ri+1 ] in the cluster C(∃S 0 ) belong to finpaths(ITb ); condition (1c) avoids to include a witness that is already realized by tail (σ). Moreover, by condition 2 the length of every path is bounded, and since E is finite, then finpaths(ITb ) is a also finite. We consider a subset of finpaths(ITb ) as the domain of ITf that it is determined by ϕ = C v B. More specifically, for σ = dS · σ 0 ∈ finpaths(ITb ), we write ϕ ; σ iff there is a sequence of roles R0 , . . . , Rn such that: 1. C u ¬B v ∃R0 , ∃S ∈ [∃Rn− ]; i R 2. for i ≤ n, ∃Ri ∈ [∃Si ], [∃Si ] −→ [∃Si+1 ], and ∃Ri 6∈ [∃Si+1 ]; − 3. either (funct Ri ) 6∈ Tb or [∃Si+1 ] 6 [∃Si ]. f We are ready now to define ITf . We set ∆IT = {σ ∈ finpaths(ITb ) | ϕ ; σ}. For f f f f each concept name A, AIT ⊆ ∆IT , and for each atomic role P , P ⊆ (∆IT ×∆IT ), such that: f f AIT ={σ ∈ ∆IT | tail (σ) vTb A}; f I P Pk T ={((σ · dSi ), (σ · dSi dSj )) | [∃Si ] −→ [∃Sj ]} P− ∪ {((σ · dSi dSj ), (σ · dSi )) | [∃Sj ] −→ [∃Si ]} ∪ {(dϕ , (d− P · σ)) | ϕ v ∃P } ∪ {((d− − P · σ), dϕ ) | ϕ v ∃P } ∪ {((σ · dP ), (σ 0 , d− 0 − P )) | σ 6= σ , (funct P ) 6∈ T }. b As an example, consider the model ITf , shown in Figure 6 for the TBox T from Example 2. We claim that ITf and UTb are g-equisimilar. Indeed, a global g-equisimulation ρ can be defined by (σ, γ) ∈ ρ iff tail (γ) = dR , tail (σ) = dS and ∃R ∈ [∃S]. Since UTb |= Tb , by Lemma 1(b), ITf |= Tb ; and since T ⊆ Tb , ITf |= T . More- over, ITf is as desired: ITf 6|= C v B, since by construction tI f (dϕ ) = tUTb (dϕ ). T Finally, the case for ϕ = (funct R), can be handled by a slight modification of the previous construction. Essentially, we substitute dϕ in the previous construction by a witness dR with two R-successors. From Lemma 3 and Lemma 4 we conclude that finite model TBox reasoning in DL-LiteF horn can be reduced to arbitrary TBox reasoning. Theorem 1. For a given DL-LiteF horn TBox T , concepts C1 and C2 . We have that the following hold: 1. T is finitely satisfiable iff finClosure(T ) is satisfiable. 2. T |=fin C1 v C2 iff finClosure(T ) |= C1 v C2 . Next, we show that the complexity of finite model reasoning in DL-LiteF horn remains in PTime, when considering also an ABox, i.e., the following hold: Theorem 2. Let K = (T , A) be a DL-LiteFhorn KB. Then K is finitely satisfiable iff (finClosure(T ), A) is satisfiable. Thus, the complexity of reasoning in DL-LiteF horn coincides for finite and arbi- trary models. Theorem 3. Finite model reasoning in DL-LiteF horn is PTime-complete. As pointed out in Section 3 the canonical interpretation of a knowledge base K constructed as in Definition 1 it is not in general a model of K, due to the presence of functionality constraints (and arbitrary number restrictions in gen- eral). The latter observation provides an intuition for the construction of ITf . Intuitively, ITb can be transformed into a finite model by creating ‘copies’ of cer- tain portions (clusters) in order to resolve violations to functionality constraints; then, although the number of R-successors of some objects in the model increases (specifically for those roles R in the TBox such that (funct R) 6∈ Tb ), this does not trigger any inconsistency, because the expressive power of DL-LiteF horn al- lows only to distinguish between two types of objects: those with exactly one R-successor, and those with one or more. As we shall see on the next section this approach for constructing a finite model fails when considering arbitrary number restrictions. 5 Finite Model Reasoning in DL-LiteN horn Kontchakow et. al., [9] show the following result by a reduction of the SAT problem to finite satisfiability in DL-LiteN horn . Lemma 5 ([9, Remark 98]). Finite satisfiability of DL-LiteN horn TBoxes is NP-hard. From the proof of the previous lemma, it can be seen that, contrary to the arbi- trary model case, when restricting to finite models in DL-LiteN horn , it is possible to express disjunctive knowledge, such as covering of a concept C by a disjunc- tion of concepts, even though the disjunction operator, ‘t’, is not part of the logic. Moreover, DL-LiteN horn looses convexity when restricting to finite models. In order to understand this more clearly, let us consider a TBox T with the following axioms: ≥ 3 P1 v ⊥, ∃P1 v≥ 2 P1 , ≥ 2 P1 ≡ ∃P2 , > v ∃P1− , (funct P1− ), − − B2 ≡ ∃P2 , (funct P2 ), (funct P2 ), B1 u B2 v ⊥. Let I be a finite model of T , and N = ](∆I ). We have that N = 2·](≥ 2 P1 )I . Furthermore, ](≥ 2 P1 ) = ](B2 )I = M , since P2I is a bijective function; and since B1 is disjoint with B2 , then ](B1 )I = M . Hence, ∆I = (B1 )I ∪ (B2 )I ; and as a consequence T |=fin ≥ 2 P1 v B1 t B2 . However, T 6|=≥ 2 P1 v B1 , and T 6|=≥ 2 P1 v B2 . The best known upper bound for finite satisfiability in DL-LiteN horn is Exp- Time, which is given by the complexity of finite model reasoning in ALCQI [11]. The approach taken by Lutz et. al., [11] is to transform a given ALCQI TBox into a system of linear inequalities which is exponential on the size of the TBox. We conjecture that this exponential blow up can be avoided when considering DL-LiteN horn TBoxes. The combinatorial nature of this problem suggests indeed the use of techniques of linear programming. However, we consider that a re- duction of this problem to the fragment of FOL with one variable and counting quantifiers is also feasible. For devising ad hoc algorithms for finite model rea- soning in DLs, it is still relevant to propose a constructive approach as in the case of DL-LiteFhorn . All these research problems, as well as constructions of finite models of KBs in logics in the EL family constitute ongoing research. References 1. Artale, A., Calvanese, D., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: Rea- soning over extended ER models. In: Proc. of the 26th Int. Conf. on Conceptual Modeling (ER 2007). Lecture Notes in Computer Science, vol. 4801, pp. 277–292. Springer (2007) 2. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and relations. J. of Artificial Intelligence Research 36, 1–69 (2009) 3. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope further. In: Clark, K., Patel-Schneider, P.F. (eds.) Proc. of the 5th Int. Workshop on OWL: Experiences and Directions (OWLED 2008) (2008) 4. Berardi, D., Calvanese, D., De Giacomo, G.: Reasoning on UML class diagrams. Artificial Intelligence 168(1–2), 70–118 (2005) 5. Borgida, A., Brachman, R.J.: The description logic handbook: theory, implemen- tation, and applications, chap. Conceptual Modeling with Description Logics, pp. 349–372. Cambridge University Press (2003) 6. Cosmadakis, S.S., Kanellakis, P.C., Vardi, M.Y.: Polynomial-time implication problems for unary inclusion dependencies. J. ACM 37(1), 15–46 (1990) 7. Goranko, V., Otto, M.: Handbook of Modal Logic, chap. Model Theory of Modal Logic, pp. 255–325. Elsevier (2006) 8. Kontchakov, R., Lutz, C., Toman, D., Wolter, F., Zakharyaschev, M.: The com- bined approach to query answering in DL-Lite. In: Lin, F., Sattler, U. (eds.) Proc. of the 12th Int. Conf. on the Principles of Knowledge Representation and Reason- ing (KR 2010). AAAI Press (2010) 9. Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology comparison and module extraction with an application to DL-Lite. AIJ 174(15), 1093–1141 (2010) 10. Lutz, C., Piro, R., Wolter, F.: Description logic TBoxes: Model-theoretic charac- terizations and rewritability. In: Proc. of the 22st Int. Joint Conf. on Artificial Intelligence (IJCAI 2012). AAAI Press (2011) 11. Lutz, C., Sattler, U., Tendera, L.: The complexity of finite model reasoning in description logics. Information and Computation 199, 132–171 (2005) 12. de Rijke, M.: A note on graded modal logic. Studia Logica 64(2), 271–283 (2000) 13. Rosati, R.: Finite model reasoning in DL-Lite. In: Proc. of the 5th Eur. Semantic Web Conf. (ESWC 2008). Lecture Notes in Computer Science, vol. 5021, pp. 215– 229 (2008)