Towards Expressive Metamodelling with Instantiation Petra Kubincová, Ján Kl’uka, and Martin Homola Comenius University in Bratislava, Faculty of Mathematics, Physics, and Informatics, Mlynská dolina, 842 48 Bratislava, Slovakia petra.kubincova@gmail.com, {kluka,homola}@fmph.uniba.sk Abstract. In metamodelling we allow concepts and roles to be classified into “meta” concepts and to be reasoned with as if they were individuals. This is useful in modelling of certain complex domains or in reasoning about ontology entities for sake of verification of methodological constraints. What many proposed meta- modelling languages lack is the ability to model with instantiation – the relation between an instance and a concept it belongs to – similar to the ability to express restrictions on rdf:type in the undecidable OWL Full. We investigate a variant of higher-order description logics combining various desired metamodelling fea- tures, including: (a) a fixly interpreted instanceOf role connecting instances with their concepts, freely usable in modelling; (b) promiscuous concepts that may have individuals, other concepts, and roles as instances at the same time; but also (c) strictly typed concepts allowing only a certain type of instances. We show the decidability of two expressive fragments by means of reduction. Keywords: Description logics, higher-order logic, metamodelling. 1 Introduction Metamodelling allows to model with extensional entities (concepts and roles) as if they were individuals: they may be instances of other concepts, and they may be related to other entities with roles. This is useful in some complex domains with a high number of extensional entities where it makes sense to further categorize them into meta-concepts, and use meta-roles to express relations among them. For example, in the biological tax- onomy the rank Species contains the taxon Giraffa camelopardalis. Taxa are regular concepts (they classify specimens); ranks such as Species and Genus are thus meta- concepts. Ranks may be further classified into meta-meta-concepts, such as Rank. Other applications of metamodelling include reasoning about ontology entities for verification of methodological constraints. More details can be found in the literature [3,4,10,21]. Finding an agreement on how a DL suitable for metamodelling should look like is hard. Logics proposed for this purpose include works of Motik [16] and De Giacomo et al. [3] who take an approach similar to RDF [8] and allow all entities to have threefold semantics – of individual, concept, and role – simultaneously; also concepts and roles are promiscuous – the same concept (role) may contain (connect) any kind of entity. These works rely on HiLog-style semantics developed originally for higher-order Pro- log [2]. It is essentially first-order and corresponds to Ullmann’s meaning triangle [22]: Each entity name is interpreted as an intension – internal meaning with no known struc- ture, thus technically an object. Concept and role extensions are subsequently assigned to intensions. De Giacomo et al. interpret via intensions also concept and role expres- sions, more in the spirit of original HiLog. Homola et al. [11,10] proposed a HiLog-style higher-order DL that is strictly typed, i.e., the entities of different types (and orders) are disjoint. On the other hand, works of Pan et al. [18,19] and Motz et al. [17] rely on the stronger, Henkin’s truly higher-order semantics [9] and are strictly typed. While Ho- mola et al. and Pan et al. sort the higher order entities beforehand, Motz et al. introduce a new kind of axioms (=m ) by which one identifies a concept with an individual when needed. Distinctly, Glimm et al. [4] propose an axiomatization of metamodelling within a DL, relying on companion individuals for all regular concepts, which can then be as- serted into meta-concepts as needed. This work supports only the second order, and the orders are separated. Besides, in OWL 2 there is the option of punning [5], i.e., using the same name in different contexts, which is essentially equivalent to the π-semantics investigated by Motik [16] who showed that there is no semantic relation between the contextually different uses. Finally, OWL Full [20] allows almost arbitrary metamodelling, including restrictions on the language constructs, such as instantiation, subconcept relation, or even restrictions themselves. OWL Full is undecidable and Motik [16] showed that it remains so even if the underlying DL is downgraded to ALC. Interestingly enough, Glimm et al. [4] axiomatized a metamodel of instantiation and, to some extent, also of subsumption in SROIQ. We propose a new variant of higher-order DL for metamodelling with HiLog-style semantics, which combines and unifies some of the approaches listed above. We argue for, and implement the following features: – Basic level of separation between individuals, concepts, and roles is needed, to avoid confusion, and to provide basic sanity checks for the modeller. Therefore individuals, corresponding to particular objects in the world, have no extensions. Concepts have only concept extensions and roles have only role extensions. – Both promiscuous and strictly typed concept and role extensions coexist in the framework and may be freely chosen by the modeller. This allows, e.g., to require that the concept Person has individuals as instances only (it does not make sense for people to have extensions), while in the same ontology the concept Deprecated can have any instances (anything may become deprecated). – In most of the former proposals, meta-levels can be viewed as additional layers in the ontology. Constraints may be modelled inside each layer but they cannot equally penetrate to different layers and create complex inter-layer dependencies. This is possible by modelling with instantiation. In our approach, a fixed role instanceOf connects instances with the concepts they belong to (it has equal se- mantics to rdf:type) and it may be freely modelled with. We are able to require, say, that for each species defined by von Linné there is specimen (instance of the species) in the British Museum. The paper starts with brief preliminaries in Sect. 2. Section 3.1 builds HI(L), a promiscuous higher-order variant of L with instantiation modelling in which roles can- not be classified. Section 3.2 builds HIR(L) which adds the option to classify roles as well. Consequently, Sect. 3.3 shows how strict types are axiomatized in these languages, and Sect. 3.4 reviews the basic properties of these logics. Conclusions follow in Sect. 4. Table 1. Syntax and Semantics of SROIQ Cons’tor Syntax Semantics Syn. Semantics complement ¬C ∆ \C I 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 ∈ RI ∧ y ∈ C I } ≥ n} chain (w) S ·Q S I ◦ QI self restr. ∃R.Self {x | hx, xi ∈ RI } Axiom Syntax Semantics Syntax Semantics I I conc. incl. (GCI) CvD C ⊆D 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 = ∅ 2 Preliminaries 2.1 SROI Q Description Logic SROIQ DL [12] currently constitutes a generally accepted standard for a very expres- sive description logic. It uses a DL vocabulary N = NC ] NR ] NI with countable sets of atomic concepts (NC ), atomic roles (NR ), and individuals (NI ). Complex concepts (com- plex roles) are defined as the smallest sets containing all concepts and roles that can be inductively constructed using the concept (role) constructors1 in Table 1, where C, D are concepts, P, R are atomic or inverse roles, 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 ; or (c) it occurs on the right-hand side of a RIA, but each such RIA is of the form 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. 1 There are additional SROIQ constructors and axioms all of which, including individual equality (=), are reducible to the core constructs listed in Table 1. Table 2. Syntax and ν-semantics of SHOIQmm Cons’tor Syntax Semantics Syn. Semantics I I intersection D1 u D2 C (D1 ) ∩ C (D2 ) complement ¬D ∆I \ C I (D) exist. restr. ∃S .D { x | ∃y hx, yi ∈ R (S )∧ y ∈ C (D) } I I nominal {a} {aI } card. restr. >nS .D { x | ]{y | hx, yi ∈ R (S )∧ y ∈ C (D)} ≥ n } I I Axiom Syntax Semantics Syntax Semantics I I conc. incl. (GCI) D1 v D2 C (D1 ) ⊆ C (D2 ) role incl. (RIA) S 1 vR S 2 RI (S 1 ) ⊆ RI (S 2 ) transitivity S 1 ·S 1 vR S 1 RI (S 1 ) is transitive concept assertion a : D1 aI ∈ C I (D1 ) role assert. a, b : S 1 haI , bI i ∈ RI (S 1 ) 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 N2ExpTime complete [14]. 2.2 DLs with Metamodelling and the ν-Semantics Motik [16] has proposed DLs for metamodelling with HiLog-based ν-semantics. In DL applications of HiLog semantics [2], names (and sometimes expressions) are first assigned domain objects called intensions, which, in turn, are assigned extensions: sets of intensions for concepts, or sets of pairs of intensions for roles. When treated as a concept instance or a role actor, the semantics of a name is its intension. When treated as a concept or a role, the extension of the name’s intension is considered. Motik’s DL SHOIQ with metamodelling (abbreviated to SHOIQmm) uses a set of names N = Na ∪{ n− | n ∈ Na } where Na is a set of atomic names. The set of concepts is the smallest superset of N containing all concepts that can be inductively constructed using the constructors in Table 2, where D1 and D2 are concepts, a, S ∈ N, and n is a non-negative integer. A SHOIQmm knowledge base is a set K of axioms of the forms listed in Table 2 where S 1 , S 2 , a, b ∈ N, and D1 , D2 are concepts. Simple names are defined as SROIQ simple roles (using vR instead of v). A KB K employs the unique role assumption (URA) if ({S 1 } v ¬{S 2 }) ∈ K for each two distinct names S 1 and S 2 occurring as roles in K. A ν-interpretation is a quadruple I = h∆I , ·I , C I , RI i where ∆I , ∅ is a domain set, ·I : N → ∆I is a name interpretation function, C I : ∆I → 2∆ is an atomic concept ex- I ∆I ×∆I tension function and R : ∆ → 2 I I is a role extension function. The extension of C I to concepts and ν-satisfaction of axioms (I |= ϕ) are specified in Table 2. The notions of ν-model and ν-entailment are defined analogously to their SROIQ counterparts. A concept D is ν-satisfiable w.r.t. K if C I (D) , ∅ in some ν-model I of K. Decidability of ν-satisfiability in NExpTime was proved by Motik [16] if (a) only simple names appear in cardinality restrictions, and (b) the KB employs URA, or con- tains no nominals and no cardinality restrictions. Table 3. Syntax and semantics of HI(SROIQ) and HIR(SHOIQ) Syntax Extensions in HI(SROIQ) Extensions in HIR(SHOIQ) R0 RIE 0 RIE 0 R− { (y, x) | (x, y) ∈ R } E { (y, x) | (x, y) ∈ RE } U (∆II ] ∆IC ) × (∆II ] ∆IC ) – S ·Q S E ◦ QE RE ◦ RE for S = R, Q = R instanceOf { (x, y) | x ∈ ∆II ] ∆IC ∧ y ∈ ∆IC ∧ x ∈ yE } { (x, y) | x ∈ ∆I ∧ y ∈ ∆IC ∧ x ∈ yE } A AIE AIE ¬C (∆II ] ∆IC ) \ C E ∆I \ C E CuD C E ∩ DE C E ∩ DE {B} {BI } {BI } ∃R.C { x | ∃y.(x, y) ∈ RE ∧ y ∈ C E } { x | ∃y.(x, y) ∈ RE ∧ y ∈ C E } >nR.C { x | #{ y | (x, y) ∈ RE ∧ y ∈ C E } ≥ n } { x | #{ y | (x, y) ∈ RE ∧ y ∈ C E } ≥ n } ∃R.Self { x | (x, x) ∈ RE } – CvD C E ⊆ DE C E ⊆ DE B: C BI ∈ C E BI ∈ C E B1 , B2 : R (BI1 , BI2 ) ∈ RE (BI1 , BI2 ) ∈ RE B1 , B2 : ¬R (BI1 , BI2 ) < RE – wvR wE ⊆ RE wE ⊆ RE for w = P or w = R · R Dis(P, R) PE ∩ RE = ∅ – 3 Higher-Order DLs with Promiscuous Concepts and Instantiation Modelling The logics HI(L) and HIR(L) defined in this section for an underlying first-order DL L rely on HiLog-style semantics. They feature promiscuous higher-order concepts with different types of entities allowed as instances. In addition, the fixed instanceOf role metamodels the instantiation relation, and it is usable in axioms like any other role. The letter H stands for higher-order, I for instanceOf, and R for metamodelling of roles. 3.1 Promiscuous Concepts and Instance Modelling We first define HI(SROIQ), a higher-order variant of SROIQ allowing individuals and concepts to be classified, and featuring the instanceOf role. Roles relate both in- dividuals and concepts with one another, but they cannot be classified. HI(L) for a fragment L of SROIQ is the corresponding fragment of HI(SROIQ). In some HiLog-based DLs [16,3], names designate intensions and are fully inter- changeable as individuals, concepts, and roles, depending on their occurrence. We be- lieve that such an approach is less suitable in the realm of DLs. The individual-concept- role distinction is fundamental from the ontological standpoint (see, e.g., [6, Pt. II], [7, Ch. 4, 6, 7], [21]) and dates back to Aristotle [1, 2a11, 6a37]. This distinction also saves users accustomed to first-order DLs from surprises, and provides basic sanity checks. Let us now define the syntax of HI(SROIQ). Note that the instanceOf role can occur anywhere where any regular atomic role can. Definition 1. Let N = NI ] NC ] NR be a DL vocabulary such that instanceOf ∈ NR . HI(SROIQ) role expressions are inductively defined as the smallest set containing the expressions listed in Table 3 (upper part), where R0 ∈ NR \ {instanceOf, U}, R is an atomic or inverse role, S and Q are role expressions. HI(SROIQ) descriptions are inductively defined as the smallest set containing the expressions listed in Table 3 (middle part), where A ∈ NC , B ∈ NI ] NC , C and D are descriptions, and R is an atomic or inverse role. A HI(SROIQ) knowledge base K is a finite set of axioms of the forms listed in Table 3 (bottom part), where B, B1 , B2 ∈ NI ] NC , C and D are descriptions, P and R are atomic or inverse roles, and w is a role chain. HI(SROIQ) easily models the taxonomic example from the Introduction. Taxons are classified to meta-concepts of ranks (Species, Genus, . . . ), ranks to the meta-meta- concept Rank (1). Metaconcepts are axiomatized just as concepts (2). G. camelopardalis : Species Giraffa : Genus Species : Rank Genus : Rank (1) Species t Genus t · · · v Taxon Species u Genus v ⊥ (2) Metaroles with concepts on one or both sides of the relationship allow specifying that a taxon or rank was definedBy a person (3), and that one species is an evolution- ary successorOf of another (4). We can then express complex meta-concepts such as LinneanSpecies (5). ∃definedBy.> v Taxon t Rank > v ∀definedBy.Person Giraffa, M. T. Brünnich : definedBy (3) ∃successorOf.> v Species > v ∀successorOf.Species (4) LinneanSpecies ≡ Species u ∃definedBy.{vonLinné} (5) First-order modelling still works as in SROIQ: Individual organisms are classified to taxons and particular species are subsumed by their respective genera (6). Roles record that a specimen (a studied example individual of a species) was describedBy a person, and is locatedIn a museum (7). Zarafa : G. camelopardalis G. camelopardalis v Giraffa Specimen v Organism (6) ∃describedBy.>t∃locatedIn.> v Specimen > v ∀describedBy.Personu∀locatedIn.Museum (7) HI(SROIQ) employs HiLog-based semantics: each entity is denoted to a domain element (the intension) using the intension function ·I . The intensions for individuals, concepts, and roles are disjoint. Intensions of concepts (roles) are assigned concept (role) extensions. Only one extension function ·E is therefore needed, unlike in the ν- semantics. The instanceOf role has fixed semantics: it connects an instance with the intension of each concept it belongs to – i.e., just like rdf:type in RDF [8]. Definition 2. An HI-interpretation of a DL vocabulary N with instanceOf ∈ NR is a triple I = (∆I , ·I , ·E ) such that: 1. ∆I = ∆II ] ∆IC ] ∆IR where ∆II , ∆IC , ∆IR are pairwise disjoint, 2. aI ∈ ∆II for each a ∈ NI , AI ∈ ∆IC for each A ∈ NC , RI ∈ ∆IR for each R ∈ NR , 3. cE ⊆ ∆II ] ∆IC for each c ∈ ∆IC , rE ⊆ (∆II ] ∆IC ) × (∆II ] ∆IC ) for each r ∈ ∆IR . Extensions of role expressions RE and of descriptions C E are inductively defined ac- cording to Table 3. The semantics of axioms (and of nominals above) is defined so that when a name is treated as a concept instance or a role actor, its intension is considered. Definition 3. An axiom ϕ is satisfied by a HI-interpretation I (I |= ϕ) if I satisfies the respective semantic constraints from the lower part of Table 3. A HI-interpretation I is a model of K (I |= K) if I satisfies every axiom ϕ ∈ K. A concept C is satisfiable w.r.t. K if there exists a model I of K such that C I , ∅. An axiom ϕ is entailed by K (K |= ϕ) if I |= ϕ holds for each I such that I |= K. The semantics of instanceOf should now be apparent. The fixed interpretation of this role allows to “move accross” meta-layers in modelling: Restrictions on instanceOf can select instances of concepts satisfying various meta-criteria, e.g., specimens of Lin- nean species described by someone else than von Linné (8). Conversely, restrictions on instanceOf− select concepts whose instances satisfy complex criteria, e.g., species with specimens located in the British Museum. Liberal treatment of the instanceOf role allows creating its subroles, e.g., hasType assigning a prototypical specimen to each species (10), and using them in number restrictions, e.g., to assert that each species has exactly one holotype (the “most notable” specimen) and it is located in a major museum (11). While we could have created the meta-role hasType anyway, without relating it to instanceOf we could not assure that it connects each species with one of its instances. Specimen u ∃instanceOf.(Species u ∃definedBy.{vonLinné}) u ∃describedBy.¬{vonLinné} (8) Species u ∃instanceOf− .(Specimen u ∃locatedIn.{britishMusem}) (9) hasType v instanceOf− ∃hasType.> v Species > v ∀hasType.Specimen (10) Species v (61hasType.Holotype) u =1hasType.(Holotype u ∃locatedIn.MajorMusem) (11) We will now show how HI(SROIQ) can be reduced to first-order SROIQ. The reduction, fully defined below, is based on ideas by Glimm et al. [4]. For each concept A, a new individual name cA is introduced to represent A’s intension. These new names are instances of a new concept >C of concept intensions. The relationship between the extension A and the intension cA is expressed through the instanceOf role in the InstSync axioms. In the reduced knowledge base, instanceOf is an ordinary, axiomatized role. Definition 4 (First-Order Reduction). A DL vocabulary N with instanceOf ∈ NR is re- duced into a DL vocabulary N 1 := (NC1 , NR1 , NI1 ) where NC1 = NC ]{>C }, NR1 = NR , NI1 = NI ] {cA | A ∈ NC } for fresh names >C and cA for all A ∈ NC . A given HI(SROIQ) KB K in N is reduced into a SROIQ KB K 1 := Bound(K) ∪ InstSync(K) ∪ Typing(K) in N 1 where Bound(K) is obtained from K by replacing each occurence of A ∈ NC in a nominal or in the left-hand side of a concept or (negative) role assertion by cA . InstSync(K) consists of axioms A ≡ ∃instanceOf.{cA } for all A ∈ NC . Typing(K) con- sists of axioms > v ∀instanceOf.>C , a : ¬>C and cA : >C for all a ∈ NI and A ∈ NC . The following theorem asserts that K 1 is just as strong as K. The more involved part of its proof is finding a HI(SROIQ) model I of K for a first-order model J of K 1 . We define the set of concept intensions ∆IC as >J C , and let the intension of each atomic con- cept A be cJ A . We then define for each concept intension c ∈ ∆C the extension c as the I E set of all xs related to it by instanceOf . This ensures instanceOf = instanceOf . More- J E J over, since the interpretation of instanceOf is constrained by the InstSync axioms, ex- tension of each atomic concept AIE is equal to its first-order interpretation AJ . A more detailed proof of the theorem can be found in the extended version of this paper [15]. Theorem 1. For any HI(SROIQ) KB K and any axiom ϕ in a common vocabulary N, we have K |= ϕ iff K 1 |= Bound(ϕ). Observe that K 1 is linear in the size (string-length) of K (assuming N consists exactly of all symbols occurring in K). If K satisfies, for all roles including instanceOf, the SROIQ restrictions (cf. Sect. 2.1), so does K 1 . Corollary 1. Concept satisfiability and subsumption in HI(SROIQ) conforming to SROIQ restrictions on roles including instanceOf are decidable in N2ExpTime. In general, HI(L) reduces to LO if the DL L admits GCIs, existential restric- tion, and complement. The decidability and complexity of standard reasoning tasks for HI(L) are then the same as for LO. A natural next step after metamodelling instantiation is metamodelling subsump- tion. For a singleton meta-concept C, the meta-concept ∀instanceOf− .∃instanceOf.C, due to Glimm et al. [4], classifies subconcepts of the single instance of C. We can thus express that all species of genus Giraffa except G. camelopardalis are extinct (12). Glimm et al. [4] axiomatized a subClassOf role over atomic concepts, but, unlike instanceOf, it does not extend to unnamed concept intensions. Metamodelling of subsumption with the intended semantics { (x, y) | x, y ∈ ∆IC ∧ xE ⊆ yE } is a part of our near-future work. Species u ∀instanceOf− .∃instanceOf.{Giraffa} u ¬{G. camelopardalis} v Extinct (12) 3.2 Classification of Roles We now define another variant of higher-order DL with a notable addition: allowing concepts to contain and roles to connect also atomic role names. We define the logic HIR(SHOIQ), on top of the SHOIQ DL [13] disallowing some SROIQ constructs (we say that an expression is allowed if its extension is defined in the right column of Table 3). HIR(L) for a fragment L of SHOIQ is the corresponding fragment of HIR(SHOIQ). HIR uses the same vocabulary as HI. The most notable syntactic difference for HIR(L) compared to HI(L) is the op- tion to use atomic roles as individuals. The full syntax is as follows. Definition 5. HIR(SHOIQ) role expressions are inductively defined as the smallest set containing the allowed expressions listed in the upper part of Table 3, where R0 ∈ NR \ {instanceOf}, R is an atomic or inverse role. HIR(SHOIQ) descriptions are inductively defined as the smallest set containing the allowed expressions listed in the middle part of Table 3, where A ∈ NC , B ∈ N, C and D are descriptions and R is an atomic or inverse role. A HIR(SHOIQ) knowledge base K is a finite set of allowed axioms of the forms listed in the bottom part of Table 3, where B, B1 , B2 ∈ N, C and D are descriptions, P and R are atomic or inverse roles. In contrast to HI, HIR extensions range over all intensions, and hence concepts in HIR(L) are fully promiscuous, though about each instance we are able to say if it is an individual, concept, or role. In many cases such promiscuity is not desired; we will later learn how to constrain it if needed. However, there are certain concepts such as Deprecated for which it makes sense. Concepts, but as well roles, and even individuals may become deprecated if they are replaced by new names or more refined versions. In the taxonomy domain, taxa, ranks, end even specimens may become deprecated (e.g., when they are invalidated by further studies). A role with a truly promiscuous domain is, e.g., definedBy; as it is applicable on both taxa and ranks. Definition 6. An HIR-interpretation of a DL vocabulary N with instanceOf ∈ NR is a triple I = (∆I , ·I , ·E ) such that 1. ∆I = ∆II ] ∆IC ] ∆IR (all three sets pairwise disjoint), 2. aI ∈ ∆II for each a ∈ NI , AI ∈ ∆IC for each A ∈ NC , RI ∈ ∆IR for each R ∈ NR , 3. cE ⊆ ∆I for each c ∈ ∆IC , rE ⊆ ∆I × ∆I for each r ∈ ∆IR , and the extensions of role expressions and complex descriptions are inductively defined according to Table 3. Satisfiability, model, and entailment are defined as for HI(SROIQ). We will now reduce HIR(SHOIQ) to SHOIQmm under ν-semantics. While there are similarities with the previous first-order reduction, the target is now already a HiLog-based higher- order logic. The core idea is to separate concepts, individuals, and roles which are not distinguished by SHOIQmm. We introduce >I , >C and >R , representing disjoint top- concepts for individuals, concepts, and roles (their union being >0 ). The instanceOf role is reduced into an ordinary role with domain >0 and range >C , axiomatized through InstSync axioms. As SHOIQmm uses a set of names including an inverse name n− for each atomic name n, we also introduce >− to handle all inverse names separately. Definition 7 (Reduction to SHOI Qmm with ν-semantics). A DL vocabulary N with instanceOf ∈ NR is reduced into the set of atomic names Naν = NI ] NC ] NR ] {>C , >R , >I , >0 , >− } for fresh names >C , >R , >I , >− , and >0 . HIR(SHOIQ) KB K in N is reduced into a SHOIQmm KB K ν in N ν as fol- lows: K ν = Bound(K) ∪ InstSync(K) ∪ Typing(K), where InstSync(K) contains A ≡ ∃instanceOf.{A} for all A ∈ NC , Bound(K) contains for each ϕ ∈ K its transformed version where every occurrence of a description C in the form ¬D is replaced by >0 uC and every RIA w v S is replaced by w vR S . Typing(K) consists of axioms: 1. ¬({instanceOf, >C , >R , >I , >0 , >− } t >− ) ≡ >0 ≡ >C t >R t >I , 2. >C u >I v ⊥, >C u >R v ⊥, >R u >I v ⊥, 3. > v ∀instanceOf.>C , ∃instanceOf.> v >0 , 4. (i) a : >I for all a ∈ NI , (ii) A : >C , A v >0 for all A ∈ NC , (iii) R : >R , > v ∀R.>0 , ∃R.> v >0 for all R ∈ NR \ {instanceOf}, (iv) n− : >− for all n ∈ N ν . The following theorem states that K ν is just as strong as K. Its proof is similar to the proof of Theorem 1, and is included in the extended version [15]. Theorem 2. For any HIR(SHOIQ) KB K and axiom ϕ over a common vocabu- lary N, we have K |= ϕ iff K ν |= Bound(ϕ). The ν-reduction of a HIR(SHOIQ) KB K is linear in the size of K. Simple roles are defined as for SROIQ. URA is defined as for SHOIQmm, but only for names from NR . We can now state the following corollary. Its assumptions suffice to satisfy the decidability conditions of ν-satisfiability of K ν from Sect. 2.2. Table 4. Knowledge base with n types > v ∀instanceOf .>X(t−1) for each t s. t. t > 0 X(t) − a : >I(1) for each a ∈ NI >X(t) v ¬>Y(u) for each t, u s. t. 0 < t, u ≤ n ∧ t , u >IR(1) ≡ >I(1) t >R(1) R : >R(1) for each R ∈ NR Corollary 2. Let a HIR(SHOIQ) KB K be such that (a) only simple roles occur in cardinality restrictions, and (b) K employs URA, or it contains no nominals and no cardinality restrictions. Concept satisfiability and entailment in a HIR(SHOIQ) KB are then decidable in NExpTime. Note that the reduction theorem can be generalized to reducibility of HIR(L) to LOmm, if L admits GCIs, existential restriction, and complement. 3.3 Type Hierarchy Strikes Back In HI(L) (HIR(L)), concepts are promiscuous – any individuals, concepts (and roles) may become their instances. In case selected concepts need to be strictly typed, this is axiomatized as follows: Definition 8 (Typing framework). Given n ∈ N, a HI KB with n types adds fresh concepts names >I(i) for each i such that 0 < i ≤ n, and contains axioms listed in the upper part of Table 4 for X = Y = I. A HIR KB with n types adds fresh concept names >X(i) for each i, 0 < i ≤ n, and each X ∈ {I, R, IR}, and contains axioms listed in the upper and lower part of Table 4 for all X, Y ∈ {I, R, IR}. The >I(1) concept classifies precisely all individuals (similarly, >R(1) classifies pre- cisely all roles and >IR(1) classifies precisely all individuals and roles), >I(2) classifies precisely all concepts with only individual instances (analogously, >R(2) for concepts of roles, and >IR(2) for mixed concepts), etc. We can thus assert some typing in our example: Organism t Person t Museum v >I(1) Taxon v >I(2) Rank v >I(3) Typing is propagated to subconcepts and instances: G. camelopardalis v >I(1) and Species v >I(2) is now entailed, and so for other taxa and ranks. Domains and ranges of roles may be typed similarly, e.g.: ∃successorOf.> v >I(2) and > v ∀successorOf.>I(2) . This, though, is also already entailed, since Species was already asserted as the domain and range, and it is already typed. 3.4 Some Properties of HI (SROI Q) and HI R(SHOI Q) HI(SROIQ) and HIR(SHOIQ) have the basic properties of HiLog-based logics: intensional regularity K, (X = Y) |= X ≡ Y, and the lack of extensionality K, (X ≡ Y) |= X = Y. Indeed, if K |= A = B for two concept names A and B, then K |= A ≡ B, since in every model AI = BI , hence also AIE = BIE . Both logics are thus intensionally regular for concepts. This is a quite natural requirement for metamodelling. If we assert that an international and a Slovak name denote the same species (G. camelopardalis = Žirafa štíhla), we expect their extensions to also be equal. HIR(SHOIQ) is intensionally regular also for roles, but K never entails R = S under decidability conditions. A model of a KB such that K |= A ≡ B can assign A and B distinct intensions AI = a , b = BI with the same extension, e.g., aE = bE = {x}. Both our logics thus lack extensionality. This enables, e.g., deprecating an old binomial name of a species (e.g., Cervus camelopardalis) without deprecating its newer name (Giraffa camelopardalis) al- though they classify the same organisms (Giraffa c. ≡ Cervus c.), or modelling of single- species genera such as Sommeromys ≡ S. macrorhinos, where S. macrorhinos : Species and Sommeromys : Genus without contradicting Species u Genus v ⊥. HI(SROIQ)’s expressivity makes it vulnerable to Russel’s paradox of naïve set theory. A concept of such concepts which are not instances of themselves is defined as Barber ≡ ¬∃instanceOf.Self. Take any HI(SROIQ) model I of K, and let b := BarberI ∈ ∆C , B := bE , and S := ∃instanceOf.Self = { x | (x, x) ∈ instanceOfE } = { x | x ∈ ∆C ∧ x ∈ xE }. We have B = (∆I ] ∆C ) \ S = ∆I ] (∆C \ S ) = ∆I ] { x | x ∈ ∆C ∧ x < xE }. Hence the contradiction: b ∈ bE iff b < bE . Even though SHOIQ does not admit self-restriction, simpler contradictions involving instanceOf, e.g., x : Y and (x, Y) : ¬instanceOf, can be expressed in HIR(SHOIQ). However, these examples are actually not specific to HI or HIR logics, as they reduce to contradictory SROIQ and SHOIQmm KBs, respectively. 4 Conclusions We have introduced a higher-order framework HIR(L) which enriches a DL L with promiscuous higher-order concepts, and makes the instantiation relation accessible to the modeller in the form of a fixly interpreted role named instanceOf, whose semantics is akin to rdf:type. We showed a number of examples illustrating how such constructs may be useful for metamodelling. Our work is most closely related to that of Homola et al. [10] which is here extended by promiscuity and modelling with instantiation. The former approach is strictly typed; types are easily constructed in HIR(L) by axiomatization if needed, and may be used – but they are not strictly enforced. We base many of our constructions on Glimm et al. [4] who, however, do not enable orders higher than the second, meta-roles, nor promiscuity. They also do not provide any higher-order model-theoretic characterization, only an axiomatization in a regular DL. Such characterization is instrumental in showing that the logic has desired properties, which we have discussed in Sect. 3.4. Computational support for logics up to HIR(SHOIQ) can be obtained via a re- duction to Motik’s extension of SHOIQ with metamodelling (under ν-semantics). For the weaker variant HI(L), which disallows classification of roles, HI(SROIQ) is fully reducible to regular SROIQ by adapting the reduction known from Glimm et al. The question whether the subsumption relation and further logical constructs of the un- derlying DL can be made accessible for metamodelling is an interesting open problem. Acknowledgments. This work was funded by project VEGA 1/1333/12. Petra Kubin- cová received an extraordinary scholarship awarded by Faculty of Math., Physics, and Informatics. We thank Miroslav Vacura and Vojtěch Svátek for valuable suggestions. References 1. Aristotle: The Categories, On Interpretation, Prior Analytics. The Loeb Classical Library, Harvard University Press, Cambridge, MA (1962), transl. by Tredennick, H., Cook, H.P. 2. Chen, W., Kifer, M., Warren, D.S.: A foundation for higher-order logic programming. J. Logic Programming 15(3), 187–230 (1993) 3. De Giacomo, G., Lenzerini, M., Rosati, R.: Higher-order description logics for domain meta- modeling. In: AAAI (2011) 4. Glimm, B., Rudolph, S., Völker, J.: Integrated metamodeling and diagnosis in OWL 2. In: ISWC (2010) 5. Grau, B.C., Horrocks, I., Motik, B., Parsia, B., Patel-Schneider, P., Sattler, U.: OWL 2: The next step for OWL. Web Semantics: Science, Services and Agents on the World Wide Web 6(4), 309–322 (2008) 6. Grossmann, R.: The Categorial Structure of the World. Indiana University Press, Blooming- ton (1983) 7. Guizzardi, G.: Ontological Foundations for Structural Conceptual Models. Telematics Insti- tuut, Enschede (2005) 8. Hayes, P.J., Patel-Schneider, P.F. (eds.): RDF 1.1 Semantics. W3C Recommendation (25 February 2014) 9. Henkin, L.: Completeness in the theory of types. J. Symbolic Logic 15, 81–91 (1950) 10. Homola, M., Kl’uka, J., Svátek, V., Vacura, M.: Typed higher-order variant of SROIQ – why not? In: DL (2014) 11. Homola, M., Kl’uka, J., Svátek, V., Vacura, M.: Towards typed higher-order description log- ics. In: DL (2013) 12. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: KR (2006) 13. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. J. Autom. Reasoning 39(3), 249–276 (2007) 14. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: KR. pp. 274–284 (2008) 15. Kubincová, P., Homola, M., Kl’uka, J.: Towards expressive metamodelling with instantiation (extended version). Tech. Rep. TR-2015-045, Comenius University (2015), available online: http://kedrigern.dcs.fmph.uniba.sk/reports/download.php?id=60 16. Motik, B.: On the properties of metamodeling in OWL. J. Log. Comput 17(4), 617–637 (2007) 17. Motz, R., Rohrer, E., Severi, P.: Reasoning for ALCQ extended with a flexible meta- modelling hierarchy. In: JIST 2014 (2014) 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. Schneider, M. (ed.): OWL 2 Web Ontology Language RDF-Based Semantics. W3C Recom- mendation, 2nd edn. (11 December 2012) 21. Svátek, V., Homola, M., Kl’uka, J., Vacura, M.: Metamodeling-based coherence checking of OWL vocabulary background models. In: OWLED (2013) 22. Ullmann, S.: Semantics: An introduction to the science of meaning. Barnes & Noble, Inc., New York (1962)