=Paper= {{Paper |id=Vol-1350/paper-32 |storemode=property |title=Towards Expressive Metamodelling with Instantiation |pdfUrl=https://ceur-ws.org/Vol-1350/paper-32.pdf |volume=Vol-1350 |dblpUrl=https://dblp.org/rec/conf/dlog/KubincovaKH15 }} ==Towards Expressive Metamodelling with Instantiation== https://ceur-ws.org/Vol-1350/paper-32.pdf
    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)