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 description 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., satis ability 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 e ectively for conceptual modelling we need to ensure (1) that the chosen DL language is expressive enough to capture faithfully 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 nite, therefore, reasoning on conceptual models should be understood as reasoning w.r.t. nite models. The latter is not the usual assumption in DLs mainly because traditional description logics enjoy the nite model property (FMP), and hence there is no need to distinguish between reasoning w.r.t. arbitrary models, and w.r.t. nite ones. Notably, ALC (one of the traditional DLs) is not expressive enough for capturing cardinality constraints. In DLs cardinality constraints are expressed by (quali ed) number restrictions. ALCQI {which extends ALC with quali ed 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: nite satis ability 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 nite model reasoning exist. As an alternative, members of the DL-Lite-family of description logics including unquali ed ? We would like to thank the anonymous reviewers, as well as Alessandro Artale, Andre Hernich, and V ctor Gutierrez-Basulto for valuable remarks to improve the nal version of this paper.
Introduction
number restrictions [
The purpose of this paper is to bring attention to nite model reasoning
in description logics from a model theoretical view point. We adapt existing
techniques [
Preliminaries DL-Lite syntax and semantics The language of DL-LitehNorn contains individual 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 j Pi ;
B ::= ? j Ai j 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 9R. A DL-LitehNorn-TBox T is a nite set of axioms of the form B1 u u Bk v B; k 0, where by de nition the empty conjunction is >. We also consider the sublogic DL-LitehForn, 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 nite set of assertions of the form: A(ai) or P (ai; aj ). Together, a TBox T and an ABox A constitute a DL-LitehForn 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 fPk; Pk j Pk 2 role(K)g. For a role R 2 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 2 I ; to each concept name Aj a subset AjI I , and to each role name Pk, a binary relation PkI I I . The interpretation function is extended to concepts and roles as follows: (inverse role) (Top) (Bottom) (number rest.) (conjunction) (Pk )I = f(e; d) 2
I
I j (d; e) 2 PkI g; >I = ?I = ;;
I ; ( n R)I = fd 2
I j ]fe 2
I j (d; e) 2 RI g ng; (Bi u Bj )I = BiI \ BjI ; where ] denotes the cardinality of a set. An interpretation I satis es a TBox axiom dk Bk v B i (dk Bk)I BI , in that case we write I j= dk Bk v B; similarly, I j= (funct R) i whenever both (d; e) 2 RI and (d; e0) 2 RI , then e = e0. For ABox assertions we have that I j= A(ai) i aiI 2 AI ; and I j= Pk(ai; aj ) i (aiI ; ajI ) 2 P I . A knowledge base K = (T ; A) is satis able (or consistent) if k there is an interpretation I, satisfying every axiom in T and every assertion in A. In this case we write I j= K (as well as I j= T , and I j= A), and we say that I is a model of K (and of T and A). If I is nite (i.e., its domain is nite) we say that a K (as well as T and A) is nitely satis able. The type of d in I is the set tI (d) = fB j d 2 BI g, where B is a DL-LitehNorn-concept. The set of all types of I, is types(I) = ftI (d) j d 2 I g. We consider standard reasoning tasks. Speci cally, satis ability and subsumption. Let L 2 fDL-LitehForn, DL-LitehNorng. The satis ability problem consists on deciding, given an L-KB K, whether K is satis able; while the subsumption problem amounts to decide, given an L-TBox T and L-concepts C1 and C2, whether T j= C1 v C2, i.e., whether C1I C2I in every model I of T . 3
Model Theoretical Characterizations
Lutz et. al., [
For a DL-LitehNorn interpretation I, an object d 2 I , and a role R, R-succI (d) = fe 2
I j (d; e) 2 RI g is the set of R-successors of d in I.
Let I1 = ( I1 ; I1 ) and I2 = ( I2 ; I2 ) be two DL-LitehNorn interpretations. A graded equisimulation(or g-equisimulation) between I1 and I2 is a relation
I1 I2 that satis es the following properties: (atom) for every concept name A, if (d; e) 2 then d 2 AI1 i e 2 AI2 ; (role) for every role R, if (d; e) 2 , then the following hold: (i) for every nite set S R-succI1 (d), there exists a
R-succI2 (e), such that ]S = ]S0; and nite set S0 (ii) for every nite set S R-succI2 (e), there exists a
R-succI1 (d), such that ]S = ]S0.1 is called global if and only if (i) for every d 2 I1 there is some e 2 I2 with (d; e) 2 , (ii) for every e 2 I2 there is some d 2 I1 with (d; e) 2 .
We write (I1; d) (I2; e) if there exists a g-equisimulation between I1 and
I2 such that (d; e) 2 . 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-LitehNorn TBox, C a DL-LitehNorn concept; and I1
and I2 be two DL-LitehNorn interpretations over the signature of T and C. The
following statements hold:
(a) DL-LitehNornconcepts are invariant under g-equisimulations: (I1; d) (I2; e)
implies d 2 CI1 i e 2 CI2 .
(b) DL-LitehNorn TBoxes are invariant under global g-equisimulations: if I1 I2
then I1 j= T i I2 j= T .
(c) Every model of a DL-LitehNorn TBox is g-equisimilar to a tree-shaped model.
Canonical Models We use a standard characterization of unrestricted
entailment in terms of canonical models [
Ri+1 ).
De nition 1. Let K = (T ; A) be a DL-LitehNorn KB. The canonical interpretation IK = ( IK ; IK ) of K is de ned as follows:
IK = ind (A) [ fdR j R is generating in Kg;
aIK = a for every a 2 ind (A);
AIK = fa 2 ind (A) j K j= A(a)g [ fdR 2 IK j T j= 9R v Ag;
P IK = f(ai; aj ) 2 ind (A) ind (A) j P (ai; aj ) 2 Ag[
f(a; dP ) j a ; dP g [ f(dP ; a) j a ; dP g[
f(dS; dP ) j dS ; dP g [ f(dP ; dS) j dS ; dP g:
The canonical interpretation IK of a given KB K can be computed in polynomial
time on the size of K [
Example 1. Let K = (T ; A), where T = f9S v 9P1; 9P1 v 9P2; 9P2 v 9P1; 9P2 v 9P3 ; 9P3 v 9S (funct P1 ); (funct P2 ); (funct S); B v 9P1g, and A = fB(a)g.
The canonical interpretation IK, depicted in Figure 1, clearly violates the functionality of P1 and hence is not a model of K.
In general, IK cannot be a model of K since it is nite, and DL-LitehNorn does
not enjoy the nite model property (FMP). A standard way to construct a
(canonical) model from IK is to unravel it into a forest-shaped interpretation
UK [
Finite Model Reasoning in DL-LitehForn In this section, we study nite model reasoning in DL-LitehForn. Notably, the FMP it is already lost when considering only functionality constraints. Let us take the following DL-LitehForn KB to illustrate this:
K0 = (T [ fB u 9P2 v ?g; A) (1) with T and A from Example 1. It is not hard to see that K0 is satis able only by in nite models. Intuitively, in every model I of K0, there is an in nite 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 9P1 v 9P2, d1 has a P2 successor di erent from aI (from B u 9P2 v ?), say d2, from 9P2 v 9P1 , d2 has a P1-successor, d3, di erent from d1, (since P1 is functional), and d3 has a P2-successor, d4, di erent from d2 (since P2 is functional). These arguments can be used repeatedly to see that indeed an in nite number of objects are needed to satisfy the constraints in K0.
In order to provide a method for reasoning in DL-LitehForn w.r.t. nite models,
we follow the approach taken by Cosmadakis et. al., [
To simplify the presentation we consider an extension of DL-LitehForn with axioms of the form Bi Bj , with the following intended semantics for nite models: a nite interpretation I satis es Bi Bj if and only if ](Bj )I ](Bj )I . De nition 2. For a given DL-LitehForn TBox T , nClosure(T ) denotes the minimal set of axioms satisfying the following conditions: 1. T nClosure(T ); 2. For every pair of basic concepts B1; B2 occurring in T . If nClosure(T ) j=
B1 v B2, then B2 B1 2 nClosure(T ); 3. if (funct R) 2 nClosure(T ) then 9R 9R 2 nClosure(T ); 4. if fB1 B2; B2 B3g nClosure(T ) then B1 B3 2 nClosure(T ); 5. if f(funct R); 9R 9Rg nClosure(T ) then (funct R ) 2 nClosure(T ); 6. if nClosure(T ) j= B1 v B2, and B1 B2 2 nClosure(T ) then B2 v B1 2 nClosure(T ).
From 1, it follows that every model of nClosure(T ) is also a model of T . Since
TBox reasoning in DL-LitehForn is PTime-complete [
nite models. Hence, we have the following result: Lemma 3. Let T be a DL-LitehForn-TBox. Then, the following hold: (a) if nClosure(T ) j= dk Bk v B then T j= n dk Bk v B; (b) if (funct R) 2 nClosure(T ) then T j= n (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 ) 2 E i Bi Bj 2 nClosure(T ). The implications w.r.t. nite models can be better understood by observing the structure of (V; E ).
Example 2 ( nClosure). Consider the TBox T from Example 1. nClosure(T ) contains (among others) the axioms T1 = f9P2 v 9P1 ; 9P1 v 9P2 ; (funct P1); (funct P2)g. Figure 2 shows a portion of the graph induced by nClosure(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 ; dP2 ), corresponding to the axiom 9P2 v 9P1, it is inferred that 9P1 v 9P2 2 nClosure(T ). Analogously, from the solid line labelled with P1 , corresponding to (funct P1 ) it is inferred that (funct P1).
If there is an unsatis able concept Bi, this is re ected by an axiom of the form ? Bi. Let us consider K0 from (1). We have that from the `cycle rules', 9P1 v 9P2 2 nClosure(T 0). Hence, nClosure(T 0) j= f9P1 v 9P2 ; B v 9P1; B u 9P2 v ?g, which implies that nClosure(T 0) j= B v ?, and then, by rule 1, ? B 2 nClosure(T 0) (see Figure 3). This means that in every nite model I of T 0, ]BI = 0. An inconsistency w.r.t. nite models is then derived from the ABox assertion B(a).
B a
P1 P2 dP1 dP2
P1
P1 P3 dS
S dP3 dP1 dP2
P1
P2 P3 dS dP3
S P1
d' P3 dP3 SdS
P2 P3 dP3
SdS Fig. 5: UTb
P3
dP3 Lemma 4. Let T be a DL-LitehForn-TBox, and ' a DL-LitehForn axiom on the signature of T , i.e., ' is either a concept inclusion or a functionality constraint. If T j= n ' then nClosure(T ) j= '.
Proof. We shall show that nClosure(T ) 6j= ' implies T 6j= n '. In what follows, we x a DL-LitehForn-TBox T , and set Tb = nClosure(T ). Then, by Lemma 2(p2), it su ces to show that UTb 6j= ' implies T 6j= n ', where UTb is the unravelling of a canonical interpretation ITb that depends on '. Speci cally, if ' = C v B, then the `root' of UTb is an object d 2 CUTb n BUTb . On the other hand, if ' = (funct R), then UTb is rooted at an object d with two di erent R-successors e and e0.
Let us consider the case ' = C v B. We construct a nite model ITf of T such that UTb 6j= C v B implies ITf 6j= C v B. But rst, we introduce some useful notation. For any two concepts B1; B2, we write B1 vTb B2 whenever Tb j= B1 v B2; and B1 Tb B2, if additionally B2 vTb B1. Since Tb is an equivalence relation, the set of concepts E = f9R j R 2 role (Tb )g can be partitioned into equivalence classes w.r.t. Tb . Then, [9R] 2 E= Tb denotes the following equivalence class of concepts: [9R] = fBi 2 E j Bi Tb 9Rg. f Before moving forward with the de nition of IT , we observe that the canonical interpretation ITb constructed as in De nition 1 may introduce multiple witnesses for a given existential. We set ds = d0s whenever 9S Tb 9S0. Therefore, domain of the canonica(le.ign.t,erapsrientaFtiigounrIeTb4).
contains exactly one element dS for each class [9S] 2 E=
Tb We write [9Si]
R ! [9Sj ] i 9Si vTb 9R and 9R 2 [9Sj ]. Analogously, 9Si Tb 9Sj denotes that 9Si 9Sj 2 Tb .
We observe that induces a coarser partition on E. For a concept 9Si 2 E,
Tb the cluster of 9Si is the set C(9Si) = f9Sj 2 E j 9Si Tb 9Sj and 9Sj Tb 9Sig. In particular, for every two concepts 9Si; 9Sj 2 E, if 9Si Tb 9Sj then 9Si 2 C(Sj ); but the implication on the other direction does not hold. Intuitively, if 9Si; 9Sj belong to the same cluster, then their extensions have the same cardinality in every nite model of Tb , and of T .
Further, we use [9Si] [9Sj ] to denote the fact that there exist concepts 9R 2 [9Si] and 9R0 2 [9Sj ] such that 9R Tb 9R0, but 9R0 6 Tb 9R, i.e., 9R0 62 C(9R). For example, in the TBox T from Example 2, [9P1 ] [9S]. Notably, 9P1 Tb 9S, but 9S 62 C(9P1 ) = f9P1; 9P1 ; 9P2; 9P2 g. It is also the case that [9P1 ] 6 [9P2], since C(9P1 ) = C(9P2).
For constructing the domain of the desired nite model ITf , we de ne the set of nite paths of ITb . = (dS0 dSk ) 2 npaths(ITb ) i satis es the following conditions: 1. [9Si] R! [9S0], for some role R, such that : (a) (funct R ) 2 Tb , (b) [9Si+1] 2 C(9S0), and (c) 9R 62 [9Si+1] 2. [9Si+1] [9Si]
Intuitively, by condition (1a) a path ( dR) can be `reused' as a witness of an existential 9R, whenever the inverse of R is not functional, otherwise a new object ( 0 dR) is needed as a witness. Condition (1b) ensures that whenever such a witness path ( dS0 ) belongs to npaths(ITb ), then also witnesses ( dRi+1) for each class [9Ri+1] in the cluster C(9S0) belong to npaths(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 nite, then npaths(ITb ) is a also nite. by 'W=ecConvsidBe.r Masourbessepteocfi cnaplalyth,sfo(IrTb ) as the domain of ITf that it is determined = dS 0 2 npaths(ITb ), we write ' ; i there is a sequence of roles R0; : : : ; Rn such that: 1. C u :B v 9R0, 9S 2 [9Rn ]; 2. for i n, 9Ri 2 [9Si], [9Si] R!i [9Si+1], and 9Ri 62 [9Si+1]; 3. either (funct Ri ) 62 Tb or [9Si+1] 6 [9Si].
We are ready now to de ne ITf . fWe set ITf = f 2 npaths(ITb ) j ' ; g. For each concept name A, AITf IT , and for each atomic role P , P ( ITf ITf ), such that:
f AIT =f 2
f P IT =f(( k
ITf j tail ( ) vTb Ag; dSi ); (
dSi dSj )) j [9Si] P! [9Sj ]g [ f((dP [ f(( [ f((
dSi dSj ); ( [ f(d'; (dP )) j ' v 9P g
dSi )) j [9Sj ] P! [9Si]g ); d') j ' v 9P g dP ); ( 0; dP )) j 6= 0; (funct P ) 62 Tb g: 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 de ned by ( ; ) 2 i tail ( ) = dR, tail ( ) = dS and 9R 2 [9S].
Since UTb j= Tb , by Lemma 1(b), ITf j= Tb ; and since T Tb , ITf j= T . Moreover, ITf is as desired: ITf 6j= C v B, since by construction tITf (d') = tUTb (d'). Finally, the case for ' = (funct R), can be handled by a slight modi cation 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 nite model TBox reasoning in DL-LitehForn can be reduced to arbitrary TBox reasoning.
Theorem 1. For a given DL-LitehForn TBox T , concepts C1 and C2. We have that the following hold: 1. T is nitely satis able i nClosure(T ) is satis able. 2. T j= n C1 v C2 i nClosure(T ) j= C1 v C2.
Next, we show that the complexity of nite model reasoning in DL-LitehForn remains in PTime, when considering also an ABox, i.e., the following hold: Theorem 2. Let K = (T ; A) be a DL-LitehForn KB. Then K is nitely satis able i ( nClosure(T ); A) is satis able.
Thus, the complexity of reasoning in DL-LitehForn coincides for nite and arbitrary models.
Theorem 3. Finite model reasoning in DL-LitehForn is PTime-complete. As pointed out in Section 3 the canonical interpretation of a knowledge base K constructed as in De nition 1 it is not in general a model of K, due to the presence of functionality constraints (and arbitrary number restrictions in genf eral). The latter observation provides an intuition for the construction of IT . Intuitively, ITb can be transformed into a nite model by creating `copies' of certain portions (clusters) in order to resolve violations to functionality constraints; then, although the number of R-successors of some objects in the model increases (speci cally for those roles R in the TBox such that (funct R) 62 Tb ), this does not trigger any inconsistency, because the expressive power of DL-LitehForn allows 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 nite model fails when considering arbitrary number restrictions. 5
Finite Model Reasoning in DL-LitehNorn
Kontchakow et. al., [
Lemma 5 ([9, Remark 98]). Finite satis ability of DL-LitehNorn TBoxes is NP-hard.
From the proof of the previous lemma, it can be seen that, contrary to the arbitrary model case, when restricting to nite models in DL-LitehNorn, it is possible to express disjunctive knowledge, such as covering of a concept C by a disjunction of concepts, even though the disjunction operator, `t', is not part of the logic. Moreover, DL-LitehNorn looses convexity when restricting to nite models. In order to understand this more clearly, let us consider a TBox T with the following axioms:
3 P1 v ?; 9P1 v 2 P1; 2 P1 9P2; > v 9P1 ; (funct P1 ); B2 9P2 ; (funct P2); (funct P2 ); B1 u B2 v ?:
Let I be a nite 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 j= n 2 P1 v B1 t B2. However, T 6j= 2 P1 v B1, and T 6j= 2 P1 v B2.
The best known upper bound for nite satis ability in DL-LitehNorn is
ExpTime, which is given by the complexity of nite model reasoning in ALCQI [