Towards Typed Higher-Order Description Logics Martin Homola1 , Ján Kl’uka1 , Vojtěch Svátek2 , and Miroslav Vacura2 1 Comenius University in Bratislava Mlynská dolina, 842 48 Bratislava, Slovakia {homola,kluka}@fmph.uniba.sk 2 University of Economics, Prague W. Churchill Sq. 4, 130 67 Prague 3, Czech Republic {svatek,vacuram}@vse.cz Abstract. We introduce a typed higher-order description logic specifically in- tended for reasoning about ontological coherence of domain models, motivated by a practical use case from linked data vocabularies. Keywords: Description logic, higher-order logic, theory of types, meta mod- elling. 1 Introduction The advent of the Semantic Web (SW) and especially the Linked Open Data initiative brought an unprecedented amount of new ontology vocabularies that are created, pub- lished, and daily instantiated in a number of data sets. At such large quantities, many of the vocabularies were created by developers not trained in ontology design, and were often influenced by the expressive and computational limitations of the SW languages, particularly OWL. Deeper ontological nature of the entities in the modelled domain may not have been considered or is not explicitly captured by these models. This often involves cases when classes are modelled as individuals, or some of the OWL classes in fact ontologically correspond to classes of a higher order. Consider an example taken from the Music Ontology (MO) [11]: Say we want to model information about a particular LP record in our collection – an exemplar of the famous CBS release of YoYo Ma’s 1983 performance of Bach’s Six Cello Suites. The modelling is depicted in Fig. 1. Our exemplar is represented by the individual ex:my_ LP_0047 (of the type mo:MusicalItem). The record is connected to its release ex:CBS_ 37867, i.e., the collection of all exemplars with the same recording, cover, bar code, etc., as our record. The type of this release is mo:album, which is an individual of the class mo:ReleaseType. The other data is for illustration only. From a strict ontological point of view we may realize that the release ex:CBS_37867 is, in fact, not a singular object per se, but rather it is a class – an entity having a set of instances (i.e., all its exemplars). Similarly, mo:album is a class of releases, but since the releases are them- selves classes, mo:album is a 2nd -order class. Finally, the class mo:ReleaseType is of the 3rd order, as it contains 2nd -order classes such as mo:album, mo:single, etc. So far, our example shows that some relevant ontological background is hidden from the MO vocabulary user, but everything is still coherent. However, one may, for ex:JSB_session_1983 mo:Release mo:interpreter mo:published_as rdf:type ex:YoYo_Ma ex:CBS_37867 mo:ReleaseType frbr:exemplar_of mo:release_type rdf:type ex:my_LP_0047 rdf:type mo:MusicalItem mo:album B-object B-type-1 B-type-2 B-type-3 Fig. 1. Music Ontology data about my_LP_0047 instance, create a new class ex:Wish_List and put into it some releases available from a regular reseller, alongside some particular second-hand exemplars of LPs and CDs from an auction web site. The class ex:Wish _ List thus becomes incoherent, as it contains entities of different ontological nature. Even further, MO provides the mo:primary _ instrument property to indicate the instrument of choice of an artist. It is intended to connect, e.g., ex:YoYo_Ma with mo-mit:Cello, where the latter is one of the predefined individuals corresponding to instrument types (i.e., in reality classes). Some user may however assign ex:Petunia (a particular cello) as Ma’s primary instrument, having this information in her data set. Especially if the data set is later integrated with some other we may get an ontologically incoherent result. However, the resulting OWL ontology would still be logically consistent, and a reasoner would not detect the incoherence. Recently, we have noted that making the ontological background explicit may help to address problems such as those described above [13,12]. We have proposed so called PURO models [13] which allow to mark background ontological distinctions (called the background model) in a given OWL vocabulary (called the foreground model) via an- notations. The background nature of classes, property domains and ranges is indicated by labeling them with background model notions such as B-type-1, B-type-2, etc. In addition, instance–type properties such as mo:release_type, are labeled as B-instan- tiations. The aim is to keep classes, property domains and ranges homogeneous (con- taining instances of the same ontological nature), and thus the ontology coherent. Such an approach is useful to both vocabulary designers, in order to keep track of the onto- logical background, as well as vocabulary users, in order to grasp the background and consistently use the vocabulary. We have also used the model to explain various pos- sible ontological intentions leading to the use of several ontology design patterns [12]. What still lacks here is the option to automatically verify the ontological coherence of the background model represented via the annotation labels. In this paper, we investigate the extension of description logics (DLs) up to SROIQ with typed higher-order concepts and roles, having in mind the particular application to ontological background coherence checking of OWL vocabularies. We aim to de- fine a DL allowing to directly formalize a background model in the PURO language, and to explore the possibilities for the semantics of this DL. Since PURO models fea- ture higher-order B-types, and relationships between B-types of different order, these models can most directly be formalized in a higher-order logic. Moreover, since homo- geneity of B-types is a requirement in PURO models, the proposed DL features typing. Our contribution is as follows: After brief preliminaries (Sect. 2), we introduce the syntax of typed higher-order DLs, and look for a suitable semantics, considering Henkin and HiLog-style semantics, and discussing their properties (Sect. 3). We then show de- cidability for a limited case of the proposed logic (Sect. 4). Finally, we discuss relevant related work and conclude (Sects. 5 and 6). 2 Preliminaries The SROIQ DL [6] forms the semantic basis of OWL 2 [8] and its sublanguages cover many popular DLs. A DL vocabulary Σ = NC ] NR ] NI is a set of symbols composed of three mutually disjoint countably infinite sets of atomic concepts (NC ), atomic roles (NR ), and individuals (NI ). Complex concepts (complex roles) are defined as the small- est sets containing all concepts and roles that can be inductively constructed using the concept (role) constructors3 in Table 1, where A is any atomic concept, C and D are any concepts, P and R are any atomic roles, S and Q are any (possibly complex) roles, a and b are any individuals, and n stands for any positive integer. A SROIQ knowledge base (KB) is a finite set K of axioms of multiple types as given at the bottom of Table 1. A DL interpretation is a pair I = h∆I , ·I i where ∆I , ∅ is the interpretation domain and ·I is an interpretation 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 and decidable for SROIQ [6]. However, further syntactic restrictions are required: the universal role cannot occur on the left-hand side of RIA axioms and in role assertions, only so called simple roles may appear in cardinality restrictions, and the role hierarchy needs to be regular. For the lack of space, we are not able to fully cover these restrictions here. The reader is kindly referred to the work of Horrocks et al. [6]. 3 Typed Higher-Order DL 3.1 Syntax Starting from a DL L up to SROIQ we build a typed higher order variant T H(L). The language is constructed over a typed vocabulary which explicitly distinguishes between entities of different types. 3 There are additional SROIQ constructors and axioms all of which (including equality) can be reduced to the core constructs listed in Table 1: > reduces to A t ¬A; ⊥ reduces to A u ¬A; C t D reduces to ¬(¬C u¬D); ∀R.C reduces to ¬∃R.¬C; 6nR.C reduces to ¬>n+1R.C; =nR.C reduces to >nR.Cu¬>n+1R.C; C ≡ D reduces to C v D and D v C, a = b reduces to {a} ≡ {b}, Sym(R) reduces to R− v R; Tra(R) reduces to R◦R v R; Irr(R) reduces to ∃R.Self v ⊥. Table 1. Syntax and Semantics of SROIQ Concept constructors Syntax Semantics atomic concept A AI complement ¬C ∆I \ C I intersection CuD C I ∩ DI existential restriction ∃R.C { x | ∃yhx, yi ∈ RI ∧ y ∈ C I } min. card. restriction >nR.C { x | ]{ y | hx, yi ∈ RI ∧ y ∈ C I } ≥ n } self restriction ∃R.Self { x | hx, xi ∈ RI } nominal {a} {aI } Role constructors Syntax Semantics atomic role R RI inverse role R− { hy, xi | hx, yi ∈ RI } universal role U ∆I × ∆I role chain S ·Q S I ◦ QI Axioms Syntax Semantics concept inclusion (GCI) CvD C I ⊆ DI role inclusion (RIA) S vR S I ⊆ RI reflexivity assertion Ref(R) RI is reflexive role disjointness Dis(P, R) PI ∩ RI = ∅ concept assertion a: C aI ∈ C I role assertion a, b : R haI , bI i ∈ RI negated role assertion a, b : ¬R haI , bI i < RI Definition 1 (Typed DL Vocabulary). A typed DL vocabulary is a disjoint union of a countable number of countable sets of the form ] ] NCt ] NRtu t≥0 t>0,u>0 where for each t ≥ 0, NCt is the set of concept names of type t, and for each t, u > 0, NRtu is the set of role names between types t and u. In addition, the set of individual names NI = NC0 is equal to the set of concept names of type 0. For clarity of presentation, we introduce the following notation: symbols of the from At , Bt , . . . belong to NCt , and specifically, symbols of the form A0 , B0 , . . . , a, b, . . . belong to NI . Symbols of the form R st , S st , . . . belong to NRst . Similarly for longer symbols, for example, InstrumentType2 ∈ NC2 and primaryInstrument12 ∈ NR12 . Complex concepts and roles are also respective to a particular type and may not be arbitrarily combined. Definition 2 (tu-role expression). Given a DL L with role constructors CR the set of tu-role expressions of T H(L) is recursively defined as the smallest set containing: 1. Rtu 2. Rut − if − ∈ CR 3. Utu if L allows the universal super-role U 4. S 1t1 u1 · S 2t2 u2 · · · · · S ntn un , if · ∈ CR , where t1 = t, un = u, ui = ti+1 for 1 ≤ i < n, and n > 1 is an integer where Rtu is an atomic role in NRtu , and S tu , S iti ui are tu- or ti ui -role expressions respec- tively, for t, u, ti , ui ≥ 0 and 1 ≤ i ≤ n. Definition 3 (t-description). Given a DL L with concept constructors CC the set of t-descriptions of T H(L) is recursively defined as the smallest set containing: 1. At 2. ¬C t if ¬ ∈ CC 3. C t  Dt if  ∈ CC ∩ {u, t} 4. Rtu .C u if  ∈ CC ∩ {∃, ∀} 5. nRtu .C u if  ∈ CC ∩ {6, >} 6. ∃Rtt .Self if Self ∈ CC 7. {At−1 } if {·} ∈ CC where At and At−1 are atomic concepts in NCt and NCt−1 respectively, C t , Dt are t- descriptions, C u is an u-description, Rtu is a tu-role expression, Rtt is a tt-role expres- sion, for t, u > 0. We further assume that >t = At t ¬At for t > 0 and some At ∈ NCt . Finally, T H(L) KBs are defined as follows. Definition 4. Given a DL L, a T H(L) knowledge base K is a finite set of axioms of the following forms: 1. C t v Dt if L allows concept inclusions, 2. Rtu v S tu if L allows role inclusions, 3. Tra(Rtu ), Ref(Rtu ), Irr(Rtu ), Sym(Rtu ), Dis(Rtu , S tu ), if L allows role transitivity, reflexivity, irreflexivity, symmetry, and disjointness, respectively, 4. At−1 : C t if L allows concept assertions, 5. At−1 , Bu−1 : Rtu if L allows role assertions, 6. At−1 , Bu−1 : ¬Rtu if L allows negative role assertions, where At−1 , Bu−1 are atomic concepts of NCt−1 and NCu−1 , respectively, C t , Dt are t- descriptions, Rtu , S tu are tu-role expressions, and t, u > 0. 3.2 Semantics We will now present two of the possible approaches to the semantics of T H(L). The most direct way of interpreting a typed higher-order logic is perhaps to adapt Henkin’s general models [5] of Church’s simple theory of types. Henkin’s semantics deals di- rectly with higher-order structures via a hierarchy of power sets. Let P(S ) = 2S denote the power set of a set S , let P0 (S ) = S , and let Pn+1 (S ) = P(Pn (S )). Definition 5 (Henkin Interpretation). Given a T H(L) KB K, a Henkin interpretation is a pair I = ({∆Is } s , ·I ) where 1. ∆I0 , ∅, ∆It+1 ⊆ P(∆It ), and ·I is an interpretation function that interprets the ele- ments of T H(L) as follows: (a) AtI ∈ ∆It for each At ∈ NCt , t ≥ 0, (b) RtuI ⊆ ∆It−1 × ∆Iu−1 for each Rtu ∈ NRtu , t, u > 0. 2. The domains ∆Is are closed under the interpretation of complex descriptions and role expressions in T H(L), which is inductively defined in the usual way (as in Table 1) with two exceptions for all t, u > 0: (a) (¬C t )I = ∆It−1 \ (C t )I , (b) (Utu )I = ∆It−1 × ∆Iu−1 . The advantage of Henkin interpretations is that the semantics of complex concepts is naturally defined as in any classical DL. For instance (∃R23 .C 3 )I = { x | ∃y.hx, yi ∈ R23I ∧ y ∈ C 3I }; this works in the usual way even if (∃R23 .C 3 )I ∈ P2 (∆I ), i.e., it is a set of sets of elements of ∆I . Similarly the notions of satisfaction, and model are analogous. Definition 6 (Henkin Satisfaction). Given a formula (axiom) φ in T H(L), a Henkin interpretation I = (∆I , ·I ) satisfies φ (denoted I |= φ) as follows: 1. I |= C t v Dt if C tI ⊆ DtI , 2. I |= Rtu v S tu if RtuI ⊆ S tuI , 3. I |= Tra(Rtu ) (Ref(Rtu ), Irr(Rtu ), Sym(Rtu )) if RtuI is a transitive (resp. reflexive, irreflexive, symmetric) relation, 4. I |= Dis(Rtu , S tu ) if RtuI and S tuI are disjoint, 5. I |= At−1 : C t if At−1I ∈ C tI , 6. I |= At−1 , Bu−1 : Rtu , if hAt−1I , Bu−1I i ∈ RtuI , 7. I |= At−1 , Bu−1 : ¬Rtu if hAt−1I , Bu−1I i < RtuI . Definition 7 (Henkin Model). A Henkin interpretation I = (∆I , ·I ) is a model of a T H(L) KB K if I |= φ for all φ ∈ K. The straightforward interpretation of higher-order classes as sets of sets in Henkin semantics leads to properties that are not intuitive in knowledge representation, as dis- cussed below in Sect. 3.3. We therefore consider also HiLog-style semantics which was successfully applied in higher-order logic programming [1] and DL as well [7,2] (note that in [2], this semantics is, quite confusingly, introduced as “a Henkin semantics”). HiLog-style interpretations first assign each name an element of a single domain, thus effectively assigning it an intension (for which we will use the function ·I ). The in- tension is then assigned both a class extension (subset of the domain ∆I ) and a role extension (subset of ∆I × ∆I ). In order to obtain a typed version of this semantics, we partition the domain into disjoint slices, each dedicated to intensions of members of one type (either a class type t, or a role type tu). An extension is then possibly assigned to the intentions (using the function ·E ) as appropriate, e.g., an intension cannot be assigned a class extension and a role extension simultaneously. In HiLog [1] and some of its DL applications (e.g., the higher-order DL of De Giacomo et al. [2]), also complex expressions (roles, concepts) are required to have intensions. However, in our application (ontological coherence checking of OWL vo- cabularies), we do not expect the need to express higher-order assertions over complex concepts and roles. Therefore, we directly derive extensions of such complex entities without requiring them to have any intension. In this sense, our approach is similar to the one of Motik [7] which will allow us, at least in a limited case, to show decidability of the HiLog-style semantics by reduction to Motik’s one in Sect. 4. Table 2. HiLog-style interpretation constraints X XE X XE ¬C t ∆It−1 \ C t E ∃S tt .Self { x | hx, xi ∈ S tt E } C t u Dt C t E ∩ Dt E {C t−1 } {C t−1I } ∃Rtu .C u { x | ∃y.hx, yi ∈ Rtu E ∧ y ∈ C u E } Rtu − { hy, xi | hx, yi ∈ R st E } >nS tu .C u { x | ]{ y | hx, yi ∈ S tu E , y ∈ C u E } ≥ n } R1t1 u1 · · · · ·Rntn un R1t1 u1 E ◦ · · · ◦ Rntn un E Definition 8 (HiLog-Style Interpretation). Given a T H(K) KB K, a HiLog-style interpretation 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 s.t. ∆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 complex descriptions and role expressions is inductively de- fined according to Table 2, where, by abuse of notation, we redefine X E := (X I )E for atomic concepts and roles and X E := X E for non-atomic ones. As remarked by Chen et al. [1], this way we obtain an essentially first-order seman- tics (free of higher-order power sets) for a higher-order language. On the other hand, we have to be careful to properly use the two interpretation in the definition of satisfaction. Definition 9 (HiLog-Style Satisfaction). Given a formula (axiom) φ in T H(L), a HiLog-style interpretation I = (∆I , ·I , ·E ) satisfies φ (denoted I |= φ) as follows: 1. I |= C t v Dt if C t E ⊆ Dt E , 2. I |= Rtu v S tu if Rtu E ⊆ S tu E , 3. I |= Ref(Rtu ) if Rtu E is a reflexive relation, 4. I |= Dis(Rtu , S tu ) if Rtu E and S tu E are disjoint, 5. I |= At−1 : C t if At−1 I ∈ C t E , 6. I |= At−1 , Bu−1 : Rtu if hAt−1 I , Bu−1 I i ∈ Rtu E , 7. I |= At−1 , Bu−1 : ¬Rtu if hAt−1 I , Bu−1 I i < Rtu E . Definition 10 (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. 3.3 Properties We will now compare the HiLog-style semantics and Henkin semantics, in order to see in which respects they differ, and how suitable each of them is for our use case. Obviously, Henkin semantics assigns each concept a single semantic object, while the HiLog-style semantics assigns a concept (in our case, only atomic concepts) two separate semantic objects: the concept’s intension and extension. We may then ask the following question: If the intensions of a concept are equal, are the extensions equal as well, and vice versa? This question is formalized as the properties of intensional regularity (1) and extensionality (2): K |= At = Bt =⇒ K |= At ≡ Bt , (1) K |= A ≡ B =⇒ K |= A = B . t t t t (2) Intensional regularity is typically a desired property. It also fits our use case, as illustrated in the following example originally studied by Motik [7]: Example 1. Consider the knowledge base K = {Aquila1 = Eagle1 , Harry0 : Eagle1 , Harry0 : ¬Aquila1 }. Given that Aquila1 and Eagle1 are just two different names for the same class, which are made equal on the intensional level (i.e., they are the names of the same concept in different languages), it is natural to expect that if we put same object into Eagle1 and ¬Aquila1 , the KB becomes inconsistent. Both Henkin and the HiLog-style semantics are intensionally regular, and so K is inconsistent in both of them. In the case of Henkin semantics, we ought to realize that the axioms Aquila1 = Eagle1 and Aquila1 ≡ Eagle1 have exactly the same mean- ing, as there is just one denotation ·I for each entity which serves both as its inten- sion and extension at the same time. In the case of the HiLog-style semantics, inten- sions (Aquila1 )I and (Eagle1 )I are both equal to the same element d of ∆I , and hence (Aquila1I )E = dE = (Eagle1I )E . When it comes to extensionality, in most use cases it is undesired. For instance, in meta modelling we want to express versioning meta information within logic, as illustrated in the following example. In OWL, such information can only be expressed using annotation properties. Example 2. Consider a KB K = {Aquila1 ≡ Eagle1 , Eagle1 : Deprecated2 } in which we have two extensionally equivalent classes Aquila1 and Eagle1 and the latter is marked as deprecated. Now deriving K |= Aquila1 : Deprecated2 which is a direct consequence of extensionality is apparently undesired. While Henkin semantics is inherently extensional for the same reason which makes it intensionally regular (i.e., a single denotation), HiLog-style semantics is not exten- sional. Indeed, it is possible in a HiLog-style model of K that Aquila1I = a and Eagle1I = e, a , e, but aE = eE , together with e ∈ (Deprecated2I )E and a < (Deprecated2I )E . Interestingly enough, extensionality can be regained by a minor modification to the HiLog-style semantics, as shown in the following proposition proved in Appendix A. Proposition 1. A modified HiLog-style semantics which requires ·E to be injective has the extensionality property. Extensionality may be seen as desired in some use cases, e.g., in tight vocabulary in- tegration scenarios we might want to unify classes completely by asserting their equiv- alence. This is however outside of the scope of our use case. Finally, we would like to remark that by choosing not to include intensions for complex entities, we made the HiLog-style semantics weaker compared to Henkin se- mantics. Consider the following example: Example 3. Let us have K = {Eagle1 ≡ {Harry0 }, Aquila1 ≡ {Mary0 }, Harry0 , Marry0 , >2 v {Eagle1 , Aquila1 }} in which for whatever reason we decided to limit the number of type-1 classes to two. While this KB has a HiLog-style model, it has no Henkin model. Henkin semantics requires that each, even non-atomic, description has an interpretation present in the domain. Note that there are only two objects of type 2 available in K, since we have ∆I1 = (>2I ) = {E, A}, E = Eagle1I = {Harry0I } = {h} and A = Aquila1I = {Marry0I } = {m}, E , A, h , m. The Henkin interpretation (Eagle1 t Aquila1 )I is equal to a {h, m}, which is different from both E and A, and so it does not fit in ∆I1 . This may at first sound as a drawback of the HiLog-style semantics, but in our use case it is not. Since we do not really want to assert higher-order statements over complex concepts or roles, we do not want to care about their intensions. Note that since there is a countable infinite number of complex concept expressions, there can also be an infinite number of intensions. This further adds to the complexity of the semantics, which is not necessary. In the version of HiLog-style semantics used in this paper, we may understand nominals as operating on entities which have explicit identity (intension). If we wish to create an intension for a complex concept, we can always do it by introducing a new atomic name for it, and an equivalence axiom. 4 Decidability We will now demonstrate decidability of decision problems in T H(ALCHOIQ) by reduction to the untyped ALCHOIQ with meta modelling under the HiLog semantics (also called ν-semantics) as defined and proved decidable by Motik [7]. Definition 11 (ALCHOI Q with Meta Modelling [7]). For a set Na of atomic names, define the set of names as N = Na ∪ {n− | n ∈ Na }. For each n ∈ Na , let Inv(n) = n− , and Inv(n− ) = n. The set of ALCHOIQ concepts is the smallest set containing each A ∈ N, and for each R, i ∈ N, non-negative integer n, and ALCHOIQ concepts C and D, also the concepts {i}, ¬C, C u D, ∃R.C, and >nR.C. An ALCHOIQ knowledge base with meta modelling is a finite set consisting of role inclusion axioms R vR S for any R, S ∈ N, concept inclusion axioms C vR D for any concepts C and D, and assertions of the forms a : C and a, b : R where C is a concept and a, b, R ∈ N. Definition 12 (ν-Semantics [7]). Let K be a ALCHOIQ KB with meta modelling. A ν-interpretation of K is a quadruple I = (∆I , ·I , CI , RI ) where ∆I is a non-empty domain, ·I : N → ∆I is a name interpretation function, CI : ∆I → P(∆I ) is an atomic concept extension function, and RI : ∆I → P(∆I × ∆I ) is a role extension function satisfying RI (S I ) = RI ((Inv(S ))I )− . The atomic concept extension function is extended to ALCHOIQ concepts as shown in Table 3 left. Table 3 right defines the ν-satisfaction relation. The notions of ν-satisfiability and ν-model of K are defined as usual. Theorem 1 ([7]). ν-satisfiability of a KB K in the DL ALCHOIQ with meta mod- elling is decidable in non-deterministic exponential time. The following reduction allows application of Motik’s results to T H(ALCHOIQ). Table 3. The ν-semantics [7] X CI (X) φ I |=ν φ A C I (AI ) S vR T RI (S I ) ⊆ RI (T I ) {i} {iI } D1 v D2 C I (D1 ) ⊆ C I (D2 ) ¬D ∆I \ C I (D) a: D aI ∈ CI (D) D1 u D2 C I (D1 ) ∩ C I (D2 ) a, b : S haI , bI i ∈ RI (S I ) ∃S .D { x | ∃y.hx, yi ∈ RI (S ) ∧ y ∈ CI (D) } >nS .D { x | ]{ y | hx, yi ∈ RI (S ) ∧ y ∈ CI (D) } ≥ n } Definition 13 (Untyped Reduction). Let K be a T H(L) knowledge base in a vocab- ulary Σ = t≥0 NCt ] t,u>0 NRtu . Let Na = Σ ] {>t | t > 0} ] {>tu | t, u > 0}, where >t U U and >tu for each t, u > 0 are mutually distinct fresh names. The untyped reduction Υ(K) of K is a KB in the DL L with meta modelling over the set of atomic names Na defined as Υ(K) = TB(K) ∪ TC(K), where the type-bound version TB(K) of K is obtained by replacing each occurrence of a t-description of the form ¬C t in K by >t u ¬C t , and the set of typing constraints TC(K) consist of the following axioms (m is the maximum type number occurring in K): 1. for each t, u, v, w, such that 0 < t, u, v, w ≤ m+1, >t v ¬>u if t , u, >tu v ¬>vw if (t, u) , (v, w), and >tu v ¬>v ; 2. A : > for each A occurring in K, 0 < t ≤ m+1; t−1 t t−1 3. Rtu : >tu for each Rtu occurring in K, 0 < t, u ≤ m; 4. At v >t for each At occurring in K, 0 < t ≤ m; 5. ∃Rtu .> v >t and > v ∀Rtu .>u for each Rtu occurring in K, 0 < t, u ≤ m. Proposition 2. Let K be a T H(L) KB. Then K is satisfiable in the HiLog semantics iff Υ(K) is ν-satisfiable. Proposition 2 is proved in Appendix A. Since Υ(K) can be constructed from K in polynomial time, Theorem 1 and Proposition 2 imply the following corollary. Corollary 1. Satisfiability in T H(ALCHOIQ) in the HiLog semantics is decidable in non-deterministic exponential time. 5 Related Work Considering typed higher order languages for SW vocabularies, our approach relates to the work of Pan and Horrocks [9] who introduced a typed higher-order variant of RDFS, dubbed RDFS(FA). RDFS itself is a higher-order language, however it lacks distinguished types. While RDFS itself employs a HiLog-style semantics, RDFS(FA) resorts to a variant of standard higher-order semantics, a less-general instance of Henkin semantics (see Henkin [5] for detailed comparison). We argued in Sect. 3, that HiLog- style semantics is more appropriate in our use case. Both Motik [7] and De Giacomo et al. [2] have investigated higher-order extensions of DL under HiLog-style semantics which are not typed. De Giacomo et al. have stud- ied a stronger variant of the semantics where intensions are assigned also to complex entities. Example 3 can be used to show that these semantics differ, the latter one being the stronger. Our work can be seen as an extension of these two approaches, introduc- ing the types. In Sect. 4, we were able to show the relation with Motik’s semantics by reduction. As noted above, we have intentionally chosen a weaker semantics, similar to the Motik’s one as it is sufficient for our use case. In our previous work [13], we sketched how coherence checking w.r.t. the PURO model can be done using a meta modelling approach. The current work is an improve- ment, as it allows to reason in both the original vocabulary and the (PURO) meta level at the same time. In this light, we would like to point out the work of Glimm et al. [4], where meta level reasoning (with the OntoClean meta model) is integrated with the original vocabulary via a direct translation into OWL. In the future, we would like to investigate a similar direction in order to obtain effective reasoning support also for more expressive fragments of T H(SROIQ). Punning is a new feature of OWL 2 [8] allowing the same name to be used in different contexts, e.g., once as a class and then as in individual. As already noted by Motik [7] who investigated a similar approach under the name contextual semantics, it does not satisfy intensional regularity, which we identified as an important property in Sect. 3.3. Finally, it should also be remarked that scenarios similar to the one outlined in the introduction could also be modelled with more advanced techniques, such as the materialization relationship [10], or in DL extensions such as a theory of collections [3]. However, such approaches rely on notions which are unfamiliar to many linked data (LD) vocabulary developers, while in our proposal we tried to keep a high level of similarity with the LD terminology (e.g., we still deal with objects, types, instantiation, and relationships even if some of them may be of higher orders). 6 Conclusions The recently introduced PURO model [13] intended for ontological coherence checking of OWL vocabularies requires consideration of higher-order entities in the vocabularies. With the aim to enable automated reasoning support for the coherence checking task, we have investigated a typed higher-order extension of SROIQ, dubbed T H(SROIQ). In search for a suitable semantics, we have considered a Henkin [5] and a HiLog [1] in- spired approach. As a conclusion, we find the latter one more favourable as it is simpler but sufficient to support our use case. Compared to the Henkin semantics it is not exten- sional, and, as discussed, extensionality may be undesired in meta modelling scenarios such as ours. Finally, we were able to show that for a limited case of T H(ALCHOIQ) the HiLog-style semantics is decidable. Acknowledgements. This work was supported from the EU ICT FP7 under no. 257943 (LOD2 project), from the Slovak VEGA project no. 1/1333/12, and from the Czecho- Slovak bilateral project nos. 7AMB12SK020 (AIP) and SK-CZ-0208-11 (APVV). 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. De Giacomo, G., Lenzerini, M., Rosati, R.: On higher-order description logics. In: DL (2009) 3. Franconi, E.: A treatment of plurals and plural quantifications based on a theory of collec- tions. Minds and Machines 4(3), 453–474 (1993) 4. Glimm, B., Rudolph, S., Völker, J.: Integrated metamodeling and diagnosis in OWL 2. In: ISWC (2010) 5. Henkin, L.: Completeness in the theory of types. J. Symbolic Logic 15, 81–91 (1950) 6. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: KR (2006) 7. Motik, B.: On the properties of metamodeling in OWL. J. Log. Comput 17(4), 617–637 (2007) 8. OWL Working Group (ed.): OWL 2 Web Ontology Language Document Overview. Recom- mendation, W3C (2009) 9. Pan, J.Z., Horrocks, I.: RDFS(FA): Connecting RDF(S) and OWL DL. IEEE Trans. Knowl. Data Eng. 19, 192–206 (2007) 10. 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) 11. Raimond, Y., Giasson, F. (eds.): Music Ontology Specification (28 Nov 2010), available online: http://purl.org/ontology/mo/ 12. Svátek, V., Homola, M., Kl’uka, J., Vacura, M.: Mapping structural design patterns in OWL to ontological background models. In: K-CAP (2013) 13. Svátek, V., Homola, M., Kl’uka, J., Vacura, M.: Metamodeling-based coherence checking of OWL vocabulary background models. In: OWLED (2013) A Proofs Proof (Proposition 1, sketch). The proposition is proven by an obvious repetition of the reasoning under Example 2, where we realize that the injectivity of ·E assures no two distinct intensions can be assigned the same extension. Hence, if extensions of two classes are equal, the same must hold for their intensions. t u Proof (Proposition 2). Denote the smallest typed DL vocabulary of K by Σ = t≥0 NCt ] U U st s>0,t>0 NR . (⇐) Assume Υ(K) is ν-satisfiable and take its ν-model J = (∆J , ·J , CJ , RJ ). We define a HiLog interpretation I of K as follows: Let ∆It−1 := CJ (>tJ ) for each t > 0, and ∆Itu := CJ (>tuJ ) for each t, u > 0. Observe that ∆I := t≥0 ∆It ] t,u>0 ∆Itu is indeed U U a disjoint union, which is ensured by the typing constraints 1 of TC(K). Let ·I := ·J |Σ (the restriction of ·J to Σ), and observe that the typing constraints 2 and 3 imply the conditions 2 and 3 of Def. 8. Now let ∆IC = t>0 ∆It and ∆IR = t,u>0 ∆Itu . Since ∆IC S S and ∆IR are disjoint, the union ·E := CJ |∆I ∪ RJ |∆I is a function from ∆IC ] ∆IR . Typing C R constraints 4 and 5 ensure that ·E satisfies the conditions 4 and 5 of Def. 8. Observe that RtuE = RJ (Rtu ) for all tu-role expressions. Now we can easily verify by induction on the construction of t-descriptions, that C tE = CJ (TB(C t )). For atomic descriptions, this follows from the typing constrains. For complex descriptions, the only interesting case is the one when C t is of the form ¬Dt , and we have C tE = ∆It−1 \ DtE = ∆It−1 \ CJ (DtJ ) = CJ (>tJ ) ∩ (∆J \ CJ (DtJ )) = CJ (>t u ¬Dt ) = CJ (TB(C t )), where the second equality holds by the induction hypothesis. In conclusion, we have AtI = AtJ for all concept names At ∈ NCt , t ≥ 0, RtuE = R (Rtu ) for all tu-role expressions Rtu over Σ, and C tE = CJ (TB(C t )) for all t-descrip- J tions C t over Σ, t, u > 0. These properties allow us to straightforwardly verify that for any axiom φ ∈ K we have I |= φ iff J |= TB(φ), which implies satisfiability of K. (⇒) Assume K has a HiLog model I = (∆I , ·I , ·E ). We construct a ν-model J of Υ(K) as follows: Let ∆> = {δt | t > 0}]{δtu | t, u > 0}, where δt and δtu are any mutually distinct objects not occurring in ∆I . We define the domain of J as ∆J := ∆I ] ∆> , and its name interpretation function as N J := N I for each concept or role name N ∈ Σ, >tJ := δt for each t > 0, and >tuJ := δtu for each t, u > 0. Let ∆IC = t>0 ∆It and S ∆IR = t,u>0 ∆Itu . We define the atomic concept extension function as CJ (c) := cE for S each c ∈ ∆IC , as CJ (δt ) := ∆It−1 for each t > 0, as CJ (δtu ) := ∆Itu for each t, u > 0, and as CJ (x) = ∅ for each x ∈ ∆I \ (∆IC ∪ ∆> ). The role extension function is defined as RJ (r) := rE for each r ∈ ∆IR , and as RJ (x) = ∅ for each x ∈ ∆I \ ∆IR . With the construction of J completed, we can now show similarly as above that we have AtJ = AtI for all concept names At ∈ NCt , t ≥ 0, RJ (Rtu ) = RtuE for all tu-role expressions Rtu over Σ, and CJ (TB(C t )) = C tE for all t-descriptions C t over Σ, t, u > 0. These properties allow us to straightforwardly verify that for any axiom φ ∈ K we have I |= φ iff J |= TB(φ), which implies ν-satisfiability of Υ(K). t u