=Paper=
{{Paper
|id=Vol-477/paper-7
|storemode=property
|title=Adding Weight to DL-Lite
|pdfUrl=https://ceur-ws.org/Vol-477/paper_51.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/ArtaleCKZ09
}}
==Adding Weight to DL-Lite==
https://ceur-ws.org/Vol-477/paper_51.pdf
Adding Weight to DL-Lite
A. Artale,1 D. Calvanese,1 R. Kontchakov,2 and M. Zakharyaschev2
1 2
KRDB Research Centre School of Comp. Science and Inf. Sys.
Free University of Bozen-Bolzano Birkbeck College
I-39100 Bolzano, Italy London WC1E 7HX, UK
lastname @inf.unibz.it {roman,michael}@dcs.bbk.ac.uk
1 Introduction
Description logics (DLs) have recently been used to provide access to large
amounts of data through a high-level conceptual interface, which is of relevance
in several application contexts, notably data integration and ontology-based data
access. Besides the traditional reasoning services of knowledge base satisfiability
and instance checking, a further important service in that context is that of an-
swering complex database-like queries by fully taking into account the axioms
in the TBox and the data stored in the ABox. The key property for such an
approach to be viable in practice is the efficiency of query evaluation, in partic-
ular for conjunctive queries and, more generally, for positive existential queries
(this class of queries includes unions of conjunctive queries) [1]. To address these
needs, the DL-Lite family of description logics has been proposed and investi-
gated in [6–8, 16], with the aim of identifying a class of DLs that could capture
typical conceptual modeling formalisms, such as UML class diagrams and ER
models, and for which query answering could be performed efficiently in terms of
data complexity. The data complexity measure presupposes that only the size of
the ABox is considered as variable while the sizes of the TBox and the query are
regarded as fixed. Such a measure is important since in the typical application
contexts we are interested in here, the size of the data stored in the ABox largely
dominates that of the TBox and the query. As shown in [6–8, 16], for the logics
of the DL-Lite family, a (union of) conjunctive queries posed over a TBox can
be answered by rewriting it into a new union of conjunctive queries that has
‘compiled in’ the assertions in the TBox, and that can simply be evaluated (by
a relational engine) over the ABox to produce the correct answer to the original
query. In other words, it was shown that such logics enjoy FO rewritability [7,
8], and so belong to the complexity class FO in terms of descriptive complexity
theory, and to the class AC0 in terms of circuit complexity [10].
Successive work [3] has shown that some of the nice computational properties
of DL-Lite logics can be preserved, even when they are extended with additional
constructs used in conceptual modeling. In particular, it was proved in [3] that
the data complexity of answering positive existential queries stays in AC0 for
the logic DL-LiteN horn which allows conjunctions on the left-hand side of concept
inclusions as well as arbitrary number restrictions. Moreover, the same data
complexity bound holds also for satisfiability and instance checking in the logic
Language Combined complexity Data complexity
Satisfiability Instance checking Query answering
0
(RN )
DL-Litecore NLogSpace in AC in AC0
0
(RN )
DL-Litehorn P ≤ [Th.1] in AC in AC0 ≤ [Th.3]
DL-Lite(RN
krom
)
NLogSpace ≤ [Th.1] in AC0 coNP ≥[18]
(RN )
DL-Litebool NP ≤ [Th.1] in AC0 ≤ [Th.2] coNP ≤[14, 13, 9]
Table 1. Combined and data complexity.
DL-LiteN
bool which allows full Booleans as concept constructs. (Note that these
results hold only under the unique name assumption. DL-Lite logics without
this assumption are investigated in [4].)
One aim of this paper is to extend DL-LiteN N
horn , DL-Litebool and their
fragments with a number of new constructs without spoiling their computa-
tional properties. The resulting logic is called DL-Lite(RN )
horn . Another aim is to
present explicit (exponential) FO rewritings of positive existential queries over
DL-Lite(RN )
horn KBs. The constructs we add to our logics are as follows: (i) role
inclusions, (ii) qualified number restrictions, and (iii) role disjointness, symme-
try, asymmetry, reflexivity, and irreflexivity constraints. Needless to say that
when adding (i) and (ii), we have to restrict the interaction of these constructs
with number restrictions (otherwise, even the logic DL-LiteR,F core with extremely
primitive concept inclusions, but with unrestricted role inclusions and global
functionality constraints is ExpTime-complete for combined complexity and P-
complete for data complexity [11].) This will be done by generalizing the ideas
of [16]. Our main tool for dealing with DL-Lite logics is embedding into the one-
variable fragment QL1 of first-order logic without equality and function symbols,
which seems to be a natural logic-based characterization of the DL-Lite logics.
The complexity results obtained in this paper are summarized in Table 1.
2 DL-Lite(RN )
bool and its fragments
We start by defining the description logic DL-Lite(RN )
bool , the most expressive of our
logics, which subsumes, in particular, all members of the DL-Lite family [6–8].
(RN )
The language of DL-Litebool contains object names a0 , a1 , . . . , concept names
A0 , A1 , . . . , and role names P0 , P1 , . . . . Complex concepts C and roles R are
defined as follows:
B ::= ⊥ | Ai | ≥ q R, R ::= Pi | Pi− ,
C ::= B | ¬C | ≥ q R.C | C1 u C2 ,
where q is a positive integer. The concepts of the form B will be called basic. A
DL-Lite(RN )
bool TBox, T , is a finite set of concept inclusions (CIs, for short), role
inclusions, and role constraints of the form:
C1 v C2 , R1 v R2 , Dis(R1 , R2 ), Irr(Pk ), and Ref(Pk ).
We write inv(R) for Pk− if R = Pk , and for Pk if R = Pk− . Denote by v∗T the
0 0 0
reflexive and transitive closure of {(R, R ), (inv(R), inv(R )) | R v R ∈ T }. Say
2
that R0 is a proper sub-role of R in T if R0 v∗T R and R 6v∗T R0 . We impose the
(RN )
following syntactic conditions on DL-Litebool TBoxes T (cf. DL-LiteA [16]):
(inter) if R has a proper sub-role in T then T contains no negative occurrences 1
of number restrictions ≥ q R or ≥ q inv(R) with q ≥ 2;
(exists) T may contain only positive occurrences of ≥ q R.C, and if ≥ q R.C
occurs in T then T does not contain negative occurrences of ≥ q 0 R or
≥ q 0 inv(R), for q 0 ≥ 2.
It follows that no TBox can contain both a functionality constraint ≥ 2 R v ⊥
and an occurrence of ≥ q R.C, for some q ≥ 1 and some role R.
An ABox, A, is a finite set of assertions of the form: Ak (ai ), Pk (ai , aj ) and
(RN )
¬Pk (ai , aj ). Taken together, T and A constitute the DL-Litebool knowledge base
(KB, for short) K = (T , A).
As usual in description logic, an interpretation, I = (∆I , ·I ), consists of
a nonempty domain ∆I and an interpretation function ·I that assigns to each
object name ai an element aIi ∈ ∆I , to each concept name Ai a subset AIi ⊆ ∆I ,
and to each role name Pi a binary relation PiI ⊆ ∆I × ∆I . In this paper, we
adopt the unique name assumption (UNA): aIi 6= aIj , for all i 6= j, and refer the
reader to [4] for results on the DL-Lite logics without UNA.
The role and concept constructs are interpreted in I in the standard way.
We will also use standard abbreviations such as > = ¬⊥, ∃R = (≥ 1 R) and
≤ q R = ¬(≥ q + 1 R). The satisfaction relation |= is also standard; we only
mention here that I |= Dis(R1 , R2 ) iff R1I ∩ R2I = ∅ (R1 and R2 are disjoint),
/ PkI for all x ∈ ∆I (Pk is irreflexive), I |= Ref(Pk ) iff
I |= Irr(Pk ) iff (x, x) ∈
(x, x) ∈ Pk for all x ∈ ∆I (Pk is reflexive). Note that symmetric and asymmetric
I
role constraints can be regarded as syntactic sugar in this language: Sym(Pk )
and Asym(Pk ) can be equivalently replaced with Pk− v Pk and Dis(Pk , Pk− ),
respectively (extending a TBox with Pk− v Pk cannot violate (inter) as Pk−
is not a proper sub-role of Pk ). 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.
It is to be emphasized that such constructs as role constraints and qual-
ified number restrictions are used in conceptual modeling and also belong to
the OWL 2 proposal; moreover, as we show, adding them does not affect the
computational complexity of our logics.
Similarly to classical logic, we adopt the following definitions: a TBox T is
– a DL-Lite(RN )
horn TBox if its CIs are of the form B1 u · · · u Bk v B (the Bi
and B are basic concepts and, by definition, the empty conjunction is >);
2
– a DL-Lite(RN )
krom TBox if its CIs are of the form B1 v B2 , B1 v ¬B2 or
¬B1 v B2 ;
1
An occurrence of a concept on the right-hand (resp., left-hand) side of a concept
inclusion is called negative if it is in the scope of an odd (resp., even) number of
negations ¬; otherwise the occurrence is called positive.
2
The Krom fragment of first-order logic consists of all formulas in prenex normal form
whose quantifier-free part is a conjunction of binary clauses.
3
– a DL-Lite(RN )
core TBox if its CIs are of the form B1 v B2 or B1 v ¬B2 .
As B1 v ¬B2 is equivalent to B1 u B2 v ⊥, core TBoxes can be regarded as
both Krom and Horn TBoxes. We note here that a concept C occurring in T in
some ≥ q R.C can be a conjunction of any concepts allowed on the right-hand
side of concept inclusions in the respective language.
3 DL-Lite in the Light of First-Order Logic
Our main aim in this section is to prove the upper combined complexity bounds
for reasoning in DL-Lite(RN )
bool and its fragments and develop the technical tools
we need to investigate the data complexity of query answering in DL-Lite(RN )
horn .
(RN ) ±
For a DL-Litebool KB K = (T , A), denote by role (K) the set of role names
occurring in K and their inverses and by ob(A) the set of object names occurring
in A. Let QRT be the set of natural numbers containing 1 and all the numerical
parameters q such that ≥ q R or ≥ q R.C occurs in T . Note that |QR T | ≥ 2 if T
contains a functionality constraint for R. Our main result in this section is:
Theorem 1. (i) Satisfiability of DL-Lite(RN )
bool KBs is NP-complete; (ii) satisfi-
ability of DL-Litehorn KBs is P-complete; and (iii) satisfiability of DL-Lite(RN
(RN )
krom
)
(RN )
and DL-Litecore KBs is NLogSpace-complete.
Let us consider first the sub-language of DL-Lite(RN )
bool without qualified num-
ber restrictions and role constraints, which will be required for purely technical
)− (RN )−
reasons; we denote it by DL-Lite(RNbool . In Section 4, we will also use DL-Litehorn .
)−
Let K = (T , A) be a DL-Lite(RN bool KB and let Id be a distinguished role
name, which will be used to simulate the identity relation required for encoding
the role constraints. We assume that either K does not contain Id at all or
satisfies the following conditions:
(Id1 ) Id(ai , aj ) ∈ A iff i = j, for all ai , aj ∈ ob(A),
Id−
(Id2 ) > v ∃Id, Id− v Id ⊆ T , and QId
T = QT = {1},
(Id3 ) Id is only allowed in role inclusions of the form Id− v Id and Id v R.
0
∗ 0
We assume, without loss of generality, that QR R
T ⊆ QT whenever R vT R (for
R0
if this is not the case we can always introduce the missing numbers in QT , e.g.,
by adding ⊥ v ≥ q R0 to the TBox).
(RN )−
We present now a reduction of the satisfiability problem for DL-Litebool
1
KBs to satisfiability of first-order formulas with one variable, or QL -formulas.
With every object name ai ∈ ob(A) we associate the individual constant ai
of QL1 and with every concept name Ai the unary predicate Ai (x) from the
signature of QL1 . For each role R ∈ role± (K), we introduce |QR T |-many fresh
unary predicates Eq R(x), for q ∈ QR T . The intended meaning of these predicates
is as follows: for a role name Pk , E1 Pk (x) and E1 Pk− (x) represent the domain
and range of Pk , respectively; more generally, for each q ∈ QR T , Eq Pk (x) and
Eq Pk− (x) represent the sets of points with at least q distinct Pk -successors and at
4
least q distinct Pk -predecessors, respectively. We write inv(Eq R)(x) for Eq Pk− (x)
if R = Pk , and for Eq Pk (x) if R = Pk− . Additionally, for every pair of roles
Pk , Pk− ∈ role± (K), we take two fresh individual constants dpk and dp− k of QL ,
1
which will serve as ‘representatives’ of the points from the domain and range of
Pk , respectively (provided that it is not empty). Denote the set of all those dpk
and dp− −
k by dr(K) and write inv(dr) for dpk if R = Pk , and for dpk if R = Pk .
−
1 ∗
By induction on the construction of concept C we define the QL -formula C :
⊥∗ = ⊥, (Ai )∗ = Ai (x), (≥ q R)∗ = Eq R(x),
(¬C)∗ = ¬C ∗ (x), (C1 u C2 )∗ = C1∗ (x) ∧ C2∗ (x).
For every role R ∈ role± (K), we need two QL1 -formulas:
εR (x) = E1 R(x) → inv(E1 R)(inv(dr)),
^
δR (x) = Eq0 R(x) → Eq R(x) .
q,q 0 ∈QR 0
T , q >q
q 0 >q 00 >q for no q 00 ∈QR
T
Formula εR (x) says that if the domain of R is not empty then its range is not
empty either: it contains the constant inv(dr), the ‘representative’ of the domain
of inv(R). The meaning of δR (x) should be obvious. For a KB K, we define
h ^ i
K‡e = ∀x T ∗R (x) ∧ εR (x) ∧ δR (x) ∧ A ‡e , where
R∈role± (K)
^ ^ ^
T ∗R (x) = C1∗ (x) → C2∗ (x) Eq R(x) → Eq R0 (x) ,
∧
C1 vC2 ∈T RvR0 ∈T or q∈QR
T
inv(R)vinv(R0 )∈T
^ ^ ^
A‡e = Ak (ai ) ∧ EqR,a
e R(a) ∧ (¬Pk (ai , aj ))⊥e ,
Ak (ai )∈A R(a,a0 )∈CleT (A) ¬Pk (ai ,aj )∈A
CleT (A) = {R0 (ai , aj ) | R(ai , aj ) ∈ A, R v∗T R0 },3 qR,a
e
is the maximum number
in QT such that there are qR,a many distinct ai with R(a, ai ) ∈ CleT (A), and
R e
(¬Pk (ai , aj ))⊥e = ⊥ if Pk (ai , aj ) ∈ CleT (A) and > otherwise. Note that the size
of K‡e is linear in the size of K, no matter whether the numerical parameters are
coded in unary or in binary. The following lemma is an analogue of [3, Theorem 1]
(for the proof see [4]):
−
Lemma 1. A DL-Lite(RN
bool
)
KB K is satisfiable iff the QL1 -sentence K‡e is
satisfiable.
It should be clear that the translation ·‡e can be computed in NLogSpace for
combined complexity. Indeed, this is trivial for the first conjunct of K‡e . To
compute A‡e , we first need to be able to check, given a role R and a pair of ob-
jects ai , aj , whether R(ai , aj ) ∈ CleT (A) and second, given R(a, a0 ) ∈ CleT (A), to
3
We slightly abuse notation and write R(ai , aj ) ∈ A to indicate that Pk (ai , aj ) ∈ A
if R = Pk , or Pk (aj , ai ) ∈ A if R = Pk− .
5
e
compute qR,a . The R(ai , aj ) ∈ CleT (A) test can be done by a non-deterministic
algorithm using space logarithmic in |role± (K)| (see, e.g., the NLogSpace di-
e
rected graph reachability problem [12]). The following algorithm computes qR,a :
set q = 0 and then enumerate all object names ai in A incrementing q each time
R(a, ai ) ∈ CleT (A); stop if q = max QR T or the end of the object name list is
e
reached. The resulting qR,a is the maximum number in QR T not exceeding q.
−
As follows from the proof of Lemma 1, for a DL-Lite(RN
bool
)
KB K = (T , A),
‡e
every model M of K induces a model IM of K with the following properties:
(abox) For all ai , aj ∈ ob(A), (aIi M , aIj M ) ∈ RIM iff R(ai , aj ) ∈ CleT (A).
(uniq) The object names a ∈ ob(A) induce a partitioning of ∆IM into disjoint
labeled trees Ta = (Ta , Ea , `a ) with nodes Ta , edges Ea , root aIM , and a
labeling function `a : Ea → role± (K) \ {Id, Id− }.
(cp) There is a function cp : ∆IM → ob(A) ∪ dr(K) such that cp(aIM ) = a for
a ∈ ob(A), and cp(w) = dr, for role R such that w0 ∈ Ta , (w0 , w) ∈ Ea and
`a (w0 , w) = inv(R), for some a ∈ ob(A).
(iso) For each R ∈ role± (K), all labeled subtrees generated by w ∈ ∆IM with
cp(w) = dr are isomorphic.
(con) For all basic concepts B in K and w ∈ ∆IM , w ∈ B IM iff M |= B ∗ [cp(w)].
(role) For every role name Pk , including Id,
PkIM = (aIi M , ajIM ) | R(ai , aj ) ∈ A, R v∗T Pk ∪ (w, w) | Id v∗T Pk ∪
(w, w0 ) ∈ Ea | a ∈ ob(A), `a (w, w0 ) = R, R v∗T Pk .
Such a model will be called an untangled model of K (the untangled model of K
induced by M, to be more precise). It should be pointed out that there are two
main distinguishing features of untangled models for DL-Lite(RN )
bool KBs: (i) there
are at most |ob(A)| + |role± (K)| different types of points in them, and (ii) al-
though two points may be connected by a set of roles Ω, one can always select
R ∈ Ω such that Ω is an upward closure of {R} under v∗T , provided that one of
the points is not from ob(A).
(RN )
The following lemma reduces satisfiability of DL-Litebool KBs to satisfiability
−
of DL-Lite(RN
bool
)
KBs (for the proof see [4, Lemma 5.17]):
0 0 0
Lemma 2. For every DL-Lite(RN )
bool KB K = (T , A ), one can construct (in
−
linear time and logarithmic space) a DL-Lite(RN
bool
)
KB K = (T , A) such that
– every untangled model IM of K is a model of K0 , provided that
there are no R1 (ai , aj ), R2 (ai , aj ) ∈ CleT (A) with Dis(R1 , R2 ) ∈ T 0 , and
there is no R(ai , ai ) ∈ CleT (A) with Irr(R) ∈ T 0 ;
– every model I 0 of K0 gives rise to a model I of K based on the same domain
as I 0 and such that I agrees with I 0 on all symbols from K0 .
Theorem 1 follows from Lemmas 2 and 1, the observation that K‡e is a QL1 -
1
formula, for a DL-Lite(RN ) (RN )
bool KB, a universal Horn QL -formula, for a DL-Litehorn
1 (RN )
KB, and a universal Krom QL -formula, for a DL-Litekrom KB, and the com-
plexity results for the respective fragments of QL1 [15, 5].
For the data complexity the following result is proved in [4, Section 6]:
6
Theorem 2. The satisfiability and instance checking problems for DL-Lite(RN
bool
)
0
KBs are in AC for data complexity.
4 FO Rewritability of Query Answering
In this section we study the data complexity of query answering over DL-Lite(RN horn
)
KBs. We assume that all concept and role names of a KB occur in its TBox and
write role± (T ) and dr(T ) instead of role± (K) and dr(K), respectively. Denote
by Bcon(T ) the set of basic concepts occurring in T (i.e., concepts of the form
A and ≥ q R, for a concept name A occurring in T , R ∈ role± (T ) and q ∈ QR T ).
A positive existential query q(x) is a first-order formula ϕ(x) constructed
by means of conjunction, disjunction and existential quantification from atoms
of the from A(t1 ) and P (t1 , t2 ), where t1 , t2 are terms taken from the list of
variables y0 , y1 , . . . and object names a0 , a1 , . . . . The free variables of ϕ are called
distinguished variables of q. An assignment a in ∆I is a function associating with
each variable y an element a(y) of ∆I . We write aI,a i = aIi and y I,a = a(y). For
K = (T , A), say that a tuple a of object names from A is a certain answer to
q(x) w.r.t. K, and write K |= q(a), if I |= q(a) whenever I |= K. The query
answering problem is, given K, a query q(x) and a ⊆ ob(A), decide whether
K |= q(a). Our main result in this section is the following:
Theorem 3. The positive existential query answering problem for DL-Lite(RN
horn
)
KBs is in AC0 for data complexity.
0 0 0
Proof. Suppose that we are given a consistent DL-Lite(RN )
horn KB K = (T , A ) and
a positive existential query in prenex form q(x) = ∃y ϕ(x, y), y = y1 , . . . , yk ,
)−
in the signature of K0 . Consider the DL-Lite(RN
horn KB K = (T , A) provided by
Lemma 2. The untangled models of K produce exactly the same answers as K0 :
Lemma 3. For every tuple a of object names in K0 , we have K0 |= q(a) iff
I |= q(a) for all untangled models I of K.
Next we show that, as K‡e is a universal Horn sentence, it is enough to
consider just one special untangled model I0 of K. Let M0 be the minimal
Herbrand model of K‡e . We remind the reader (see, e.g., [2, 17]) that M0 can be
constructed by taking the intersection of all Herbrand models for K‡e , that is,
of all models based on the domain Λ = ob(A) ∪ dr(T ). It follows that
M0 |= B ∗ [c] iff K‡e |= B ∗ (c), for all c ∈ Λ and B ∈ Bcon(T ).
Denote by I0 the untangled model of K induced by M0 and its domain by ∆I0 .
By Lemma 1 with (con) and (cp),
aiI0 ∈ B I0 iff K |= B(ai ), for all ai ∈ ob(A) and B ∈ Bcon(T ). (1)
±
For each R ∈ role (T ), by Lemma 1, if RI0 6= ∅ then M0 |= (∃R)∗ [dr] and thus,
(T ∪ {∃R v ⊥}, A) is not satisfiable, whence RI 6= ∅, for all models I of K.
Moreover, if RI0 6= ∅ then
w ∈ B I0 iff K |= ∃R v B, for all w ∈ ∆I0 with cp(w) = dr, (2)
7
where cp : ∆I0 → Λ is the function provided by (cp).
Lemma 4. If I0 |= q(a) then I |= q(a) for all untangled models I of K.
Proof. Suppose I |= K. As q(a) is a positive existential sentence, it is enough
to construct a homomorphism h : I0 → I. By (uniq), ∆I0 is partitioned into
trees Ta , for a ∈ ob(A). Define the depth of w ∈ ∆I0 to be the length of the
path in the respective tree from its root to w. Denote by Wm the set of points
of depth ≤ m; in particular, W0 = {aI0 | a ∈ ob(A)}. We construct h as the
union of homomorphisms hm : Wm → I, m ≥ 0, such that hm+1 (w) = hm (w),
for all w ∈ Wm . For the basis of induction, set h0 (aIi 0 ) = aIi , for ai ∈ ob(A);
h0 is a homomorphism by (1) and (abox). For the induction step, suppose hm
has been defined. If v ∈ Wm , set hm+1 (v) = hm (v). Otherwise, v ∈ Wm+1 \ Wm .
By (uniq), there is a unique u ∈ Wm with (u, v) ∈ Ea , for some a ∈ ob(A). Let
`a (u, v) = S. By (cp), cp(v) = inv(ds) and, by (role), u ∈ (∃S)I0 . As hm is a
homomorphism, hm (u) ∈ (∃S)I , whence there is w ∈ ∆I with (hm (u), w) ∈ S I .
Set hm+1 (v) = w. As (∃inv(S))I0 6= ∅, cp(v) = inv(ds) and w ∈ (∃inv(S))I ,
by (2), if v ∈ B I0 then w ∈ B I , for all B ∈ Bcon(T ). It remains to show that
(w, v) ∈ RI0 implies (hm+1 (w), hm+1 (v)) ∈ RI . By (role), we have (w, v) ∈ RI0 ,
for w ∈ Wm+1 and v ∈ Wm+1 \ Wm , just in two cases: either w ∈ Wm+1 \ Wm ,
and then w = v with Id v∗T R, or w ∈ Wm , and then w = u with S v∗T R. In the
former case, (hm+1 (v), hm+1 (v)) ∈ IdI ⊆ RI . In the latter case, (u, v) ∈ S I0 ;
hence (hm+1 (u), hm+1 (v)) ∈ S I ⊆ RI . t
u
Our next lemma shows that to check whether I0 |= q(a) it suffices to consider
only the set of points Wm0 of depth ≤ m0 in ∆I , for some m0 that does not
depend on |A| (see [4, Lemma 7.4] for the proof):
Lemma 5. Let m0 = k + |role± (T )|. If I0 |= ∃y ϕ(a, y) then there is an assign-
ment a0 in Wm0 (i.e., a0 (yi ) ∈ Wm0 for all i) such that I0 |=a0 ϕ(a, y).
To complete the proof of Theorem 3, we encode the problem ‘K |= q(a)?’
as a model checking problem for first-order formulas. We fix a signature that
contains a unary predicate Ak (x) for each concept name Ak and a binary pred-
icate Pk (x, y) for each role name Pk , and then represent the ABox A of K as a
first-order model AA with domain ob(A): for each ai , aj ∈ ob(A),
AA |= Ak [ai ] iff Ak (ai ) ∈ A and AA |= Pk [ai , aj ] iff Pk (ai , aj ) ∈ A.
Now we define a first-order formula ϕT ,q (x) in the above signature such that (i)
ϕT ,q (x) depends on T and q but not on A, and (ii) AA |= ϕT ,q (a) iff I0 |= q(a).
To simplify the presentation, we denote by e(T ) the extension of T with:
– ≥ q 0 R v ≥ q R, for all R ∈ role± (T ) and q, q 0 ∈ QR 0
T with q > q, and
– ≥ q R v ≥ q R0 , for all q ∈ QR
T and R v R 0
∈ T or inv(R) v inv(R0 ) ∈ T .
It follows from the definition of ·‡e and Lemma 1 that, for a Horn concept inclu-
sion C v B, we have T |= C v B iff (C ∗ (x) → B ∗ (x)) is a logical consequence
of {(Ci∗ (x) → Bi∗ (x)) | Ci v Bi ∈ e(T )}.
8
We begin by defining formulas ψB (x), B ∈ Bcon(T ), that describe the types
of the elements of ob(A) in the model I0 in the following sense (cf. (1)):
AA |= ψB [ai ] iff aiI0 ∈ B I0 , for B ∈ Bcon(T ) and ai ∈ ob(A). (3)
0 1
These formulas are defined as the ‘fixed-points’ of sequences ψB (x), ψB (x), . . .
of formulas with one free variable, where
A(x),
if B = A,
0
h ^ i
ψB (x) = ∃y1 . . . ∃yq
^
T
(yi 6= yj ) ∧ R (x, yi ) , if B = ≥ q R,
1≤i