=Paper= {{Paper |id=None |storemode=property |title=Towards Typed Higher-Order Description Logics |pdfUrl=https://ceur-ws.org/Vol-1014/paper_88.pdf |volume=Vol-1014 |dblpUrl=https://dblp.org/rec/conf/dlog/HomolaKSV13 }} ==Towards Typed Higher-Order Description Logics== https://ceur-ws.org/Vol-1014/paper_88.pdf
     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