=Paper=
{{Paper
|id=None
|storemode=property
|title=Finite Model Reasoning in DL-Lite with Cardinality Constraints
|pdfUrl=https://ceur-ws.org/Vol-846/paper_53.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/Ibanez-Garcia12
}}
==Finite Model Reasoning in DL-Lite with Cardinality Constraints==
https://ceur-ws.org/Vol-846/paper_53.pdf
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)