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