We introduce a typed higher-order description logic specifically intended for reasoning about ontological coherence of domain models, motivated by a practical use case from linked data vocabularies.
1 Introduction The advent of the Semantic Web (SW) and especially the Linked Open Data initiative brought an unprecedented amount of new ontology vocabularies that are created, published, and daily instantiated in a number of data sets. At such large quantities, many of the vocabularies were created by developers not trained in ontology design, and were often influenced by the expressive and computational limitations of the SW languages, particularly OWL. Deeper ontological nature of the entities in the modelled domain may not have been considered or is not explicitly captured by these models. This often involves cases when classes are modelled as individuals, or some of the OWL classes in fact ontologically correspond to classes of a higher order.
Consider an example taken from the Music Ontology (MO) [11]: Say we want to model information about a particular LP record in our collection – an exemplar of the famous CBS release of YoYo Ma’s 1983 performance of Bach’s Six Cello Suites. The modelling is depicted in Fig. 1. Our exemplar is represented by the individual ex:my_ LP_0047 (of the type mo:MusicalItem). The record is connected to its release ex:CBS_ 37867, i.e., the collection of all exemplars with the same recording, cover, bar code, etc., as our record. The type of this release is mo:album, which is an individual of the class mo:ReleaseType. The other data is for illustration only. From a strict ontological point of view we may realize that the release ex:CBS_37867 is, in fact, not a singular object per se, but rather it is a class – an entity having a set of instances (i.e., all its exemplars). Similarly, mo:album is a class of releases, but since the releases are themselves classes, mo:album is a 2nd-order class. Finally, the class mo:ReleaseType is of the 3rd order, as it contains 2nd-order classes such as mo:album, mo:single, etc.
So far, our example shows that some relevant ontological background is hidden from the MO vocabulary user, but everything is still coherent. However, one may, for ex:JSB_session_1983 mo:Release mo:interpreter mo:published_as
rdf:type frbr:exemplar_of mo:release_type rdf:type ex:YoYo_Ma
B-object ex:my_LP_0047 rdf:type ex:CBS_37867 mo:MusicalItem
B-type-1 mo:album B-type-2 mo:ReleaseType
B-type-3 instance, create a new class ex:Wish_List and put into it some releases available from a regular reseller, alongside some particular second-hand exemplars of LPs and CDs from an auction web site. The class ex:Wish_List thus becomes incoherent, as it contains entities of di erent ontological nature. Even further, MO provides the mo:primary_ instrument property to indicate the instrument of choice of an artist. It is intended to connect, e.g., ex:YoYo_Ma with mo-mit:Cello, where the latter is one of the predefined individuals corresponding to instrument types (i.e., in reality classes). Some user may however assign ex:Petunia (a particular cello) as Ma’s primary instrument, having this information in her data set. Especially if the data set is later integrated with some other we may get an ontologically incoherent result. However, the resulting OWL ontology would still be logically consistent, and a reasoner would not detect the incoherence.
Recently, we have noted that making the ontological background explicit may help to address problems such as those described above [13,12]. We have proposed so called PURO models [13] which allow to mark background ontological distinctions (called the background model) in a given OWL vocabulary (called the foreground model) via annotations. The background nature of classes, property domains and ranges is indicated by labeling them with background model notions such as B-type-1, B-type-2, etc. In addition, instance–type properties such as mo:release_type, are labeled as B-instantiations. The aim is to keep classes, property domains and ranges homogeneous (containing instances of the same ontological nature), and thus the ontology coherent. Such an approach is useful to both vocabulary designers, in order to keep track of the ontological background, as well as vocabulary users, in order to grasp the background and consistently use the vocabulary. We have also used the model to explain various possible ontological intentions leading to the use of several ontology design patterns [12]. What still lacks here is the option to automatically verify the ontological coherence of the background model represented via the annotation labels.
In this paper, we investigate the extension of description logics (DLs) up to SROIQ with typed higher-order concepts and roles, having in mind the particular application to ontological background coherence checking of OWL vocabularies. We aim to define a DL allowing to directly formalize a background model in the PURO language, and to explore the possibilities for the semantics of this DL. Since PURO models feature higher-order B-types, and relationships between B-types of di erent order, these models can most directly be formalized in a higher-order logic. Moreover, since homogeneity of B-types is a requirement in PURO models, the proposed DL features typing.
Our contribution is as follows: After brief preliminaries (Sect. 2), we introduce the syntax of typed higher-order DLs, and look for a suitable semantics, considering Henkin and HiLog-style semantics, and discussing their properties (Sect. 3). We then show decidability for a limited case of the proposed logic (Sect. 4). Finally, we discuss relevant related work and conclude (Sects. 5 and 6). 2
Preliminaries The SROIQ DL [6] forms the semantic basis of OWL 2 [8] and its sublanguages cover many popular DLs. A DL vocabulary = NC ] NR ] NI is a set of symbols composed of three mutually disjoint countably infinite sets of atomic concepts (NC), atomic roles (NR), and individuals (NI). Complex concepts (complex roles) are defined as the smallest sets containing all concepts and roles that can be inductively constructed using the concept (role) constructors3 in Table 1, where A is any atomic concept, C and D are any concepts, P and R are any atomic roles, S and Q are any (possibly complex) roles, a and b are any individuals, and n stands for any positive integer. A SROIQ knowledge base (KB) is a finite set K of axioms of multiple types as given at the bottom of Table 1.
A DL interpretation is a pair I = h I; Ii where I , ; is the interpretation domain and I is an interpretation function such that aI 2 I for all a 2 NI, AI I for all A 2 NC, and RI I I for all R 2 NR. Interpretation of complex concepts and roles is inductively defined as given in Table 1. An axiom is satisfied by I (denoted I j= ) if I satisfies the respective semantic constraint listed in Table 1, and I is a model of K (denoted I j= K ) if it satisfies all axioms of K .
A concept C is satisfiable w.r.t. K if there is a model of K such that CI , ;. A formula is entailed by K (denoted K j= ) if I j= for all models I of K . The two reasoning tasks of concept satisfiability and concept subsumption entailment are inter-reducible and decidable for SROIQ [6]. However, further syntactic restrictions are required: the universal role cannot occur on the left-hand side of RIA axioms and in role assertions, only so called simple roles may appear in cardinality restrictions, and the role hierarchy needs to be regular. For the lack of space, we are not able to fully cover these restrictions here. The reader is kindly referred to the work of Horrocks et al. [6]. 3 3.1
Typed Higher-Order DL
Syntax Starting from a DL L up to SROIQ we build a typed higher order variant T H (L). The language is constructed over a typed vocabulary which explicitly distinguishes between entities of di erent types. 3 There are additional SROIQ constructors and axioms all of which (including equality) can be reduced to the core constructs listed in Table 1: > reduces to A t :A; ? reduces to A u :A; C t D reduces to :(:C u :D); 8R:C reduces to :9R::C; 6nR:C reduces to :>n+1R:C; =nR:C reduces to >nR:Cu:>n+1R:C; C D reduces to C v D and D v C, a = b reduces to fag fbg, Sym(R) reduces to R v R; Tra(R) reduces to R R v R; Irr(R) reduces to 9R:Self v ?. Definition 1 (Typed DL Vocabulary). A typed DL vocabulary is a disjoint union of a countable number of countable sets of the form ] NCt ] where for each t 0, NCt is the set of concept names of type t, and for each t; u > 0, NRtu is the set of role names between types t and u. In addition, the set of individual names NI = NC0 is equal to the set of concept names of type 0.
For clarity of presentation, we introduce the following notation: symbols of the from At, Bt, . . . belong to NCt, and specifically, symbols of the form A0, B0, . . . , a, b, . . . belong to NI. Symbols of the form Rst, S st, . . . belong to N st. Similarly for longer R symbols, for example, InstrumentType2 2 NC2 and primaryInstrument12 2 NR12.
Complex concepts and roles are also respective to a particular type and may not be arbitrarily combined.
Definition 2 ( tu-role expression). Given a DL L with role constructors CR the set of tu-role expressions of T H (L) is recursively defined as the smallest set containing: 1. Rtu 2. Rut if 2 CR 3. Utu if L allows the universal super-role U 4. S t1u1 S t2u2
1 2 n > 1 is an integer
S ntnun , if 2 CR, where t1 = t, un = u, ui = ti+1 for 1 i < n, and where Rtu is an atomic role in Ntu, and S tu, S tiui are tu- or tiui-role expressions respec
R i tively, for t, u, ti, ui 0 and 1 i n.
Definition 3 ( t-description). Given a DL L with concept constructors CC the set of t-descriptions of T H (L) is recursively defined as the smallest set containing: 1. At 2. :Ct if : 2 CC 3. Ct Dt if 2 CC \ fu; tg 4. Rtu:Cu if 2 CC \ f9; 8g 5. nRtu:Cu if 2 CC \ f6; >g 6. 9Rtt:Self if Self 2 CC 7. fAt 1g if f g 2 CC where At and At 1 are atomic concepts in NCt and NCt 1 respectively, Ct, Dt are tdescriptions, Cu is an u-description, Rtu is a tu-role expression, Rtt is a tt-role expression, for t; u > 0. We further assume that >t = At t :At for t > 0 and some At 2 Nt . C
Definition 4. Given a DL L, a T H (L) knowledge base K is a finite set of axioms of the following forms: 1. Ct v Dt if L allows concept inclusions, 2. Rtu v S tu if L allows role inclusions, 3. Tra(Rtu), Ref(Rtu), Irr(Rtu), Sym(Rtu), Dis(Rtu; S tu), if L allows role transitivity, reflexivity, irreflexivity, symmetry, and disjointness, respectively, 4. At 1 : Ct if L allows concept assertions, 5. At 1; Bu 1 : Rtu if L allows role assertions, 6. At 1; Bu 1 : :Rtu if L allows negative role assertions, where At 1; Bu 1 are atomic concepts of NCt 1 and NCu 1, respectively, Ct, Dt are tdescriptions, Rtu; S tu are tu-role expressions, and t; u > 0. 3.2
Semantics We will now present two of the possible approaches to the semantics of T H (L). The most direct way of interpreting a typed higher-order logic is perhaps to adapt Henkin’s general models [5] of Church’s simple theory of types. Henkin’s semantics deals directly with higher-order structures via a hierarchy of power sets. Let P(S ) = 2S denote the power set of a set S , let P0(S ) = S , and let Pn+1(S ) = P(Pn(S )).
Definition 5 (Henkin Interpretation). Given a T H (L) KB K , a Henkin interpretation is a pair I = (f Isgs; I) where
0I , ;, tI+1 P( tI), and I is an interpretation function that interprets the elements of T H (L) as follows: (a) AtI 2 tI for each At 2 NCt, t 0, (b) RtuI tI 1 uI 1 for each Rtu 2 NRtu, t; u > 0. 2. The domains Is are closed under the interpretation of complex descriptions and role expressions in T H (L), which is inductively defined in the usual way (as in Table 1) with two exceptions for all t; u > 0: (a) (:Ct)I = tI 1 n (Ct)I, (b) (Utu)I = tI 1 uI 1.
The advantage of Henkin interpretations is that the semantics of complex concepts is naturally defined as in any classical DL. For instance (9R23:C3)I = f x j 9y:hx; yi 2 R23I ^ y 2 C3I g; this works in the usual way even if (9R23:C3)I 2 P2( I), i.e., it is a set of sets of elements of I. Similarly the notions of satisfaction, and model are analogous. Definition 6 (Henkin Satisfaction). Given a formula (axiom) in T H (L), a Henkin interpretation I = ( I; I) satisfies (denoted I j= ) as follows: 1. I j= Ct v Dt if CtI DtI, 2. I j= Rtu v S tu if RtuI S tuI, 3. I j= Tra(Rtu) (Ref(Rtu), Irr(Rtu), Sym(Rtu)) if RtuI is a transitive (resp. reflexive, irreflexive, symmetric) relation, 4. I j= Dis(Rtu; S tu) if RtuI and S tuI are disjoint, 5. I j= At 1 : Ct if At 1I 2 CtI, 6. I j= At 1; Bu 1 : Rtu, if hAt 1I; Bu 1Ii 2 RtuI, 7. I j= At 1; Bu 1 : :Rtu if hAt 1I; Bu 1Ii < RtuI.
Definition 7 (Henkin Model). A Henkin interpretation I = ( I; I) is a model of a T H (L) KB K if I j= for all 2 K .
The straightforward interpretation of higher-order classes as sets of sets in Henkin
semantics leads to properties that are not intuitive in knowledge representation, as
discussed below in Sect. 3.3. We therefore consider also HiLog-style semantics which was
successfully applied in higher-order logic programming [
In HiLog [
As remarked by Chen et al. [
Definition 10 (HiLog-Style Model). A HiLog-style interpretation I = ( I; I; E) is a model of a T H (L) KB K if I j= for all 2 K . 3.3
Properties We will now compare the HiLog-style semantics and Henkin semantics, in order to see in which respects they di er, and how suitable each of them is for our use case.
Obviously, Henkin semantics assigns each concept a single semantic object, while the HiLog-style semantics assigns a concept (in our case, only atomic concepts) two separate semantic objects: the concept’s intension and extension. We may then ask the following question: If the intensions of a concept are equal, are the extensions equal as well, and vice versa? This question is formalized as the properties of intensional regularity (1) and extensionality (2):
K j= At = Bt =) K j= At
Bt; K j= At
Bt =) K j= At = Bt: (1) (2)
Intensional regularity is typically a desired property. It also fits our use case, as illustrated in the following example originally studied by Motik [7]: Example 1. Consider the knowledge base K = fAquila1 = Eagle1; Harry0 : Eagle1; Harry0 : :Aquila1g. Given that Aquila1 and Eagle1 are just two di erent names for the same class, which are made equal on the intensional level (i.e., they are the names of the same concept in di erent languages), it is natural to expect that if we put same object into Eagle1 and :Aquila1, the KB becomes inconsistent.
Both Henkin and the HiLog-style semantics are intensionally regular, and so K is inconsistent in both of them. In the case of Henkin semantics, we ought to realize that the axioms Aquila1 = Eagle1 and Aquila1 Eagle1 have exactly the same meaning, as there is just one denotation I for each entity which serves both as its intension and extension at the same time. In the case of the HiLog-style semantics, intensions (Aquila1)I and (Eagle1)I are both equal to the same element d of I, and hence (Aquila1I)E = dE = (Eagle1I)E.
When it comes to extensionality, in most use cases it is undesired. For instance, in meta modelling we want to express versioning meta information within logic, as illustrated in the following example. In OWL, such information can only be expressed using annotation properties.
Example 2. Consider a KB K = fAquila1 Eagle1; Eagle1 : Deprecated2g in which we have two extensionally equivalent classes Aquila1 and Eagle1 and the latter is marked as deprecated. Now deriving K j= Aquila1 : Deprecated2 which is a direct consequence of extensionality is apparently undesired.
While Henkin semantics is inherently extensional for the same reason which makes it intensionally regular (i.e., a single denotation), HiLog-style semantics is not extensional. Indeed, it is possible in a HiLog-style model of K that Aquila1I = a and Eagle1I = e, a , e, but aE = eE, together with e 2 (Deprecated2I)E and a < (Deprecated2I)E.
Interestingly enough, extensionality can be regained by a minor modification to the HiLog-style semantics, as shown in the following proposition proved in Appendix A. Proposition 1. A modified HiLog-style semantics which requires E to be injective has the extensionality property.
Extensionality may be seen as desired in some use cases, e.g., in tight vocabulary integration scenarios we might want to unify classes completely by asserting their equivalence. This is however outside of the scope of our use case.
Finally, we would like to remark that by choosing not to include intensions for complex entities, we made the HiLog-style semantics weaker compared to Henkin semantics. Consider the following example: Example 3. Let us have K = fEagle1 fHarry0g; Aquila1 fMary0g; Harry0 , Marry0; >2 v fEagle1; Aquila1gg in which for whatever reason we decided to limit the number of type-1 classes to two.
While this KB has a HiLog-style model, it has no Henkin model. Henkin semantics requires that each, even non-atomic, description has an interpretation present in the domain. Note that there are only two objects of type 2 available in K , since we have 1I = (>2I) = fE; Ag, E = Eagle1I = fHarry0Ig = fhg and A = Aquila1I = fMarry0Ig = fmg, E , A, h , m. The Henkin interpretation (Eagle1 t Aquila1)I is equal to a fh; mg, which is di erent from both E and A, and so it does not fit in 1I.
This may at first sound as a drawback of the HiLog-style semantics, but in our use case it is not. Since we do not really want to assert higher-order statements over complex concepts or roles, we do not want to care about their intensions. Note that since there is a countable infinite number of complex concept expressions, there can also be an infinite number of intensions. This further adds to the complexity of the semantics, which is not necessary. In the version of HiLog-style semantics used in this paper, we may understand nominals as operating on entities which have explicit identity (intension). If we wish to create an intension for a complex concept, we can always do it by introducing a new atomic name for it, and an equivalence axiom. 4
Decidability We will now demonstrate decidability of decision problems in T H (ALCH OIQ) by reduction to the untyped ALCH OIQ with meta modelling under the HiLog semantics (also called -semantics) as defined and proved decidable by Motik [7]. Definition 11 (ALCH OI Q with Meta Modelling [7]). For a set Na of atomic names, define the set of names as N = Na [ fn j n 2 Nag. For each n 2 Na, let Inv(n) = n , and Inv(n ) = n. The set of ALCH OIQ concepts is the smallest set containing each A 2 N, and for each R; i 2 N, non-negative integer n, and ALCH OIQ concepts C and D, also the concepts fig, :C, C u D, 9R:C, and >nR:C. An ALCH OIQ knowledge base with meta modelling is a finite set consisting of role inclusion axioms R vR S for any R; S 2 N, concept inclusion axioms C vR D for any concepts C and D, and assertions of the forms a : C and a; b : R where C is a concept and a; b; R 2 N. Definition 12 ( -Semantics [7]). Let K be a ALCH OIQ KB with meta modelling. A -interpretation of K is a quadruple I = ( I; I; CI; RI) where I is a non-empty domain, I : N ! I is a name interpretation function, CI : I ! P( I) is an atomic concept extension function, and RI : I ! P( I I) is a role extension function satisfying RI(S I) = RI((Inv(S ))I) . The atomic concept extension function is extended to ALCH OIQ concepts as shown in Table 3 left. Table 3 right defines the -satisfaction relation. The notions of -satisfiability and -model of K are defined as usual. Theorem 1 ([7]). -satisfiability of a KB K in the DL ALCH OIQ with meta modelling is decidable in non-deterministic exponential time.
The following reduction allows application of Motik’s results to T H (ALCH OIQ). X CI (X) A CI(AI) fig fiIg :D I n CI(D) D1 u D2 CI(D1) \ CI(D2) 9S :D f x j 9y:hx; yi 2 RI(S ) ^ y 2 CI(D) g >nS :D f x j ]f y j hx; yi 2 RI(S ) ^ y 2 CI(D) g n g
I j= S vR T RI(S I) RI(T I) D1 v D2 CI(D1) CI(D2) a : D aI 2 CI(D) a; b : S haI; bIi 2 RI(S I) Definition 13 (Untyped Reduction). Let K be a T H (L) knowledge base in a vocabulary = Ut 0 NCt ] Ut;u>0 NRtu. Let Na = ] f>t j t > 0g ] f>tu j t; u > 0g, where >t and >tu for each t; u > 0 are mutually distinct fresh names.
The untyped reduction (K ) of K is a KB in the DL L with meta modelling over the set of atomic names Na defined as (K ) = TB(K ) [ TC(K ), where the type-bound version TB(K ) of K is obtained by replacing each occurrence of a t-description of the form :Ct in K by >t u :Ct, and the set of typing constraints TC(K ) consist of the following axioms (m is the maximum type number occurring in K ): 1. for each t, u, v, w, such that 0 < t; u; v; w m+1,
>t v :>u if t , u, >tu v :>vw if (t; u) , (v; w), 2. At 1 : >t for each At 1 occurring in K , 0 < t m+1; 3. Rtu : >tu for each Rtu occurring in K , 0 < t; u m; 4. At v >t for each At occurring in K , 0 < t m; 5. 9Rtu:> v >t and > v 8Rtu:>u for each Rtu occurring in K , 0 < t; u and >tu v :>v;
Proposition 2. Let K be a T H (L) KB. Then K is satisfiable in the HiLog semantics i (K ) is -satisfiable.
Proposition 2 is proved in Appendix A. Since (K ) can be constructed from K in polynomial time, Theorem 1 and Proposition 2 imply the following corollary. Corollary 1. Satisfiability in T H (ALCH OIQ) in the HiLog semantics is decidable in non-deterministic exponential time. 5
Related Work Considering typed higher order languages for SW vocabularies, our approach relates to the work of Pan and Horrocks [9] who introduced a typed higher-order variant of RDFS, dubbed RDFS(FA). RDFS itself is a higher-order language, however it lacks distinguished types. While RDFS itself employs a HiLog-style semantics, RDFS(FA) resorts to a variant of standard higher-order semantics, a less-general instance of Henkin semantics (see Henkin [5] for detailed comparison). We argued in Sect. 3, that HiLogstyle semantics is more appropriate in our use case.
Both Motik [7] and De Giacomo et al. [2] have investigated higher-order extensions of DL under HiLog-style semantics which are not typed. De Giacomo et al. have studied a stronger variant of the semantics where intensions are assigned also to complex entities. Example 3 can be used to show that these semantics di er, the latter one being the stronger. Our work can be seen as an extension of these two approaches, introducing the types. In Sect. 4, we were able to show the relation with Motik’s semantics by reduction. As noted above, we have intentionally chosen a weaker semantics, similar to the Motik’s one as it is su cient for our use case.
In our previous work [13], we sketched how coherence checking w.r.t. the PURO model can be done using a meta modelling approach. The current work is an improvement, as it allows to reason in both the original vocabulary and the (PURO) meta level at the same time. In this light, we would like to point out the work of Glimm et al. [4], where meta level reasoning (with the OntoClean meta model) is integrated with the original vocabulary via a direct translation into OWL. In the future, we would like to investigate a similar direction in order to obtain e ective reasoning support also for more expressive fragments of T H (SROIQ).
Punning is a new feature of OWL 2 [8] allowing the same name to be used in di erent contexts, e.g., once as a class and then as in individual. As already noted by Motik [7] who investigated a similar approach under the name contextual semantics, it does not satisfy intensional regularity, which we identified as an important property in Sect. 3.3.
Finally, it should also be remarked that scenarios similar to the one outlined in
the introduction could also be modelled with more advanced techniques, such as the
materialization relationship [
Conclusions
The recently introduced PURO model [13] intended for ontological coherence checking
of OWL vocabularies requires consideration of higher-order entities in the vocabularies.
With the aim to enable automated reasoning support for the coherence checking task, we
have investigated a typed higher-order extension of SROIQ, dubbed T H (SROIQ). In
search for a suitable semantics, we have considered a Henkin [5] and a HiLog [
Acknowledgements. This work was supported from the EU ICT FP7 under no. 257943 (LOD2 project), from the Slovak VEGA project no. 1/1333/12, and from the CzechoSlovak bilateral project nos. 7AMB12SK020 (AIP) and SK-CZ-0208-11 (APVV). ISWC (2010) (2007) mendation, W3C (2009)
Data Eng. 19, 192–206 (2007) online: http://purl.org/ontology/mo/ to ontological background models. In: K-CAP (2013)
OWL vocabulary background models. In: OWLED (2013) A
Proofs Proof (Proposition 1, sketch). The proposition is proven by an obvious repetition of the reasoning under Example 2, where we realize that the injectivity of E assures no two distinct intensions can be assigned the same extension. Hence, if extensions of two classes are equal, the same must hold for their intensions.
Us>0;t>0 N st.
R Proof (Proposition 2). Denote the smallest typed DL vocabulary of K by (() Assume
(K ) is -satisfiable and take its -model J = ( J ; J ; CJ ; RJ ). We define a HiLog interpretation I of K as follows: Let tI 1 and tIu := CJ (>tuJ ) for each t; u > 0. Observe that I := U := CJ (>tJ ) for each t > 0, t 0 tI ] Ut;u>0 tIu is indeed a disjoint union, which is ensured by the typing constraints 1 of TC(K ). Let I := J j (the restriction of J to
), and observe that the typing constraints 2 and 3 imply the conditions 2 and 3 of Def. 8. Now let
IC = St>0 tI and
IR = St;u>0 tIu. Since
I C and
IR are disjoint, the union E := CJ j IC [ RJ j IR is a function from constraints 4 and 5 ensure that E satisfies the conditions 4 and 5 of Def. 8.
Observe that RtuE = RJ (Rtu) for all tu-role expressions. Now we can easily verify by induction on the construction of t-descriptions, that CtE = CJ (TB(Ct)). For atomic descriptions, this follows from the typing constrains. For complex descriptions, the only interesting case is the one when Ct is of the form :Dt, and we have CtE = the second equality holds by the induction hypothesis. 2 NCt, t 0, RtuE =
In conclusion, we have AtI = AtJ for all concept names At RJ (Rtu) for all tu-role expressions Rtu over , and CtE = CJ (TB(Ct)) for all t-descriptions Ct over , t; u > 0. These properties allow us to straightforwardly verify that for any axiom 2 K we have I j=
J j= TB( ), which implies satisfiability of K .
()) Assume K has a HiLog model I = ( I; I; E). We construct a -model J of (K ) as follows: Let
> = f t j t > 0g]f tu j t; u > 0g, where t and tu are any mutually distinct objects not occurring in
J := its name interpretation function as NJ := NI for each concept or role name N 2 >tJ := t for each t > 0, and >
tuJ := tu for each t; u > 0. Let IC = St>0 tI and IR = St;u>0 tIu. We define the atomic concept extension function as CJ (c) := cE for , each c 2
IC, as CJ ( t) := tI 1 for each t > 0, as CJ ( tu) := tIu for each t; u > 0, and With the construction of J completed, we can now show similarly as above that we 0, RJ (Rtu) = RtuE for all tu-role have AtJ = AtI for all concept names At
2 NCt, t expressions Rtu over , and CJ (TB(Ct)) = CtE for all t-descriptions Ct over , t; u > 0. These properties allow us to straightforwardly verify that for any axiom I j= i J j= TB( ), which implies -satisfiability of (K ).
>). The role extension function is defined as IR, and as RJ (x) = ; for each x 2