The ability to import ontologies safely, that is, expertise/authority and cooperates with other teams without changing the original meaning of their terms, has to relate the part it is working on with other parts. been identi¯ed as crucial for the collaborative development Performing an upgrade of even only one such a comand the reuse of (OWL) ontologies. ponent ontology may require the participation of all In this paper, we propose the notion of local safety of an on- the teams as di®erent component ontologies are, when tology and we identify scenarios in which this notion may combined together, interrelated, depend on and a®ect tboe iumsepfourltinothgueridoinngtotlhoegiedsevsealfoeplym.ent of an ontology that is one another (changing one component ontology may thus necessitate changes to the others and might require teams to reconcile their changes). 1 Introduction By reusing an ontology we mean using it as an input to develop a new ontology. In such a process, signi¯cant parts of the reused ontology are often extracted, re¯ned, extended or otherwise adapted and then combined with other ontologies to form the ¯nal assembly. One of the prerequisites for e±cient collaborative ontology construction and maintenance is the ability to combine ontologies in a controlled way. The interaction among component ontologies should be controlled and well-understood in order to reduce the communication that is needed among di®erent teams and to avoid expensive reconciliation processes. Ideally, controlled interaction should allow di®erent teams to develop, test and upgrade their ontologies independently, to replace a component ontology or extend an ontology with minimal side e®ects. The issue is also vital for ontology reuse, especially in the case when the reused ontology, rather than being adapted and used as a draft to develop an ontology component, is linked to and remains under the control of its original developers, who may perform changes to it autonomously.
? The work was supported by the project No. 1M0554 \Advanced Remedial Processes and Technologies" of the Ministry of Education, Youth and Sports of the Czech Republic and partly by the Institutional Research Plan AV0Z10300504 \Computer Science for the Information Society: Models, Algorithms, Applications". The ¯rst author also acknowledges the ¯nancial support of the Department of Mathematics at his institution.
cise contained in some other OWL ontology. In the import- built using concept and role constructors. We assume ing ontology, there is no logical di®erence between the the sets C, R and I of (respectively) atomic concepts, statements that are imported and the proper ones. atomic roles and individuals to be countably in¯nite
A number of recent papers by Grau et al. [3{7] and mutually disjoint and to be ¯xed for every DL. stressed the particular relevance of the ability to im- An ontology O formalized in a DL takes the form of port OWL ontologies \safely", that is, in such a way a ¯nite set of terminological and role axioms, which that the imported terms (the terms of the imported are used to suitably organize and interrelate multiple ontologies) preserve their original meaning (the mean- concept and role descriptions. DLs are distinguished ing these terms have in the imported ontologies) in the by constructors and/or types of axioms they provide. importing ontology. This ability is applicable in typi- We will use the term L-axiom (L-ontology) to emphacal scenarios of OWL ontology development such as in size we are talking about an axiom (an ontology) in the following one (see the above-mentioned works by the DL L.
Grau et al. for a motivating example): In the abstract notation we will use the letters A, B to denote atomic concepts, r, s to denote atomic roles, and a, b for individuals (all the letters possibly with a subscript). The letters C, D will be used to denote a concept (atomic or complex), R, S to denote a role, and ®, ¯ to denote an axiom.
As the minimal DLs of practical interest are usually considered the DLs E L and AL, which both are fragments of the smallest propositionally closed DL ALC. In ALC, concepts are composed inductively according to the following syntax rule: { an ontology engineer distinguishes between the socalled external terms and the so-called local terms of the ontology O he or she is developing; { the local terms are those whose meaning is assumed to be fully described in the ontology O itself, possibly with the help of the remaining, external terms; { the meaning of the external terms is assumed to be only partially described in the ontology O { in terms of their use in the description of the local terms { and to be further described in some other ontologies (preexistent or concurrently developed) that are to be imported into O; { the use of the external terms in the statements of the ontology O is expected not to alter the original meaning these terms have in the ontologies to be imported.
? (bottom concept) j > (top concept) j
In the paper, we continue in the study, initiated by Grau at al., of the methodology for OWL ontology development in the scenario given above. We propose the notion of local safety of an ontology and discuss under which conditions and how this notion can be used to guide the development of OWL ontologies. 3
In this section we introduce description logics (DLs) [
DLs view the world as being populated by ob- GCIs C v D and D v C. E L, AL and ALC provide jects and allow one to represent the relevant notions of no role axioms. the domain of interest in terms of concepts, roles and S is an extension of ALC in which an atomic role (possibly) individuals, representing sets of elements, can be declared transitive using the role axiom of the binary relationships between elements and single el- form Trans(r). ements, respectively. Starting from atomic concepts, Further extensions of DLs are indicated by apatomic roles and individuals, which are denoted sim- pending letters to the DL's name. Advanced concept ply by a name, complex concepts and complex roles are constructors include number restrictions of the form :C (concept negation) j
In AL, the syntax of complex concepts is the following: ?, >, :A (atomic concept negation), C uD, 9R:> (limited existential restriction), and 8R:C.
DLs E L, AL and ALC provide no role constructors.
The listed ALC constructors are not all independent (> = :?, C t D = :(:C u :D), 8R:C = :(9R::C)). In fact, ALC can be obtained from both E L and AL by adding the concept negation constructor. ¸ nR (indicated by appending the letter N ), quali- O j= C v D, and satis¯ability of concept C in the ¯ed number restrictions ¸ nR:C (appending Q) and case O 6j= C v ?. bnoermriensatlrsictfiaogns(aanpdpeqnudailni¯gedOn).u mInbetrheresctarsicetioofnsn,utmhe- Interpretations I and J are isomorphic (written dual constructors · nR and · nR:C are introduced I »= J ) i® there is a bijection ¹ : ¢I ! ¢J such rraeesspaprbeebscetrnievtveiinlaygt.ioNanossmifnoigrnla:elt(so¸nalnlsoe+wts1cRtoon)tacaoninndsin:trg(u¸cotnnea+icn1odRnic:vCeipd)t-, if(tnoh¹lta(leoxtrw)pf;iro¹nerg(tyaeh)tv)ioeolr2ndyssr:xaJx;r,ey2xs2eA=mI¢aanIiI®t;iAic¹®a(lx2l¹y)(xC2in);dAr=isJ2ta,inJ(Rgx.u;;Iiyasso)hm2a2bolIrrepIth(hiii®nce ual. Enumeration fa1; : : : ; ang is an abbreviation for particular, they satisfy the same axioms). fa1g t : : : t fang.
Yet other extensions include role constructors, of A signature S is a ¯nite subset of C[R[I. Two inwhich the inverse role constructor r¡ (appending I) terpretations I and J coincide on a signature S (writis the most prominent one. Another important type of ten IjS = J jS) i® ¢I = ¢J and XI = XJ holds for role axioms is the role inclusion R v S (appending H). all X 2 S.
These extensions can be used in di®erent combina- We say that I has been obtained from J through tions, for example ALN is an extension of AL with a domain expansion with the set ¢ (such I will by number restrictions, and SHOIN is the DL that uses denoted by J[¢) i® ¢ is a non-empty set disjoint 5 of the constructors we have presented. with ¢J , ¢I = ¢J [ ¢, and XI = XJ holds for all
The semantics of DLs is de¯ned via interpretations. X 2 C [ R [ I. Note that J[¢ and J only di®er in An interpretation I is a pair I = (¢I ; :I ), where ¢I that the domain of J is a proper subset of the domain is a non-empty set, called the domain of the inter- of J[¢ (with ¢ being the set of additional domain pretation, and :I is the interpretation function, which elements). maps atomic concepts to subsets of ¢I , atomic roles to binary relations over ¢I and individuals to elements A DL L is said to have the ¯nite model property of ¢I . The interpretation function extends to complex (FMP) i® every consistent L-ontology admits a model concepts as follows: that is ¯nite (i.e., with a ¯nite domain). One of the most prominent DLs that exhibit the FMP is SHOQ, ?I = ;; >I = ¢I ; while SHIN is an example of a DL that lacks the (C u D)I = CI \ DI ; (C t D)I = CI [ DI ; FMP. For a DL L with the FMP, L-ontology O and
L-axiom ® the following holds: O j= ® i® I j= ® for (:C)I = ¢I ¡ CI ; all ¯nite models I j= O. (8R:C)I = fx 2 ¢I ; 8y ((x; y) 2 RI ! y 2 CI )g; We say that an interpretation K is a disjoint union (9R:C)I = fx 2 ¢I ; 9y ((x; y) 2 RI ^ y 2 CI )g; of interpretations I and J (written K = I ] J ) i® (¸ nR)I = fx 2 ¢I ; jfy 2 ¢I ; (x; y) 2 RI gj ¸ ng; there exist some interpretations I~ and J~ satisfying (¸ nR:C)I = fx 2 ¢I ; I~ »= I, J~ =» J and ¢I~ \ ¢J~ = ; for which the foljfy 2 ¢I ; (x; y) 2 RI ^ y 2 CI gj ¸ ng; lowing holds: ¢K = ¢I [ ¢J~, XK = XI [ XJ~ for all ~ ~ a I = faI g; X 2 C [ R and aK = aI~ for all a 2 I. Intuitively, the (rf¡g)I = f(x; y); (y; x) 2 rI g: ipnotseerdpreotfattwioon uKnrfeolratwedhicpharKts =onIe]bJeinhgolidsosmisorcpohmicto I and the other to J . Disjoint union of a set of interpretations is de¯ned analogously.
The semantics of terminological axioms is de¯ned in terms of a satisfaction relation j=, which relates interpretations to the terminological axioms they satisfy. A DL L is said to have the disjoint union model It is de¯ned as follows: I j= C v D i® CI µ DI , property (DUMP) i® the set of models of arbitrary I j= R v S i® RI µ SI , I j= C(a) i® aI 2 CI , L-ontology is closed under disjoint unions. rIelja=tioRn(ar;Ib)is i®tra(nasIi;tibvIe). I2ntRerIp,reItajt=ionTsrasnast(irsf)yiin®gtahne A prominent example of a DL that enjoys the axiom are said to be its models. DUMP is SHIQ. DLs that support nominals do not
An interpretation I is a model of an ontology O have this property. (written I j= O) i® I j= ® for all ® 2 O. An ontology In the subsequent sections, will use C(®) to denote is said to be consistent if it has at least one model and the set of all atomic concepts that occur in the axiom ® is said to be inconsistent otherwise. (the sets R(®) and I(®) are de¯ned analogously). We
An ontology O entails an axiom ® (written O j= ®) will use Sig(®) as a shorthand for C(®) [ R(®) [ I(®).
i® all models of O satisfy ®, especially we will speak C(O) will stand for S®2O C(®) (the sets R(O), I(O)
about subsumption between C and D in the case of and Sig(O) are de¯ned analogously).
4 Related work As Grau et al. showed, even the problem of
checking whether an ontology consisting of a single ALC
axIn the papers by Grau et al. [3{7], safety of ontology iom is safe for a signature w.r.t. ALCO is undecidable.
import is formulated using the notion of conservative It is not yet known whether the safety for a signature
extension, in the context of ontologies ¯rst used in [
We say that O2 is a deductive conservative ex- polynomial time.
tension of O1 w.r.t. L, if for every L-axiom ® with Several extensions to OWL have been proposed
Sig(®) µ Sig(O1), we have O2 j= ® i® O1 j= ®. to better support collaborative ontology
developAn ontology O into which an ontology O0 can be safely ment and ontology reuse, including P-OWL [
We say that O is safe for O0 w.r.t. L, if O [ O0 is current candidate recommendation for OWL 2 [
Ghilardi at al. [
As regards the scenario we are concerned with, Grau et al. [3{7] argues that in practice it is often convenient, or even necessary, for the developers of an ontology O to abstract from particular ontologies that are to be imported into it and focus instead only on O and on its external terms: Grau et al. proposed the following condition to be used to guide the development of an ontology O in such cases.
The notion of safety for a signature, along with the corresponding safety classes, facilitates the construction of an ontology that is safe for any ontology (in a given DL) with which it shares only some prearranged set of terms.
In the scenario we are interested in here, however, { ontologies to be imported might not be available an ontology engineer does not always need to have during the development of O (as it is in the case the ontology O safe for every possible ontology (every when these ontologies are developed concurrently possible set of axioms in a certain DL), but often only with O); needs to have it safe for a certain, conveniently cho{ the developers of O are usually not willing to com- sen class of candidate ontologies. This is the case, for mit to particular versions of the ontologies they instance, when the scenario applies to collaborative intend to import (the development of a typical on- ontology development and O is considered as a compotology is a never-¯nished process); nent ontology for a larger ontology developed distribu{ at a later time, the developers might ¯nd ontolo- tively as a set of ontologies importing one another. The gies other than those initially considered more development of component ontologies in such a case is suitable for providing the meaning of the external typically coordinated to some extent (e.g., some printerms of O. ciples on which individual component ontologies will be build are resolved beforehand and made explicit) and the developers can make assumptions about some qualities and characteristics of the ontologies they import (as well as about the way these ontologies may further evolve).
De¯nition 3 (Safety for a signature). Let L be a DL, O an ontology and S a signature.
We say that O is safe for S w.r.t. L, if for every L-ontology O0 such that Sig(O) \ Sig(O0) µ S, O is safe for O0 w.r.t. L.
5.1
Local ontologies
Ontologies, like other engineering artifacts, are
designed. When we choose how to represent something
in an ontology4, we are making design decisions. The
4 \There is no one correct way to model a domain { there
are always viable alternatives." [
Generally accepted and widely cited are the ¯ve de- the case of domain, task and application ontologies sign criteria Gruber [19] proposed for ontologies whose at least, such an ontology can be considered badlypurpose is knowledge sharing and interoperation designed: among programs. They include the following criterion: Proposition 1. A SHOIQ ontology restricts the meaning of the top concept i® it is not local.
Grau et al. [25] also reported testing over 700 ontologies available on the Web for localness and ¯nding more than 99% of them local. However, we could not trace any further details on their experimental results. 5.2
Local safety Regarding the development of an ontology in our scenario, the considerations above suggest that it is often possible to consider only local ontologies as the candidates for importing.
6 http://www.jfsowa.com/ontology/toplevel.htm 7 Relevant points of the characterization are reproduced
at the beginning of the Appendix.
An ontology should o®er a conceptual foundation for a range of anticipated tasks, and the representation should be crafted so that one can extend and specialize the ontology monotonically. Especially, one should be able to de¯ne new terms for special uses based on the existing vocabulary, in a way that does not require the revision of the existing de¯nitions.
An ontology should be extensible. [. . . ] Extension should be possible both at a low level, by adding domain-speci¯c subconcepts, or at high level by adding intermediate or upper level concepts that cover new areas.
As regards top-level ontologies, we studied the Basic Formal Ontology5 and also the design of several other To facilitate the design, deployment and reuse of on- top-level ontologies [22], and came to the conclusion tologies, Guarino [20] suggested the development of that even in this case the developers prefer not to redi®erent kinds of ontologies with di®erent levels of gen- strict the meaning of the top concept. The only exceperality and dependence on a particular domain, task tion we found is the top-level ontology6 proposed by or point of view, namely top-level ontologies, domain John Sowa. and task ontologies and application ontologies. Terms The notion of restricting the meaning of the top of ontologies on a lower level are, in some sense, held concept is closely related to the notion of localness of to be specializations of terms of ontologies on a level an ontology studied (also under the name safety of an above. Top-level ontologies, which describe concepts ontology) by Grau et al. [23{26]. independent of a particular problem or domain (such De¯nition 5 (Localness). An ontology O is local if as space, time, object, event, action, etc.) are meant the set of its models is closed under domain expansion to be unifying for a large group of ontologies on lower (i.e., if I j= O implies I[¢ j= O for every interpretalevels. tion I and every non-empty set ¢ disjoint with ¢I ).
Swartout et al. [21] proposed a number of desiderata aimed primarily at domain, task and application In [23], a syntactic characterization of localness for ontologies. They include the two following: SHOIQ ontologies is given, which allows one to check localness of an SHOIQ ontology in polynomial time.
We used this characterization7 to show that SHOIQ ontologies restricting the meaning of the top concept are exactly those that are not local.
Ontologies should not be \stovepipes." The derisive term \stovepipe system" is used to describe a system that may be vertically integrated but cannot be integrated horizontally with other systems.
Here we propose a notion of restricting the meaning of the top concept, which, as we believe, provide a partial characterization of ontologies violating the aforementioned criteria.
De¯nition 4 (Restricting the meaning of the top concept). We say that the ontology O restricts the meaning of the top concept, if there are atomic concepts A1; : : : ; An, atomic roles r1; : : : ; rm; s1; : : : ; sk and individuals a1; : : : ; al in Sig(O) such that:
O j= > v A1 t : : : t An t 9r1:> t : : : t 9rm:> t t 9s1¡:> t : : : t 9sk¡:> t fa1; : : : ; alg: { it can not be, without previous modi¯cation, extended to cover a broader subject area than it already does, { it is unsuitable for importing into any ontology that touches, even marginally, a subject area disjoint with that already covered by it. De¯nition 6 (Local safety for a signature). Let Proposition 5. Let S be a signature such that S µ C, L be a DL, S a signature and O an ontology. O a SHIQ ontology and a an individual. Assume that
We say that O is locally safe for S w.r.t. L, if for there exists a subset S~ µ S such that the ontology every local L-ontology O0 with Sig(O) \ Sig(O0) µ S, O is safe for O0 w.r.t. L. O [ fA ´ faggA2S~ [ fA ´ ?gA2S¡S~ The following proposition provides su±cient condition for local safety w.r.t. SHOIQ.
Proposition 2. Let S be a signature and O an ontology such that for every interpretation J there exists a model I of O such that { ¢I = ¢J [ ¢ for some ¢, ¢ \ ¢J = ;, { XI = XJ for all X 2 S.
Then O is locally safe for S w.r.t. SHOIQ.
The following example demonstrates that, in comparison with safety condition proposed by Grau et al., the condition of local safety is less restrictive and may allow for a more convenient use of the external terms.
Example 1. Let us consider building an OWL ontology intended to provide a reference terminology for the annotation of ¯lms. Let us assume we intend to safely import into our ontology O some well-designed (and thus local) ontology that de¯nes the categorization of ¯lms by genre. Suppose that the atomic concept Film is expected to be the only term our ontology will share with the imported ontology. Whereas the ontology is inconsistent.
Then O is not locally safe for S w.r.t. ALO (E LO).
Corollary 1. Let S be a signature such that S µ C, O a SHIQ ontology.
Then O is locally safe for S w.r.t. SHOQ i® O is locally safe for S w.r.t. ALO (E LO).
Corollary 2. Let L be a DL that is in between ALO (E LO) and SHOQ.
The problem of deciding whether a SHIQ ontology is locally safe for a signature S, S µ C, w.r.t. L is reducible to the problem of checking consistency of a ¯nite set of SHOIQ ontologies, and thus decidable.
Corollary 3. Let O be a SHIQ ontology locally safe for S µ C w.r.t. SHOQ, O0 a local SHOQ ontology such that Sig(O)\Sig(O0) µ S. Then O [O0 is locally safe for S n Sig(O0) w.r.t. SHOQ. 6
{ ¢I = ¢J [ ¢ for some ¢, ¢ \ ¢J = ;, { XI = XJ for all X 2 S.
O = fDirector v :Film; Film v 9hasDirector:Directorg This paper contributes to the framework for ontology development presented by Grau et al. We proposed is not safe for fFilmg even w.r.t. AL (take the non- the notion of local safety of an ontology and showed local ontology O0 = f> v Filmg as a counterexample), its applicability in the development of real-world onit is, according to Proposition 2, locally safe for fFilmg tologies. We showed that local safety for a signature w.r.t. SHOIQ. consisting solely of atomic concepts is decidable for an When we are concerned with local safety w.r.t. SHOQ interesting group of description logics. (which has the FMP) we can use the following su±- For the future work, we would like to study decient condition. cidability and computational properties of (su±cient Proposition 3. Let S be a signature and O an on- conditions for) local safety for a signature that contology such that for every ¯nite interpretation J there tains atomic roles as well. The results obtained in the exists a model I of O such that paper are also directly applicable to the problem of extracting reusable ontology parts, or ontology modules, as conceived by Grau et al. in the cited works.
Then O is locally safe for S w.r.t. SHOQ.
The two following propositions give a recipe for deciding local safety of an ontology written in SHIQ (which has the DUMP) w.r.t. SHOQ in the case when all external terms are atomic concepts.
Proposition 4. Let S be a signature such that S µ C, O a SHIQ ontology and a an individual. Assume that for every subset S~ µ S the ontology
O [ fA ´ faggA2S~ [ fA ´ ?gA2S¡S~ is consistent.
Then O is locally safe for S w.r.t. SHOQ. we have CI[¢ = CI and DI[¢ = DI [ ¢. By (?) and by the fact that ¢ \ CI = ; (because ¢ \ ¢I = ;), we get CI[¢ 6µ DI[¢ . For C non-local, D local, we have CI[¢ = CI [ ¢ and DI[¢ = DI . By (?), we get CI[¢ 6µ DI[¢ . For C, D are non-local, we have CI[¢ = CI [ ¢ and DI[¢ = DI [ ¢. By (?) and by the fact that ¢ \ CI = ;, ¢ \ DI = ; (because ¢ \ ¢I = ;), we get CI[¢ 6µ DI[¢ . For each of the and Sig(®) µ Sig(O0), K 6j= ®. four possible cases we showed that I[¢ 6j= C v D.
The remaining types of SHOIQ axioms (C ´ D, not a model of ®, which yields a contradiction with
the assumption (¤).
Proof (of Proposition 1.). The proposition is obviously true for inconsistent ontologies.
meaning of the top concept. Then, by De¯nition 4, O j= > v C for some C of the form A1 t : : : t An t 9r1:>t: : :t9rm:>t 9s1¡:>t: : :t9 k s¡:>tfa1; : : : ; alg.
Take any model I of O and any x 2= ¢I . As >I[fxg = ¢I [ fxg and CI[fxg = ¢I , I[fxg 6j= > v C, and thus
Proof (of Proposition 3.). Same proof as of Proposition 2 goes through - we only need to replace the sentence labeled with (¦) with the following: Because (?) and because SHOQ has the FMP, there exists a ¯nite
Proof (of Proposition 4.). Let J be a ¯nite interpre
an unique ax 2 I, ax 2= Sig(O) (i.e., di®erent elements are associated with di®erent individuals). For every where
A1; : : : ; An, r1; : : : ; rm and a1; : : : ; al are model I all atomic concepts, atomic roles and individuals a model I of O such that I 6j= > v C. Pick any such in Sig(O). Since O 6j =
> v C, there exists . Since I 6j
= > v C, there exists an object ¢I such that x do not participate in the interpretation XI of any atomic concept, atomic role and individual X in Sig(O). Observe that: for all local SHOIQ concepts C1 composed of the symbols from Sig(O), x 2= C1I holds; for all non-local SHOIQ concepts C2 composed of the symbols from Sig(O), x 2 C2I holds. Therefore, O does not contain a GCI of O
0 w.r.t. SHOIQ.
Assume (for
contradiction) that there exists a SHOIQ axiom ® with Sig(®) µ Sig(O0) for which both O 6j 0 = ® (?) and O [ O j 0 = ® ( ) hold.
¤ By (?), there is a model J of O0 such that J 6j= ®. (¦)
The conditions of the proposition imply the existence of a model I of O such that ¢I = ¢J [ ¢, ¢ \ pretation K satisfying: ¢K = ¢I , XK = XI for all X 2 Sig(O), XK = XJ for all X 2 Sig(O0). Such an interpretation exists as XI = XJ for X 2 Sig(O)\Sig(O0), and thus is local. of the form C2 v C1 (otherwise I were not its model) following holds: AIx = faxIx g if x 2 AJ ; AIx = ; if Proof (of Proposition 2.). Let O0 be an arbitrary local and thus AI = AJ (¦). and, consequently, AI = S x 2= AJ . Thus, for A 2 S we have AI~ = S x2AJ faxI g = S x2AJ faxI~g x2AJ fxg, (?), we get CI[¢ 6µ DI[¢ . For C local, D non-local, and symbols not occurring in Sig(O) \ Sig(O0) can be ¢J = ; and XI = XJ for all X 2 S. Pick any inter- inconsistent (O [ O
O [ fA ´ faxggA2Sx [ fA ´ ?gA2S¡Sx : Pick some interpretation I~ such that I~ = U axI = x for all x 2 ¢J (to get such interpretation I it is enough to \rename" ¯nitely many elements in ¢I~). tology, SHIQ has the DUMP, ¢J is ¯nite, we have
, I j= O (?).
As axI = x for all x 2 ¢J , we have ¢J µ ¢I (¤).
interpreted arbitrarily.
Since J[¢jSig(O0), K j= O0. Therefore K j= O [ O0. we have J[¢ j= O0 and consequently, since KjSig(O0) =
= ®, we have, using Lemma 1, that J[¢ 6j= ®. Furthermore, since KjSig(O0) = J[¢jSig(O0) inition 4, O 6j= > v C for C of the form A1 t : : : t An t restrict the meaning of the top concept. Then, by Def- x 2 ¢J , let us set Sx = fA 2 S; x 2 AJ g. The conditions of the proposition imply that for 9r1:>t: : :t9rm:>t 9r1¡:>t: : :t9rm¡:>tfa1; : : : ; alg, every x 2 ¢J there exists a model Ix of w.r.t. SHOQ
.
Proof (of Proposition 5.). Consider an ALO (E LO) ontology O 0 = fA ´
faggA2S~ [ fA ´ ?gA2S¡S~ , which evidently is local, satis¯es Sig(O) \ Sig(O0) µ S and is consistent (O0 6j= > v ?). The conditions of the proposition say that the ontology O [ O
there exists a local ALO (E LO) ontology O0 satisfying