Typed Higher-Order Variant of SROIQ - Why Not?

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) involving 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 ]. Di erent applications are cited, roughly divisible into two categories: (i) modelling of certain complex domains, e.g., classifying taxonomic biological concepts such as GoldenEagle and Accipitriformes 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 entities themselves, such as deprecation of some concepts by assigning them into the Deprecated 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_instrument from Music Ontology (MO) [ 21 ]. Nigel Kennedy’s primary instrument is violin, 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) mo:Instrument

rdf:type mo-mit:Violin mo:primary_instrument ex:NigelKennedy mo: ex:Stradivarius_1707 primary_instrument (a) meta meta concepts

rdf:type comnceetapts mo:Release mo:album

rdf:type mo:release_type concepts mo:MusicalItem ex:EMI_49557

rdf:type frbr:exemplar_of individuals ex:my_CD_0007

mo:ReleaseType (b) 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 modelling 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 extension 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 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; Ii where I , ; and I is a function such that aI 2 I for all a 2 NI, AI I for all A 2 NC, and RI I I for all R 2 NR. Interpretation of complex concepts and roles is inductively defined as given in Table 1. An axiom ' is satisfied by I (denoted I j= ') if I satisfies the respective semantic constraint listed in Table 1, and I is a model of K (denoted I j= K ) if it satisfies all axioms of K . A concept C is satisfiable w.r.t. K if there is a model of K such that CI , ;. A formula ' is entailed by K (denoted K j= ') if I j= ' for all models I of K . The two reasoning tasks of concept satisfiability and concept subsumption entailment are inter-reducible [ 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 i 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 cardinality 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.

Typed Higher-Order SROI Q

Syntax

We introduce T H (SROIQ), the typed higher-order variant of SROIQ. For any sublanguage 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 di erent 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 Ut 0 NCt ] Ut>0;u>0 NRtu where for each 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 2 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, Stu, . . . belong to Ntu. Similarly for longer symR bols, e.g., NigelKennedy 2 NC0 , InstrumentType2 2 NC2 and primaryInstrument12 2 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 2 NRtu, v > 0, Stv is a tu-role expression and Qvu a vu-role expression respectively. We also define (Rtu ) = Rtu for any Rtu 2 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 2 NCt, At 1 2 NCt 1, Ct and Dt are t-descriptions, Cu 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, 8, 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 2 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, Ct and Dt are t-descriptions, Rtu and Stu 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 HiLogstyle interpretation of N is a triple I = ( I; I; E) such that 1. I = Ut 0 tI ] Ut;u>0 tIu is a disjoint union of countably many sets and 0I , ;, 2. At I 2 tI for each At 2 NCt and t 0, 3. Rtu I 2 tIu for each Rtu 2 NRtu and t; u > 0, 4. cE tI 1 for each c 2 tI and t > 0, 5. rE tI 1 uI 1 for each r 2 tIu and t; u > 0, and the interpretation of role expressions and complex descriptions is inductively defined according to, respectively, the upper and middle part of Table 2, where (and thenceforth), by abuse of notation, we redefine XE := (XI)E for atomic concepts and atomic roles, and XE := XE 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 j= ') under the conditions 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 j= ' for all ' 2 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 j= At = Bt), then so are their extensions (K j= At Bt). Extensionality, found in set theory, is the converse of intensional regularity (if K j= At Bt, then K j= At = Bt). We have come to conclusion that for metamodelling applications where higher-order names are intended to represent concepts, intensional regularity is a desirable property (see also Example 2 in Sect. 4.1), but extensionality may cause counterintuitive 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 (ALCH OIQ). 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 intension 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. Definition 7 (First-Order Reduction). Let K be a T H (SROIQ) KB using a vocabulary N = Ut 0fNCtg ] Ut;u>0fNRtug. The vocabulary is reduced into a DL vocabulary N1 = (NC; NR; NI) as follows: NC = ] NCt ]

]f>tg ; NR = ] NRtu ] finstanceOfg ; NI = NC0 ] t>0 t>0 t;u>0 ]fcAt j At 2 NCtg : t>0 The names >t, 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 N1, defined as follows: K 1 = Bound(K ) [ Typing(N) [ InstSync(N), where Typing(N) and InstSync(N) are 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, 9Utu: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 2 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 j= ' i K 1 j= Bound(').

The first-order reduction allows for decidability of T H (SROIQ) with the HiLogstyle semantics in the same complexity class as first-order SROIQ.

Corollary 1 Concept satisfiability and subsumption in T H (SROIQ) with HiLog satisfiability are decidable in 2-NExpTime.

Both proofs can be found in the extended version of the paper [ 10 ]. 4 4.1

Modelling in T H (SROI Q)

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 individuals 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 di erent 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 di erent 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 functionality on the primaryInstrumentType12 property:

Violin1 v Strings1

MusicArtist1 v 61primaryInstrumeSntrtTinygpse112v:>:2Percussions1

Drums1 v Percussions1

NigelKennedy: MusicArtist1 NigelKennedy; Violin1: primaryInstrumentType12

NigelKennedy; Drums1: primaryInstrumentType12

The KB above is consistent, but the concepts Violin1 and Drums1 are both unsatisfiable: Due to functionality of primaryInstrumentType12, they have the same intension. Thanks to intensional regularity (cf. Sect. 3.2), this implies they share the same extension, 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 su ce. 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 concepts, in a typical musical instrument classification, these concepts are further classified 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). Hornbostel and Sachs [ 11 ] classification sorts instruments into Idiophones, Membranophones, Chordophones, Aerophones and Electrophones (with many more subcategories). However, some modern instruments do not fit in any of these types. The modern classification [ 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 di erent classifications. To make some order in the vast number of categories, we will introduce concepts Classical Instrument Category, Hornbostel-Sachs Instrument Category, Modern Instrument Category, etc. (all of order 3). Some interesting ontological relations between these 3rd-order concepts 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 di erent 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., Supervisor 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 concept (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 manageable if used consistently in one ontology. However, in ontology integration and transformation, matching entities modelled at di erent levels of abstraction poses a problem. We have lately proposed so called PURO background modelling language [ 22 ] that enables 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 di erence, 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 di erent levels of abstraction, e.g., by asserting all particular violins on one side as instances of the violin concept on the other side. Materialization, as introduced by Pirotte at al. [ 20 ], is a relation between a more abstract 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 subclasses (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 higherorder 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 o ering features which can capture some of the constructs involved (such as two-faceted entities, and the possibility to assert the meta-relation materializesAs 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 materialization (modelling the di erent 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 ALCH OIQ and SH IQ, 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 o ers 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 di erence is that only second-order concepts are supported, and the approach is not characterized in model-theoretic terms. Punning OWL FA Motik ( -sem.) De Giacomo et al.

Glimm et al.

T H (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 extensionality it may be too strong for metamodelling [ 9 ]. Also, roles connecting di erent 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 distinctive 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 metameta-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 capturing 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 Handbook 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 logics . 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 Ethnologie 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 Musical 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 . Recommendation, 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 ubiquitous abstraction pattern . In: VLDB . pp. 630 - 641 . Morgan Kaufmann ( 1994 )

21. Raimond , Y. , Giasson , F . (eds.): Music Ontology Specification (28 November 2010 ), available 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 )