Typed Higher-Order Variant of SROIQ – Why Not? Martin Homola1 , Ján Kl’uka1 , Vojtěch Svátek2 , and Miroslav Vacura2 1 Comenius University in Bratislava Mlynská dolina, 842 48 Bratislava, Slovakia 2 University of Economics, Prague W. Churchill Sq. 4, 130 67 Prague 3, Czech Republic Abstract. We provide T H(SROIQ) a typed higher-order extension of SROIQ, that is itself a syntactic variant of SROIQ, i.e., it is polynomially reducible into it. We also discuss modelling scenarios in which such a language is useful. 1 Introduction Metamodelling, i.e., logical representation of relations (other than subsumption) involv- ing concepts and roles, including their membership in meta-concepts, has been recently subject to an increasing number of research proposals [16,18,15,3,4]. Different applica- tions are cited, roughly divisible into two categories: (i) modelling of certain complex domains, e.g., classifying taxonomic biological concepts such as GoldenEagle and Ac- cipitriformes into higher-order concepts such as Species, Order, etc. [4], or, similarly, classifying GoldenEagle into EndangeredSpecies [15]; or, further, modelling the topic relation, for which values as abstract as whole concepts are sometimes considerable – a book can be about eagles, hence assigning the concept GoldenEagle as a topic may sometimes make sense [16]; and (ii) expressing meta-properties of the modelled enti- ties themselves, such as deprecation of some concepts by assigning them into the Dep- recated meta-concept, or identification of authors of model entities (concepts, roles) using the meta-role definedBy [3], or sorting concepts into diagnostic meta-concepts according to some ontology analysis methodology (e.g., OntoClean [6]) [4]. Metamodelling is not enabled by DL or OWL, however in many ontologies we find hints that it could be useful. In Fig. 1 (a) we can see a usage of the role mo:primary_in- strument from Music Ontology (MO) [21]. Nigel Kennedy’s primary instrument is vio- lin, represented by the individual mo-mit:Violin. This individual in reality represents the notion of violin as a musical instrument type, hence it’s more a “concept” represented by an individual. Indeed we would assert ex:Stradivarius_1707 as its instance. Using classes as property values is not allowed in OWL, hence we need individuals such as mo-mit:Violin. More examples can be seen in Fig. 1 (b): in MO particular CDs (i.e., “true” individuals) are assigned as members to their release by frbr:exemplar_of. A release not just groups individuals released by a publisher at a given time, but also abstracts their common features (i.e, it is more like a concept in this respect). The release “concepts” are categorized into several types (singles, albums, etc.), which in MO are grouped under mo:ReleaseType (i.e, these are already “meta-concepts” in certain sense). Note that we do not suggest that the actual modelling of MO is wrong; in fact it functions well as it is. We are saying that in MO, and in many other Linked Data (LD) meta meta mo:ReleaseType concepts rdf:type meta mo:Instrument mo:Release mo:album concepts rdf:type rdf:type mo:release_type mo-mit:Violin concepts mo:MusicalItem ex:EMI_49557 mo:primary_instrument rdf:type frbr:exemplar_of ex:NigelKennedy ex:Stradivarius_1707 individuals ex:my_CD_0007 mo: primary_instrument (a) (b) Fig. 1. Music Ontology excerpts: (a) primary instrument issue; (b) recognizable higher orders vocabularies, opportunities for more widespread applications of metamodelling can be found, if it was enabled in OWL. It could provide for more obvious models, clearer separation of levels of abstraction, and further logical consequences, as we exemplify it later on (see Sect. 4). From the logical point of view, metamodelling amounts to mod- elling with higher orders. To enable it, DL and OWL have to be extended with such constructs, as already proposed by a number of researchers [15,3,4]. However, this ex- tension needs to be done in a way that is useful and intuitive to the users. We suggest the following properties to be followed: – Clear separation between individuals, roles, concepts, and meta-entities of various kinds, in order to avoid confusing models where one entity has multiple rôles. – Intuitive semantic properties, especially a reasonable relation between intension and extension of concepts to avoid paradoxical and unexpected consequences. – Avoiding unreasonable computational complexity jumps. According to our opinion (see further discussion in Sect. 5) none of the existing approaches yet got thus far. We therefore propose a higher-order extension of SROIQ [12] – the DL behind OWL 2 [17] – in which concepts may be used as individuals (as property values, assigned into meta-concepts, etc.) but which still keeps a strict separation between concepts and roles. The logic, dubbed T H(SROIQ), enables also meta-meta-concepts, and so on, ordered into a hierarchy of higher types. It employs a HiLog-style semantics [1], already used by RDF [7] and likewise other higher-order DL proposals [15,3]. This semantics fulfils some reasonable properties, as we discuss. We further show by reduction that T H(SROIQ) is decidable and in fact its computational complexity is the same as of regular SROIQ. Finally in the second part of the paper we illustrate some modelling scenarios in which our language can be useful. Proofs are included in the extended version of the paper [10]. 2 Preliminaries SROIQ [12] uses a DL vocabulary N = NC ] NR ] NI with countable sets of atomic concepts (NC ), atomic roles (NR ), and individuals (NI ). Complex concepts (complex Table 1. Syntax and Semantics of SROIQ Cons’tor Syntax Semantics Syn. Semantics complement ¬C ∆I \ C I nominal {a} {aI } intersection C u D C I ∩ DI inv. role R− {hy, xi | hx, yi ∈ RI } exist. restr. ∃R.C {x | ∃y hx, yi ∈ RI ∧ y ∈ C I } univ. role U ∆I × ∆I card. restr. >nR.C {x | ]{y | hx, yi ∈ R ∧ y ∈ C } ≥ n} chain (w) S ·Q S I ◦ QI I I self restr. ∃R.Self {x | hx, xi ∈ RI } Axiom Syntax Semantics Syntax Semantics conc. incl. (GCI) CvD C I ⊆ DI concept assert. a : C aI ∈ C I role incl. (RIA) wvR wI ⊆ RI role assertion a, b : R haI , bI i ∈ RI reflexivity assert. Ref(R) RI is reflexive neg. role assert. a, b : ¬R haI , bI i < RI role disjointness Dis(P, R) PI ∩ RI = ∅ 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 C, D are concepts, R is an atomic or inverse role, S , Q are any roles (including role chains), a, b are individuals, and n is a positive integer. A SROIQ knowledge base (KB) is a finite set K of axioms of the types shown in Table 1. A DL interpretation is a pair I = h∆I , ·I i where ∆I , ∅ and ·I is a function such that aI ∈ ∆I for all a ∈ NI , AI ⊆ ∆I for all A ∈ NC , and RI ⊆ ∆I × ∆I for all R ∈ NR . Interpretation of complex concepts and roles is inductively defined as given in Table 1. An axiom ϕ is satisfied by I (denoted I |= ϕ) if I satisfies the respective semantic constraint listed in Table 1, and I is a model of K (denoted I |= 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 C I , ∅. A formula ϕ is entailed by K (denoted K |= ϕ) if I |= ϕ for all models I of K. The two reasoning tasks of concept satisfiability and concept subsumption entailment are inter-reducible [12]. Reasoning in SROIQ is decidable if further syntactic restrictions are applied [12], which are based on the following notions. A role R is simple, if (a) it is atomic and it does not occur on the right-hand side of any RIA; (b) it is an inverse of a simple role S ; (c) if occurs on the right-hand side of a RIA but each such RIA is of the from S v R where S is a simple role. A regular order on roles ≺ is a strict partial order (transitive and irreflexive binary relation) on roles (including inverse roles) such that S ≺ R iff S − ≺ R for any roles S , R. Given a regular order on roles ≺, a RIA is ≺-regular if it has one of the following forms: (a) R·R v R; (b) R− v R; (c) S 1 · · · · ·S n v R and S i ≺ R for 1 ≤ i ≤ n; (d) R·S 1 · · · · ·S n v R and S i ≺ R for 1 ≤ i ≤ n; (e) S 1 · · · · ·S n ·R v R and S i ≺ R for 1 ≤ i ≤ n. Finally, the restrictions placed on SROIQ: (a) only simple roles may appear in car- dinality restrictions; self restriction, and role disjointness axioms; (b) there is a regular order of roles ≺ such that all RIAs in the KB are ≺-regular; (c) the universal role may not appear in any RIA, role reflexivity, nor disjointness axiom. Under these restrictions satisfiability (and thus subsumption) is decidable [12] and it is 2-NExpTime complete [13]. 3 There are additional SROIQ constructors and axioms all of which (including equality) can be reduced to the core constructs listed in Table 1. Table 2. Syntax and HiLog-Style Semantics of T H(SROIQ) tu-role expr. (ρ ) Extension (ρtu E ) tu ρtu ρtu E Rtu Rtu IE R ut − { hy, xi | hx, yi ∈ Rut E } U tu ∆It−1 × ∆Iu−1 S ·Q (w ) S tv E ◦ Qvu E tv vu tu t-description (γt ) Extension (γt E ) γt γt E At At IE ∃Rtu .C u { x | ∃y.hx, yi ∈ Rtu E ∧ y ∈ C u E } ¬C t ∆It−1 \ C t E >nS tu .C u { x | ]{ y | hx, yi ∈ S tu E ∧ y ∈ C u E } ≥ n } C t u Dt C t E ∩ Dt E ∃S tt .Self { x | hx, xi ∈ S tt E } {At−1 } {At−1I } Axiom (ϕ) Semantics (I |= ϕ) ϕ I |= ϕ C t v Dt C t E ⊆ Dt E wtu v S tu wtu E ⊆ S tu E At−1 : C t At−1 I ∈ C t E Ref(Rtt ) Rtt E is reflexive At−1 , Bu−1 : Rtu hAt−1 I , Bu−1 I i ∈ Rtu E Dis(Rtu , S tu ) Rtu E ∩ S tu E = ∅ At−1 , Bu−1 : ¬Rtu hAt−1 I , Bu−1 I i < Rtu E 3 Typed Higher-Order SROI Q 3.1 Syntax We introduce T H(SROIQ), the typed higher-order variant of SROIQ. For any sub- language L of SROIQ, its typed higher-order variant T H(L) is derived analogously. The language is constructed over a vocabulary which explicitly distinguishes between entities of different types. Definition 1 (Typed DL Vocabulary). A typed DL vocabulary N is a disjoint union of a countable number of countable sets of the form t≥0 NCt ] t>0,u>0 NRtu where for each U U t ≥ 0, NCt is the set of concept names of order t, and for each t, u > 0, NRtu is the set of role names between orders t and u. The set NC0 is also called the set of individual names and denoted by NI . The type of a name X ∈ N is either the number t if X is a concept name of order t, or the pair of numbers tu if X is a role name between orders t and u. For clarity of presentation, we introduce the following notation: Symbols of the form At , Bt , . . . belong to NCt , and specifically, symbols of the form A0 , B0 , . . . , a, b, . . . belong to NI . Symbols of the form Rtu , S tu , . . . belong to NRtu . Similarly for longer sym- bols, e.g., NigelKennedy ∈ NC0 , InstrumentType2 ∈ NC2 and primaryInstrument12 ∈ NR12 . Complex concepts and roles are also typed, and can only be combined in ways allowed in the following definition. Definition 2 (tu-role expression, t-description). The sets of tu-role expressions for all t, u > 0 are simultaneously inductively defined as the smallest sets containing the expressions listed in the upper part of Table 2, where Rtu ∈ NRtu , v > 0, S tv is a tu-role expression and Qvu a vu-role expression respectively. We also define (Rtu− )− = Rtu for any Rtu ∈ NRtu . The sets of t-descriptions for all t > 0 are simultaneously inductively defined as the smallest set containing the expressions listed in the middle part of Table 2, where t, u > 0, At ∈ NCt , At−1 ∈ NCt−1 , C t and Dt are t-descriptions, C u is an u-description, and Rtu (Rtt ) is an atomic or inverse tu-role (tt-role). The typing restrictions are quite straightforward: The inverse of a role swaps its source and target orders, a role chain connects roles with matching target and source orders. Only concepts of the same order can be intersected. Restrictions on tu-roles construct descriptions of order t if target descriptions are of order u (or t = u for the self restriction). The nominal constructs a singleton t-concept on top of a (t−1)-concept. Additional concept constructors (t, ∀, 6) can be derived from those listed in Table 2 just as in the first-order SROIQ. Note that there is a separate universal role Utu for each pair of orders t, u > 0, and for each order t > 0, a separate top (bottom) concept >t (⊥t ) can be introduced as an abbreviation of At t ¬At (At u ¬At ) using some At ∈ NCt . Finally, T H(SROIQ) KBs are defined as follows. Definition 3 (Knowledge base). A T H(SROIQ) knowledge base K is a finite set of axioms of the forms listed in the bottom part of Table 2, where t, u > 0, At−1 and Bu−1 are atomic concepts of NCt−1 and NCu−1 , respectively, C t and Dt are t-descriptions, Rtu and S tu are tu-role expressions, Rtt is a tt-role expressions, and wtu is a tu-role chain. We can again see that when an axiom relates two concepts or role expressions, their types must match exactly. On the other hand, the last three axioms, responsible for concept and role membership, assign concepts of a lower order to concepts and roles exactly one order higher. This is a fundamental principle of the type hierarchy (which also exactly reflected by the nominal constructor as discussed above). It turns out that in order to assure decidability of T H(SROIQ) – as we will prove later on – the same syntactic restriction can be applied as in regular SROIQ: (a) only simple roles may appear in cardinality restrictions, self restriction, and role disjointness axioms; (b) all RIAs in the KB are ≺-regular for some regular order of roles ≺; (c) the universal role may not appear in RIAs, role reflexivity, nor disjointness axioms. Simple roles and ≺-regular RIAs are defined exactly as in the previous section. 3.2 Semantics Typed higher-order description logics can be given several semantics, depending on the intended use. In our previous paper [9], we have discussed two options: one based on Henkin’s general models [8] of the simple theory of types, and another based on the HiLog semantics [1] of higher-order logic programming. Both options have been considered in the DL context before (see Sect. 5). Henkin’s semantics, although more straightforward, is not suitable for applications discussed below in Sect. 4. This is due to its extensionality property requiring two concepts to be equal if they have equal sets of instances. We will thus only consider the HiLog-style semantics in this paper. HiLog-style interpretations rely on a single domain ∆I . They first assign each name an element of ∆I serving as the name’s intension, for which we will use the function ·I . The intension is then possibly assigned a concept extension (a subset of the domain ∆I ) and a role extension (a subset of ∆I × ∆I ), for which we will use the function ·E . We obtain a typed version of this semantics by partitioning the domain ∆I into disjoint slices, each dedicated to intensions of members of one type (either a concept type t, or a role type tu). Domain elements are then assigned extensions as appropriate, i.e., concept intensions are only assigned concept extensions, role intensions only role extensions. Definition 4 (HiLog-Style Interpretation). Let N be a typed DL vocabulary. A HiLog- style interpretation of N is a triple I = (∆I , ·I , ·E ) such that 1. ∆I = t≥0 ∆It ] t,u>0 ∆Itu is a disjoint union of countably many sets and ∆I0 , ∅, U U 2. At I ∈ ∆It for each At ∈ NCt and t ≥ 0, 3. Rtu I ∈ ∆Itu for each Rtu ∈ NRtu and t, u > 0, 4. cE ⊆ ∆It−1 for each c ∈ ∆It and t > 0, 5. rE ⊆ ∆It−1 × ∆Iu−1 for each r ∈ ∆Itu and t, u > 0, and the interpretation of role expressions and complex descriptions is inductively de- fined according to, respectively, the upper and middle part of Table 2, where (and thenceforth), by abuse of notation, we redefine X E := (X I )E for atomic concepts and atomic roles, and X E := X E for non-atomic ones. Definition 5 (HiLog-Style Satisfaction). Given a formula (axiom) ϕ in T H(L), a HiLog-style interpretation I = (∆I , ·I , ·E ) satisfies ϕ (denoted I |= ϕ) under the condi- tions specified in the lower part of Table 2. Definition 6 (HiLog-Style Model). A HiLog-style interpretation I = (∆I , ·I , ·E ) is a model of a T H(L) KB K if I |= ϕ for all ϕ ∈ K. As remarked by Chen et al. [1], this way an essentially first-order semantics (free of higher-order power sets) for a higher-order language is obtained. On the other hand, we have to be careful to properly distinguish between the two interpretations ·I and ·E . As argued in our previous work [9], two important properties of a semantics for metamodelling are: Intensional regularity requires that if intensions of two names are equal (K |= At = Bt ), then so are their extensions (K |= At ≡ Bt ). Extensionality, found in set theory, is the converse of intensional regularity (if K |= At ≡ Bt , then K |= At = Bt ). We have come to conclusion that for metamodelling applications where higher-order names are intended to represent concepts, intensional regularity is a desir- able property (see also Example 2 in Sect. 4.1), but extensionality may cause counter- intuitive results. The HiLog-style semantics is intensionally regular, but not extensional, which makes it especially suitable for such applications. Henkin semantics has both properties, which makes it too strong for metamodelling. (For more details see [9].) 3.3 Decidability and Reasoning We will now demonstrate decidability of decision problems in T H(SROIQ) under the HiLog-style semantics, and examine their complexity. In our previous work [9], we have only obtained decidability for T H(ALCHOIQ). The new results for T H(SROIQ) are obtained by a reduction directly to first-order SROIQ, which builds on ideas by Glimm et al. [4]. The first-order reduction matches the duality of intensions and extensions in the HiLog-style semantics by representing each concept At for t > 0 with two names. The concept name At represents the extension. The individual name cAt represents the inten- sion and replaces At when used as an instance of higher-order concepts or a participant in higher-order roles. The relationship between the names At and cAt is expressed by a suitable axiom, which connects exactly the instances of At with cAt via a new instanceOf role, thus ensuring intensional regularity. Let us now define the reduction in detail. Table 3. Components of the first-order reduction Typing(N) > v ∃U.>1 >t v ¬>u for each t, u > 0, t , u At v >t cAt : >t+1 for each At ∈ NCt , t > 0 A0 : >1 for each A0 ∈ NC0 , t > 0 > v ∀Rtu .>u ∃Rtu .> v >t for each Rtu ∈ NRtu , t, u > 0 InstSync(N) At ≡ ∃instanceOf.{cAt } for each At ∈ NCt , t > 0 Definition 7 (First-Order Reduction). Let K be a T H(SROIQ) KB using a vocab- ulary N = t≥0 {NCt } ] t,u>0 {NRtu }. The vocabulary is reduced into a DL vocabulary U U N 1 = (NC , NR , NI ) as follows: ] ] ] ] NC = NCt ] {>t } , NR = NRtu ] {instanceOf} , NI = NC0 ] {cAt | At ∈ NCt } . t>0 t>0 t,u>0 t>0 t The names > , instanceOf, and cAt are fresh, and type indices are parts of these names, not mere annotations. We call cAt the metamodelling individual for At . The first-order reduction of K is a SROIQ KB K 1 over N 1 , defined as follows: K = Bound(K) ∪ Typing(N) ∪ InstSync(N), where Typing(N) and InstSync(N) are 1 defined in Table 3, and Bound(K) is an extension to sets of the following transformation of T H(SROIQ) axioms: 1. each occurrence of a t-description C of the form ¬Dt , ∃Utu .Du , or >nUtu .Du for any n ≥ 0, t, u > 0 is replaced by >t u C; 2. each occurrence of Utu is replaced by U; 3. each occurrence of At ∈ NCt for t > 0 in a nominal, or in the left-hand side of a concept assertion, a (negative) role assertion is replaced by cAt . The reduction fully captures the HiLog-style semantics, or, more formally: Theorem 1. For any T H(SROIQ) KB K in a vocabulary N and any T H(SROIQ) axiom ϕ in N, we have K |= ϕ iff K 1 |= Bound(ϕ). The first-order reduction allows for decidability of T H(SROIQ) with the HiLog- style semantics in the same complexity class as first-order SROIQ. Corollary 1 Concept satisfiability and subsumption in T H(SROIQ) with HiLog sat- isfiability are decidable in 2-NExpTime. Both proofs can be found in the extended version of the paper [10]. 4 Modelling in T H(SROI Q) 4.1 Basic Metamodelling We will remodel the situation from Fig. 1 (a) in T H(SROIQ). Note that we will also slightly change the notation and omit namespaces for simplicity. We can now use indi- viduals for musicians and for particular instruments, 1st -order concepts for instrument types, grouped under the 2nd -order concept InstrumentType2 . See Example 1. Example 1. The fragment in question now looks as follows: NigelKennedy : MusicArtist1 Stradivarius_1707 : Violin1 Violin1 : Instrument2 NigelKennedy, Stradivarius_1707: primaryInstrument11 NigelKennedy, Violin1 : primaryInstrumentType12 Notice that we are now able to assert that Stradivarius_1707 is a Violin1 , while in the original MO this was not possible. We do not yet see any added value in terms of logical consequence though. Consider that our data set is combined with yet another one, describing a different Nigel Kennedy – a drummer. Assume that we have employed an entity recognition tool, which unified both individuals because of the same name. Now, such tools are probably unaware that an artist with two primary instruments of a very different nature is unlikely and should not be unified. However, a slightly modified version of MO, shown in the next example, allows us to detect this discrepancy. Example 2. As instrument types are now concepts, we may model subsumption and disjointness between them properly with GCI axioms. In addition we assert functional- ity on the primaryInstrumentType12 property: Violin1 v Strings1 Drums1 v Percussions1 Strings1 v ¬Percussions1 MusicArtist v 61primaryInstrumentType12 .>2 1 NigelKennedy: MusicArtist1 NigelKennedy, Violin1 : primaryInstrumentType12 NigelKennedy, Drums1 : primaryInstrumentType12 The KB above is consistent, but the concepts Violin1 and Drums1 are both unsatis- fiable: Due to functionality of primaryInstrumentType12 , they have the same intension. Thanks to intensional regularity (cf. Sect. 3.2), this implies they share the same exten- sion, which must be empty, since their respective superconcepts are mutually disjoint. That is, the two concepts are inconsistent, an indicator that something went wrong. Note that this example especially demonstrates that useful consequences are derived by metamodelling combined with reasoning about concepts, which is not possible when concepts are modelled by individuals. 4.2 Beyond the Second Order While our logic can handle concepts of any finite order, only a small number of orders is typically needed. Pan and Horrocks [18] already noted that the object level (order 0) and three additional orders mostly suffice. To see a scenario that goes beyond the second order, let us consider the musical instrument types in a more complex fashion. While generic notions of instruments, such as Violin or Drums, are 1st -order con- cepts, in a typical musical instrument classification, these concepts are further classi- fied into 2nd -order instrument categories. What is more interesting, several instrument classifications have been developed. The classical classification sorts instruments into Woodwind, String, Percussion, and Electronic instruments (and subcatergories). Horn- bostel and Sachs [11] classification sorts instruments into Idiophones, Membranophones, Chordophones, Aerophones and Electrophones (with many more subcategories). How- ever, some modern instruments do not fit in any of these types. The modern classi- fication [14] thus extends Hornbostel-Sachs with additional categories. All instrument categories introduced by classifications are 2nd -order concepts (e.g., Violin is an instance of both String Instrument and Chordophone). We can clearly see, that there are at least three different classifications. To make some order in the vast number of categories, we will introduce concepts Classical In- strument Category, Hornbostel-Sachs Instrument Category, Modern Instrument Category, etc. (all of order 3). Some interesting ontological relations between these 3rd -order con- cepts are apparent: Hornbostel-Sachs Instrument Category is a subconcept of the Modern Instrument Category, while Modern and Classical Instrument Category are disjoint. More examples going up to the 3rd -order are: – Our analysis of Fig. 1(b) uses three orders of concepts: an individual CD (order 0) is classified into its respective release (order 1), releases are classified into different types, such as Single, EP, Album (order 2), instances of Release Type (order 3). – First-order concepts such as Professor, Violinist, Musicologist are rôles assumed by people, in this case, professional rôles. There are also other kinds of rôles, e.g., Su- pervisor and Apprentice (academic rôles), Father and Mother (family rôles). It makes sense to introduce 2nd -order concepts Professional Rôle, Academic Rôle, Family Rôle, which can be all classified into Human Rôle Type (order 3). Note that there can also be Animal Rôle Type (order 3), instantiated by, e.g., Animal Professional Rôle (order 2), classifying concepts such as Rescue Dog or Guard Dog (order 1). – Most cars produced fall under a certain car model, e.g., VW Beetle or Citroën 2CW which are order 1 concepts, subconcepts of Passenger Car (order 1). The concept Car Model is of order 2. Car models are commonly classified as Small Family Car, Sports Car, SUV, . . . (all order 2), which are instances of the Car Model Class con- cept (order 3), while the concept Car Model is not its instance. 4.3 Ontological Background Models Modelling of concepts as individuals and similar approximation techniques are manage- able if used consistently in one ontology. However, in ontology integration and trans- formation, matching entities modelled at different levels of abstraction poses a problem. We have lately proposed so called PURO background modelling language [22] that en- ables to explicitly mark these levels of abstraction in ontologies by annotation. Consider one LD dataset that contains records relating artists to individual instruments, such as Stradivarius_1707, and another dataset relating artists to more abstract instrument types, such as mo-mit:Violin. When populating the latter with data from the former, we want to be aware of the difference, and make the necessary changes. This can be assisted by creating an ontological background model in which the levels of abstractions (i.e., orders) are made explicit. The T H(SROIQ) language may be further useful here, as it allows, in addition, to represent background models logically, reason about them, and represent also relations between the related entities at different levels of abstraction, e.g., by asserting all particular violins on one side as instances of the violin concept on the other side. 4.4 Relationship with Materialization Materialization, as introduced by Pirotte at al. [20], is a relation between a more ab- stract class A and a more concrete class C, which is useful in conceptual modelling. The standard example provided by Pirotte et al. is when A is Car Model and C is Car. The “result” of materialization is that C is partitioned into a set of mutually disjoint sub- classes (in this case, of particular car models) which group those members of C which are related to each respective member of A. Interestingly, Pirotte at al. base their study of materialization on seeing the instances of A, e.g., car models, as “two-faceted” entities with an object facet and a class facet. The object facet describes the common features of a given model. The class facet has individual cars of the model as its instances. In our study, we have considered several such entities, e.g., music releases, musical instrument types, and also car models. In T H(SROIQ), they can be modelled as concepts of order t > 0, whose intensions ·I correspond to the object facets, and extensions ·E to the class facets. “Two-facetedness” of entities is an integral feature of our logic, which thus provides concepts with the ability to participate in roles and as instances in higher-order concepts. This shows that, at least in some cases, materialization manipulates with higher- order constructs – the class C can often be viewed as one order up from A. Notably, this is not always the case: Pirotte et al. give, e.g., an example of stories materializing as plays, which, in turn, materialize as theatrical performances, where all involved classes are naturally of the first order. Finally, while materialization is related to our work in the sense that we propose a DL language offering features which can capture some of the constructs involved (such as two-faceted entities, and the possibility to assert the meta-relation material- izesAs between two classes) Pirotte et al. focus on inheritance of properties along the materialization relation, which we do not study in the current work. It is also obvious that our language enables to model relations between classes unrelated to materializa- tion (modelling the different classifications of musical instrument types and relations between these classifications is a good example of that). 5 Related Work In Table 4 we compare T H(SROIQ) to other similar proposals. Motik [15] and De Giacomo et al. [3] proposed higher-order DLs. Both employ HiLog-style semantics, they are untyped, and with heterogeneous higher-order entities (e.g., a concept may contain any other entity including itself; same entity can act as individual, concept, and role). This limits the expressivity of the underlying language (while maintaining decidability) to ALCHOIQ and SHIQ, respectively. De Giacomo et al. [3] feature intensions also for complex expressions (roles, concepts). To obtain decidability of T H(SROIQ), we have adapted a reduction originally proposed by Glimm et al. [4]. Their work is not primarily concerned with construction and properties of a higher-order DL, instead it offers a way to metamodel higher-order entities directly in SROIQ. This methodology can be indeed used to capture a number of our intended applications. The main difference is that only second-order concepts are supported, and the approach is not characterized in model-theoretic terms. Table 4. Comparison of related higher-order DLs Unlim. Separat. Inter-ord. Intensional Complex Extensio- Expressivity high ords. ords. roles regularity intensions nality Punning Y N Y N N N SROIQ OWL FA Y Y N Y N Y SHOIQ Motik (ν-sem.) Y N Y Y N N ALCHOIQ De Giacomo et al. Y N Y Y Y N SHIQ Glimm et al. N Y Y (1–2) Y N N SROIQ T H(SROIQ) Y Y Y Y N N SROIQ In OWL 2, punning allows to use the same identifier as an individual and also as a class [5]. The two semantic denotations are completely independent, thus intensional regularity is violated. Hence punning is not very well suited for metamodelling [9,15]. Pan et al. proposed RDFS(FA)/OWL FA [18,19], a metamodelling architecture for the Semantic Web. Their approach is interesting as it also clearly separates the higher orders. This work uses Henkin semantics [8]; we have argued that due to its extension- ality it may be too strong for metamodelling [9]. Also, roles connecting different orders are not allowed. Works of Colucci et al. [2] and Szałas [23] apply second-order DLs to non-standard and common-sense reasoning tasks, respectively. 6 Conclusions and Future Work We have proposed a T H(SROIQ), a higher-order variant of SROIQ, with the distinc- tive feature of strictly separated hierarchy of types. Such a variant allows to overcome the first-order nature of OWL, and there is no additional cost for this, because, as we have showed, it is polynomially reducible back to regular SROIQ, hence decidable, and with the same computational complexity (i.e., it is 2-NExpTime complete). An arbitrary number of orders is probably not needed very often, but as we have showed, in certain metamodelling scenarios a combination of meta-concepts and meta- meta-concepts may be useful. T H(SROIQ) can also be used to directly express PURO background models [22] of existing ontologies and LD vocabularies, which is useful for analysis, debugging and integration purposes. While the strict separation of types provides for some order, there are also some cases in which it is limiting, especially in “true” metamodelling, e.g., when captur- ing deprecation or authorship of ontology entities, one might want to have just one Deprecated meta-concept and definedBy meta-role to do this, regardless of the entity being marked. In the future we want to investigate a further extension of the language by such “promiscuous” concepts and roles. Acknowledgments. This work was supported from the EU ICT FP7 under no. 257943 (LOD2 project), from the Slovak projects VEGA 1/1333/12 and APVV-0513-10. References 1. Chen, W., Kifer, M., Warren, D.S.: A foundation for higher-order logic programming. J. Logic Programming 15(3), 187–230 (1993) 2. Colucci, S., Di Noia, T., Di Sciascio, E., Donini, F.M., Ragone, A.: Second-order description logics: Semantics, motivation, and a calculus. In: DL (2010) 3. De Giacomo, G., Lenzerini, M., Rosati, R.: On higher-order description logics. In: DL (2009) 4. Glimm, B., Rudolph, S., Völker, J.: Integrated metamodeling and diagnosis in OWL 2. In: ISWC (2010) 5. Golbreich, C., Wallace, E.K. (eds.): OWL 2 Web Ontology Language New Features and Rationale. Recommendation, W3C (27 October 2009) 6. Guarino, N., Welty, C.: An overview of ontoclean. In: Staab, S., Studer, R. (eds.) The Hand- book on Ontologies, pp. 151–172. IHIS, Springer (2004) 7. Hayes, P. (ed.): RDF Semantics. Recommendation, W3C (10 February 2004) 8. Henkin, L.: Completeness in the theory of types. J. Symbolic Logic 15, 81–91 (1950) 9. Homola, M., Kl’uka, J., Svátek, V., Vacura, M.: Towards typed higher-order description log- ics. In: DL (2013) 10. Homola, M., Kl’uka, J., Svátek, V., Vacura, M.: Typed higher-order variant of sroiq (extended version). Tech. Rep. TR-2014-0042, Comenius University (2014), available online: http: //kedrigern.dcs.fmph.uniba.sk/reports/download.php?id=57 11. von Hornbostel, E.M., Sachs, C.: Systematik der Musikinstrumente. Zeitschrift für Ethnolo- gie 14, 553–590 (1914) 12. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: KR (2006) 13. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: KR. pp. 274–284 (2008) 14. Mann, S.: Natural interfaces for musical expression: Physiphones and a physics-based organology. In: Proceedings of the International Conference on New Interfaces for Musi- cal Expression. pp. 118–123 (2007) 15. Motik, B.: On the properties of metamodeling in OWL. J. Log. Comput 17(4), 617–637 (2007) 16. Noy, N. (ed.): Representing Classes As Property Values on the Semantic Web. Working Group Note, W3C (5 April 2005) 17. OWL Working Group (ed.): OWL 2 Web Ontology Language Document Overview. Recom- mendation, W3C (27 October 2009) 18. Pan, J.Z., Horrocks, I.: RDFS(FA): Connecting RDF(S) and OWL DL. IEEE Trans. Knowl. Data Eng. 19, 192–206 (2007) 19. Pan, J.Z., Horrocks, I., Schreiber, G.: Owl fa: A metamodeling extension of owl dl. In: OWLED (2005) 20. Pirotte, A., Zimányi, E., Massart, D., Yakusheva, T.: Materialization: A powerful and ubiq- uitous abstraction pattern. In: VLDB. pp. 630–641. Morgan Kaufmann (1994) 21. Raimond, Y., Giasson, F. (eds.): Music Ontology Specification (28 November 2010), avail- able online: http://purl.org/ontology/mo/ 22. Svátek, V., Homola, M., Kl’uka, J., Vacura, M.: Metamodeling-based coherence checking of OWL vocabulary background models. In: OWLED (2013) 23. Szałas, A.: Second-order reasoning in description logics. Journal of Applied Non-Classical Logics 16(3-4), 517–530 (2006)