=Paper= {{Paper |id=Vol-1193/paper_56 |storemode=property |title=Typed Higher-Order Variant of SROIQ - Why Not? |pdfUrl=https://ceur-ws.org/Vol-1193/paper_56.pdf |volume=Vol-1193 |dblpUrl=https://dblp.org/rec/conf/dlog/HomolaKSV14 }} ==Typed Higher-Order Variant of SROIQ - Why Not?== https://ceur-ws.org/Vol-1193/paper_56.pdf
    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)