Meta-Modeling Extension of Horn-SROIQ and Query Answering

Abstract

We investigate reasoning and query answering in expressive domain knowledge bases (KBs) that are in OWL 2 Full and contain large individual data sets. For this, we introduce Hi(Horn-SROIQ) and meta-queries based on HiLog semantics. Hi(Horn-SROIQ) is extended from Horn-SROIQ, the horn fragment of the most expressive description logic (DL) for OWL 2 with well known low data complexity, by allowing classes and roles to be used as individuals. Accordingly, meta-queries are obtained from conjunctive queries by allowing variables to appear in the class and role positions. For reasoning, we rst provide a method of reducing satis ability checking and conjunctive query answering in Hi(Horn-SROIQ) to the corresponding reasoning tasks in Horn-SROIQ soundly and completely, then we show that meta-query answering in Hi(Horn-SROIQ) can be captured by conjunctive query answering. Based on this, we obtain that adding meta-modeling capability to Hi(HornSROIQ) has no impact on the complexity of the considered reasoning tasks. These results make Hi(Horn-SROIQ) appealing for practical usage.

-

With the successful application of the Semantic Web technologies, more and more domain KBs have been developed over the past decades for reusing and sharing. Most of them are in OWL 2 DL so that e cient and mature DL Reasoners, such as HermiT [ 8 ], Pellet [33] and RacerPro [ 10 ], can take e ect to facilitate reasoning and query answering. However, caused by meta-modeling, there exist certain complex KBs that fall into OWL 2 Full. This can be exempli ed by the Foundational Model of Anatomy (FMA) [27], common sense KB OpenCyc [ 23 ] and Suggested Upper Merged Ontology (SUMO) [31]. All of these widely used KBs not only contain large-scale individual data but also most classes and roles are also used as individuals at the same time. OWL 2 Full is undecidable. Compared with OWL 2 DL, reasoning in OWL 2 Full has largely been unexplored. Up to now, no Reasoner has been especially developed for it. Thus, e ciently reasoning and query answering in such KBs raise new challenges.

For meta-modeling, OWL 2 DL provides a technique called punning by syntactically allowing names to have multiple uses while semantically treating the di erent uses of the same name as completely separate [ 9 ]. Such way of processing meta-modeling dooms to no new entailments can be obtained. Moreover, in order to reuse the techniques as well as systems for DLs, [3,7,11,13,21,24{26,30] investigate adding meta-modeling capability to decidable DLs by allowing one name to act as multiple roles in various ways. The referred DLs contain SHOIQ [ 15 ], SHIQ [ 16 ], SROIQ [ 14 ], and ALCQ [ 5 ]. For these works, excepting high reasoning complexity, query answering which plays an important role in Semantic Web for realizing knowledge sharing and reusing has rarely been discussed, nor the ability of handing scalability. Extension of tractable language DL-LiteR is discussed in [ 3 ] and [ 22 ]. Although having low reasoning complexity, the expressivity is every restricted.

On the other hand, in DL based knowledge representation systems, individual assertions describe the concrete world and usually account for a large proportion of domain KBs, such as, 94.6% in FMA and 78.5% in OpenCyc. As more and more applications require scalability in terms of individual assertions, Horn-DLs [1, 4, 18{20, 29] have been introduced and attract more and more attention, since they promise to make a suitable trade-o between scalability and expressivity. In [28] and [29], Ortiz has shown that data complexities (measured in the size of individual assertions) of satis ability checking and conjunctive query answering in Horn-SROIQ, the horn fragment of the most expressive DL for OWL 2, are PTime and PTime-complete. Lower data complexity makes Horn DLs a natural and e cient choice for reasoning with large number of individuals. Moreover, [ 20 ] has pointed out that many OWL 2 ontologies are Horn. When omitting metamodeling, many actual OWL 2 Full ontologies, such as OpenCyc, SUMO and Yago, fall into Horn-SROIQ.

For reasoning and query answering in OWL 2 Full ontologies containing large number of individuals, attracted by the low data complexity as well as suitable expressivity of Horn-SROIQ, in this paper, we discuss extending Horn-SROIQ with meta-modeling capability. Our contributions can be summarized as follows: (1) We formalize Hi(Horn-SROIQ) and meta-queries based on HiLog semantics. Hi(Horn-SROIQ) is de ned by unifying the sets of names for classes, roles and individuals. Accordingly, meta-queries are de ned by allowing variables to appear in the class and role positions of conjunctive queries. (2) We provide a way of reducing satis ability checking and conjunctive query answering in a Hi(Horn-SROIQ) KB to the corresponding reasoning tasks in a Horn-SROIQ KB with size no more than the original KB soundly and completely. (3) We show that meta-query answering in Hi(Horn-SROIQ) can be reduced to conjunctive query answering through materializing the variables appearing in the class and role positions soundly and completely. (4) We show that satis ability checking and meta-query answering in Hi(HornSROIQ) still have PTime and PTime-complete data complexities, respectively. From the practical point of view, our work has the following two advantages. Firstly, by allowing all the names to have di erent uses without any restriction, Hi(Horn-SROIQ) has the exibility to capture meta-modeling in the actual KBs. And secondly, by reasoning reduction, the systems tailored for DLs or Horn Logic can be used to realize reasoning with Hi(Horn-SROIQ).

Hi(Horn-SROIQ) and meta-query

In this section, we formalize the syntax and semantics of Hi(Horn-SROIQ) and meta-queries. And we start with de ning Hi(Horn-SROIQ) based on HornSROIQ [ 20, 29 ]

B, C and D are inductively de ned as follows: r1 R R vr R r2 Inv(R) vr R r3 ! vr R r4 ! R vr R r5 R ! vr R r6 Disj(S; S0) r7 C vc D r8 B(a); R(a; b); a b; a 6 b

B ::= Ajfagj9S:Self C ::= Bj9R:CjC t CjC u C D ::= Bj:Bj9R:Dj mS:Dj jD u D 1S:D Hi(Horn-SROIQ). Let N be a countably in nite set of names such that f>; ?g N . For each P 2 N , P and P are roles, and their respective inverses are Inv(P ) = P and Inv(P ) = P . A role hierarchy Rh is a set of role inclusion axioms which take the form R1 Rn vr R where R1, , Rn and R are roles. Rh is called regular, if there exists an irre exive and transitive binary relation on the set N [ fP jP 2 N g of roles such that S R i Inv(S) R for all roles S and R, and all the role inclusion axioms in Rh have the forms r1 r5 in gure 1.

Given a role hierarchy Rh, the set of roles that are non-simple in Rh is inductively de ned as follows: (1) R is non-simple if Rh contains a RIA R1

Rn vr R such that n > 1, or n = 1 and R1 is non-simple; (2) an inverse role Inv(R) is non-simple if R is. A role R is simple in Rh if it is not non-simple in Rh. Given Rh, a role disjoint axiom and a class inclusion axiom take the form r6 and form r7 in gure 1, respectively, and an individual assertion has one of the forms in r8 in gure 1.

A Hi(Horn-SROIQ) KB K is a tuple (Rh [ Rd [ C; A) where Rh is a regular role hierarchy, Rd, C and A are nite sets of role disjoint axioms, class inclusion axioms, and individual assertions, respectively. And we use jKj, jRh [ Rd [ Cj, jAj to denote the size of K, Rh [ Rd [ C and A, respectively.

Hi(Horn-SROIQ) does not separate names for classes, roles and individuals. Thus, symbols vc and vr are used to distinguish between class inclusion axioms and role inclusion axioms. Moreover, for simpli cation, we use a =l b as an abbreviation of the two axioms a vl b and b vl a, where l 2 fc; rg. The following example illustrates a simple Hi(Horn-SROIQ) KB which models some knowledge about football described in OpenCyc.

Example 1. Let K be a Hi(Horn-SROIQ) KB consisting of the following axioms ((a), (b) and (c)) and individual assertions ((d ), (e), and (f )):

SportsTeam vc :AllStarTeam (a) Football team vc SportsTeam (b) > vc 1rewriteOf:>u 9rewriteOf:Self (c) rewriteOf(FootballTeam; Football team) (d) SportsTeamTypeBySport(Football team) (e)

FootballTeam(BarcelonaDragons) (f ) In this Hi(Horn-SROIQ) KB, names FootballTeam and Football team have multiple uses, i.e, as classes and individuals.

The semantics of Hi(Horn-SROIQ) is captured by v-interpretation [26] which is based on HiLog [ 2 ] and takes a similar way of OWL 2 RDF-Based Semantics [32] to interpret the multiple uses of names in a KB.

Syntax

Semantics P RV (P V ) P f(y; x)j(x; y) 2 RV (P V )g A CV (AV ) fag faV g 9S:Self fxj(x; x) 2 RV (R)g :B V CV (B) C u D CV (C) \ CV (D) C t D CV (C) [ CV (D) 9R:C fxj9y:(x; y) 2 RV (R)^y 2 CV (C)g 8R:C fxj8y:(x; y) 2 RV (R) ! y 2 CV (C)g 1S:D fxj#fyj(x; y) 2 RV (S)^y 2 CV (D)g 1g mS:D fxj#fyj(x; y) 2 RV (S)^y 2 CV (D)g mg B vc C CV (B) CV (C) ! vr R RV (R1) RV (Rn) RV (R) Disj(S; R) RV (S) \ RV (R) = ; B(a) a 2 CV (B) R(a; b) (aV ; bV ) 2 RV (R) a b aV = bV a 6 b aV 6= bV v-semantics. A v-interpretation V = ( V ; V ; CV ; RV ) is a tuple where V is a non-empty domain set, V , CV and RV are functions satisfying: (a) V maps each name in N to an element in V ; (b) CV maps each element in V to a subset of V such that CV (>V ) = V and CV (?V ) = ;; (c) RV maps each element in

V to a subset of V V . The interpretation of class and role constructors as well as axioms and assertions are speci ed in gure 2. We say V is a v-model of a Hi(Horn-SROIQ) KB K if V satis es each axiom and assertion in K. We say K is v-satis able i it has a v-model. Moreover, the v-entailment (j=v) is de ned as usual.

In a v-interpretation, the class and role extensions of names are obtained from the domain elements they mapped into. This indicates that under v-semantics, a Hi(Horn-SROIQ) KB may imply that a non-simple role and a simple role are equivalent. Such equivalences between roles may cause (a) transitive roles (R R vr R) are used in number restrictions ( 1R:D and mS:D) or (b) role hierarchies contain cyclic dependencies. (a) and (b) are well known factors that lead to undecidability [ 16, 17 ]. Consider the following axioms and assertion: P5 P4 vr P4; P3 P4 vr P3; P3 P2 vr P2; P1 P2 vr P1 (1)

P1 P1 vr P1; > vc 5P5:> (2)

P5 P1 (3) Under v-semantics, the assertion in (3) implies the axiom P1 =r P5. Such equivalence between non-simple role P1 and simple role P5 leads to the fact that transitive role P1 is used in the number restriction in (2) and the roles in (1) contain cyclic dependencies. For decidability, motivated by [26], we assume Hi(HornSROIQ) adopts unique non-simple role assumption (UNRA), i.e., for each Hi(Horn-SROIQ) KB K and each two di erent names a and b in K, if a or b is a non-simple role in K then we assume K contains the assertion a 6 b. Meta-queries. Let V be a set of variables such that V \ N = ;. A query atom has the form x(y), x(y; z) or x y where x; y; z 2 N [ V. A meta-query Q is an expression of the form: 1 ^

^ n ! q(x ) where 1; ; n are query atoms and x called the head of Q is a tuple of elements in N [ V such that each variable in x appears in some i. Variable x is called a class (role) variable of Q if Q contains an atom x(y) (x(y; z)). Without class and role variables, Q is a conjunctive query.

For a tuple x, we use jxj to denote the length of x and use x[i] to denote the i-th element of x for 1 i jxj. For another tuple a such that jaj = jxj, we use [x=a] to denote a substitution. And for an object O (a KB, query or tuple), we use O[x=a] to denote the result of replacing each appearance of x[i] in O with a[i] for each 1 i jxj.

Meta-query answering. For v-interpretation V and meta-query Q, a binding of Q over V is a function that maps each variable in Q to an element in V and each name a in Q to aV . The satisfaction of query atoms is de ned as follows: V; j=v x(y) if (y) 2 CV ( (x)) V; j=v x(y; z) if ( (y); (z)) 2 RV ( (x))

V; j=v x y if (x) = (y) We write V; j=v Q if V and satisfy all the query atoms in Q. We write V j=v Q if there exists a binding of Q over V such that V; j=v Q. Let x be the head of Q. For Hi(Horn-SROIQ) KB K, a tuple u of names appearing in K, such that juj = jxj and if jxj 1, u[i] = x[i] for each 1 i jxj with x[i] 2 N , is called a certain answer of Q over K if V j=v Q[x=u] for each v-model V of K. We use ansv(Q; K) to denote the set of all the certain answers of Q over K.

In a meta-query, the variables that do not appear in the head of this query are treated as existential variables. This is the main di erence between meta-queries and SPARQL OWL 2 RDF-Based Semantics Entailment Regime [ 6 ] where all the variables in a query are treated as free variables. Such di erence indicates that under v-semantics, more certain answers can be obtained. For the reasoning tasks of Hi(Horn-SROIQ), we just consider v-satis ability checking and metaquery answering, since the other reasoning problems, such as individual checking, can be reduced to v-satis ability checking. 3

Reasoning with Hi(Horn-SROIQ)

In this section, we study reasoning in Hi(Horn-SROIQ). For this, we rst present a way of reducing v-satis ability checking and conjunctive query answering in Hi(Horn-SROIQ) to the corresponding reasoning tasks in Horn-SROIQ soundly and completely, then we show that meta-query answering in Hi(Horn-SROIQ) can be captured by conjunctive query answering. 3.1

v-satis ability checking and conjunctive query answering For the reasoning reduction, a naive solution is to use OWL 2 DL punning where a Hi(Horn-SROIQ) KB can be considered as a Horn-SROIQ KB by treating the multiple uses of a same name as completely separate. Although simple, completeness can not be guaranteed. Next, we explain the reason and provide a technique to obtain completeness. Before that, we rst show a way of translating a Hi(Horn-SROIQ) KB into a Horn-SROIQ KB by renaming the names appearing in the class and role positions in the original KB.

class C

c(C) role R P P r(R) vr(P ) vr(P )

A vc(A) fag fag axiom ( ) 9S:Self 9 r(S):Self C vc D c(C) v c(D) :B : r(B) ! vr R !0 v r(R) C u D c(C) u c(D) Disj(S; R) Disj( r(S); r(R)) C t D c(C) t c(D) B(a) c(B)(a) 9R:C 9 r(R): c(C) R(a; b) r(R)(a; b) 8R:C 8 r(R): c(C) a b a b 1S:D 1 r(S): c(D) a 6 b a 6 b mS:D m r(S): c(D) atom ( ) A(x) vc(A)(x) P (x; y) vr(P )(x; y) x y x y

Let NC and NR be two disjoint sets of names for Horn-SROIQ classes and roles such that NC and NR are disjoint with N and have the same size with N . For simplicity, we specify N to be the set of names for Horn-SROIQ individuals. Let vc and vr be two injective functions that map each name in N to a unique Horn-SROIQ class name and role name, respectively. The translation of Hi(HornSROIQ) classes and roles as well as axioms, assertions and query atoms is realized by functions c, r and de ned in gure 3. For a Hi(Horn-SROIQ) KB K, we use (K) to denote the KB obtained by replacing each axiom (assertion) in K with ( ). And for a conjunctive query q, we use (q) to denote the query obtained by replacing each query atom in q with ( ). The soundness of punning in terms of KB non-satis ability and conjunctive query answering is shown in the following proposition.

Proposition 1 For Hi(Horn-SROIQ) KB K, we can get that:

if K is v-satis able then (K) is satis able; ans( (q); (K)) ansv(q; K)1 for each conjunctive query q.

Next, we show the incompleteness of punning by an example. Consider the Hi(Horn-SROIQ) KB K in example 1. Obviously, K is v-satis able. However, when we add the axiom (g): FootballTeam vc AllStarTeam to it, the resultant KB K0 is not v-satis able anymore. Since, under v-semantics, by (d), (c), (b) and (a), we can get that K j=v FootballTeam vc :AllStarTeam. This conclusion contradicts with (g). However K0 is still satis able in terms of punning. Such incompleteness is caused by the fact that under v-semantics, the behaviors of names used as individuals e ect the same names used as classes and roles.

For completeness, an intuitive way is to use materialization, i.e, materializing the entailments that can be entailed by v-semantics but not punning to the original Hi(Horn-SROIQ) KBs. The next Lemma, which illustrates a su cient and necessary condition under which v-semantics and punning coincide in terms of KB satis ability and conjunctive query answering, indicates a way of doing such materialization soundly and completely.

Lemma 1 For a Hi(Horn-SROIQ) KB K, if K contains the axiom a =c b and a =r b for each two di erent names a and b in N such that (K) j= a b, then:

K is v-satis able i (K) is satis able; ansv(q; K) = ans( (q); (K)) for each conjunctive query q;

For a Hi(Horn-SROIQ) KB K, by lemma 1, the materialization can be easily realized by the following two steps. (1) If (K) is satis able then for each assertion a b entailed by (K), add the axioms a =c b and a =r b to K; (2) Iterate (1) until K does not change anymore. Then by proposition 1 and lemma 1, we can easily obtain that reasoning with the original KB under v-semantics can 1 ans( (q); (K)) denotes the set of certain answers of (q) over (K) be captured by reasoning with the resultant KB using punning soundly and completely. However, such naive way of materialization will lead to the size of the original KB increased quadratically.

Note that, lemma 1 also indicates that if a Hi(Horn-SROIQ) KB cannot entail any equivalence between di erent names by punning then v-semantics and punning are also coincident in terms of KB satis ability and conjunctive query answering. This motivates us that in order not to increase the size of the original Hi(Horn-SROIQ) KB, for each detected name equivalence, we use one name to replace the other name in the original KB rather than add new axioms. For a Hi(Horn-SROIQ) KB K, let a and b be two tuples such that jaj = jbj = 0. Then such materialization procedure can be realized by the following two steps: Step 1: If (K) is satis able then for each two di erent names a and b such that (K) j= a b, let K = K[b=a], b = (b; b) and a = (a[b=a]; a); Step 2: Iterate step 1, until K does not change anymore.

For K, we use Ke to denote the KB obtained by step 1 and step 2. And we use "K to denote the corresponding substitution [b=a]. The correctness of this materialization procedure can be guaranteed by the following two lemmas which respectively indicate that after a sires of name replacement, the resultant KB is still a Hi(Horn-SROIQ) KB, and reasoning with the original KB can be captured by the resultant KB soundly and completely.

Lemma 2 Let K be a Hi(Horn-SROIQ) KB and a and b be two names in N . If (K) is satis able and entails a b then K[b=a] is still a Hi(Horn-SROIQ) KB. Lemma 3 Let K be a Hi(Horn-SROIQ) KB and = [b=a] a substitution such that K j=v a[i] b[i] for each 1 i jbj. If K is a Hi(Horn-SROIQ) KB, then:

K is v-satis able i K is v-satis able; u 2 ansv(q; K) i u 2 ansv(q ; K ) for each conjunctive query q.

Combing the above three lemmas, we can nally obtain the way of reducing v-satis ability checking and conjunctive query answering in a Hi(Horn-SROIQ) to the corresponding reasoning tasks in a Horn-SROIQ KB with size no more than the original KB soundly and completely, showing in the following theorem.

Theorem 1 For Hi(Horn-SROIQ) KB K, the following three conclusions hold:

Ke is a Hi(Horn-SROIQ) KB;

K is v-satis able i (Ke) is satis able; u 2 ansv(q; K) i u"K 2 ans( (q"K); (Ke)) for each conjunctive query q.

Example 2. For the KB K in example 1, by step 1 and step 2, we can obtain a Hi(Horn-SROIQ) KB Ke = K"K where "K = [Football team=FootballTeam]. By theorem 1, we can get that v-satis ability checking and conjunctive query answering in K can be captured by Ke soundly and completely.

Meta-query answering in Hi(Horn-SROIQ) For a Hi(Horn-SROIQ) KB K, analogous to lemma 3, we can get that meta-query answering in K can be captured by meta-query answering in the materialized KB Ke, showing in the following lemma.

Lemma 4 For a Hi(Horn-SROIQ) KB K and meta-query Q, then we can get that u 2 ansv(Q; K) i u"K 2 ansv(Q"K; Ke).

For a Hi(Horn-SROIQ) KB K and meta-query Q, a CP-binding of Q over K is a function that maps each class variable of Q to > or a name used as class in K and maps each role variable of Q to a name used as role in K. We use Q to denote the conjunctive query obtained by replacing each appearance of x in Q with (x) for each class (role) variable x of Q. The following theorem shows that meta-query answering over the materialized KB can be captured by conjunctive query answering through CP-bindings.

Theorem 2 Let K be a v-satis able Hi(Horn-SROIQ) KB. Then for each metaquery Q, we can get that u 2 ansv (Q; Ke) i there exists a CP-binding of Q over Ke such that u 2 ansv (Q ; Ke).

Example 3. Consider the Hi(Horn-SROIQ) KB K in example 1 again. Suppose we want to know whether there exists a role that relates BarcelonaDragous to FootballTeam. This task can be realized by answering the query Q over K: ?p(BarcelonaDragous; FootballTeam) ! q() By theorem 2, lemma 4 and theorem 1, we can get that answering Q over K, can be realized by evaluating the conjunctive query:

rewriteOf(BarcelonaDragous; FootballTeam) ! q() over Ke in terms of punning, since Q"K has just one CP-binding over Ke.

Furthermore, by theorem 2 and 1 as well as the results in [29], we can get that meta-query answering in Hi(Horn-SROIQ) has universal model feature [29].

Theorem 3 Let K be a v-satis able Hi(Horn-SROIQ) KB. Then K has v-model V such that u 2 ansv(Q; K) i V j=v Q[x=u] for each meta-query Q with head x.

4

Complexity of reasoning with Hi(Horn-SROIQ)

In this section, we investigate the complexity of reasoning with Hi(Horn-SROIQ). Before that, we rst show the complexity of materializing Hi(Horn-SROIQ) KBs. Theorem 4 For Hi(Horn-SROIQ) KB K = (T ; A), the procedure of computing

Ke terminates. Moreover Ke can be obtained in 2ExpTime w.r.t. jKj and PTime w.r.t. jAj.

Based on theorem 1 and theorem 4 as well as the results in [28], we can get the complexities of v-satis ability checking in Hi(Horn-SROIQ). Theorem 5 For Hi(Horn-SROIQ) KB K = (T ; A), v-satis ability checking of

K can be done in 2ExpTime w.r.t. jKj and PTime w.r.t. jAj.

For a Hi(Horn-SROIQ) KB K = (T ; A) and meta-query Q, theorem 2 indicates that answering Q over K needs to evaluate as many as jKjjQj conjunctive queries over a Horn-SROIQ KB with size no more than K. Actually, in the appendix of this paper, we show that the number of queries need to be answered can be measured by the size of T . Then based on the results in [29], we can obtain the complexity of answering Q over K.

Theorem 6 For Hi(Horn-SROIQ) KB K and meta-query Q, ansv(Q; K) can be computed in 2ExpTime-complete w.r.t. jKj and PTime-complete w.r.t. jAj.

The above two theorems indicate that adding meta-modeling capability to Horn-SROIQ has no impact on the complexity of the considered reasoning tasks. 5

Related work

Here, we discuss other works on extending decidable DLs with meta-modeling.

[26] investigates extending SHOIQ with meta-modeling by unifying the sets of names for classes, roles and individuals. In [26], v-satis ability checking of a SHOIQ KB can be realized by checking the satis ability of as many as 2n2 SHOIQ KBs where n denotes the number of di erent names in the original KB. Thus satis ability checking in the extended SHOIQ under v-semantics has NExpTime combined complexity. Excepting high reasoning complexity, query answering has not been discussed in [26]. On the other hand, [ 3 ] addresses extending SHIQ with meta-modeling under a stronger variant of the HiLog-style semantics where extensions are also assigned to complex classes and roles. However, punning is adopted to reason with the extended SHIQ with coNP-complete data complexity of both satis ability checking and query answering. Compared with these two works, although some class axioms are not allowed in Hi(HornSROIQ), such as A t B v C, Hi(Horn-SROIQ) supports richer role axioms, such as role chains ( ) and role disjoint axioms, which are useful in medical terminologies. Most importantly, Hi(Horn-SROIQ) has much lower data complexities of satis ability checking and meta-query answering. Extension of tractable language DL-LiteR is discussed in [ 3, 22 ]. Although low complexity can be guaranteed, the expressivity is every restricted.

Moreover, [ 11, 13, 24, 25, 30 ] study typed meta-modeling extension or extension based on Henkin semantics [ 12 ]. The referred DLs contain SHOIQ, SROIQ, ALCQ and SHIQ. In the typed situation, names are typed with layer or level information (non-negative integer numbers) with the intention to describe levels of classes and roles. However, describing axioms (assertions) referring names with di erent types is limited or not allowed. Furthermore, the actual OWL 2 Full ontologies do not contain such way of meta-modeling. On the other hand, Henkin semantics, which deals with higher-order structures via a hierarchy of power sets, is stronger than HiLog-style semantics. In this semantics, the class extensions of names are the sets in the domains they mapped into. Thus the claim KB j= a b i KB j= a =c b holds. However, for both OWL 2 RDF Based Semantics and HiLog-style semantics, just the \if-then" direction holds. Moreover, under this semantics, some undesired conclusions may be entailed. For example, from the knowledge (RDF triple (a), (b) and (c)) described in Linked Open Data: (geosp : Country; owl : equivalentClass; geo : Pays) (a) (geosp : Country; rdfs : isDefinedBy; geospecies:owl) (b) (geo : Pays; rdfs : isDefinedBy; geo fr) (c) (geo : Pays; rdfs : isDefinedBy; geospecies:owl) (geosp : Country; rdfs : isDefinedBy; geo fr) (d) (e) under this semantics, we can obtain the conclusion (d) and (e). However, neither of them are desired.

Finally, we mention [ 7 ] and [ 21 ]. [ 7 ] discusses ontology-inherent meta-modeling for classes in OWL 2 DL by adding extra names, axioms and assertions. The limitation of this approach is that just two layers (classes and meta-classes) of meta-modeling can be supported. By combing and unifying some of the above mentioned approaches, [ 21 ] investigates a variant of higher-order DLs, containing (a) a xly interpreted instanceOf role connecting individuals with classes; (b) promiscuous classes may have roles and other classes as individuals; (c) strictly typed classes allowing only a certain type of individuals. 6

Discussion and conclusions

In this paper, we discuss the problem of e ciently reasoning and query answering in expressive domain KBs that are in OWL 2 Full and contain large individual datasets. For this, we introduce Hi(Horn-SROIQ) and meta-queries, and provide concrete methods of reasoning with Hi(Horn-SROIQ). For the future research, our work can be extended in the following two aspects. Firstly, theorem 2 indicates that evaluating a meta-query Q over a Hi(Horn-SROIQ) KB K may need to answer a lot of conjunctive queries over a Horn-SROIQ KB. Although having low data complexity, heuristics, such as query partition, are needed to optimize such meta-query answering procedure. And secondly, the main motivation of this paper is to discuss the theoretic features of Hi(Horn-SROIQ), thus, experiments on actual OWL 2 Full ontologies, such as OpenCyc and SUMO, are needed to validate the overall provided method.

Acknowledgments

This work was supported by the Natural Science Foundation of China (No. 61232015), the National Key Research and Development Program of China (Grant No. 2002CB312004), and the Knowledge Innovation Program of the Chinese Academy of Sciences. 25. Motz, R., Rohrer, E., and Severi, P. The description logic SHIQ with a exible meta-modeling hierarchy. Web Semantics: Science, Services and Agents on the World Wide Web. 35(4):214-234, 2015. 26. Motik, B. On the Properties of Metamodeling in OWL. J. of Logic and Computation, 17(4):617-637, 2007. 27. Noy, N F., Rubin, D L. Translating the foundational model of anatomy into OWL.

Web Semantics: Science, Services and Agents on the World Wide Web, 6(2):133-136, 2008. 28. Ortiz, M., Rudolph, S., and Simkus, M. Worst-case Optimal Reasoning for the

Horn-DL fragements of OWL 1 and OWL 2. In Proc. KR, 2010. 29. Ortiz, M., Rudolph, S., and Simkus, M. Query Answering in the Horn Fragments of the Description Logics SHOIQ and SROIQ. In Proc. IJCAI, 2011. 30. Pan, J Z., and Horrocks, I. OWL FA: A Metamodeling Extension of OWL DL. In

Proc. WWW, 1065-1066, 2006. 31. Pease, A., Niles, I., and Li, J. The suggested upper merged ontology: A large ontology for the semantic web and its applications. In Proc. AAAI, 2002. 32. Schneider, M. OWL 2 Web Ontology Language RDF-Based Semantics (Second Edition). W3C Recommendation 11 December 2012, http://www.w3.org/TR/owl2rdf-based-semantics/, 2012. 33. Sirin, E., Parsia, B., Grau, B C., Kalyanpur, A., and Katz, Y. Pellet: A practical OWL-DL reasoner. J. of Web Semantics 5(2): 51-53, 2007.

References

1. Bienvenu , M. , Lutz , C. , and Wolter , F. First-Order Rewritability of Atomic Queries in Horn Description Logics . In Proc. IJCAI , 754 - 760 , AAAI Press, 2013 .

2. Chen , W. , Kifer , M. , and Warren , D S. HILOG: a foundation for higher-order logic programming . J. of Logic Programming , 15 ( 3 ): 187 - 230 , 1993 .

3. De Giacomo, G. , Lenzerini , M. , and Rosati , R. Higher-Order Description Logics for Domain Metamodeling . In Proc. AAAI , 2011 .

4. Eiter , T. , Ortiz , M. , Simkus , M. , Tran , T K. , and Xiao , G. Towards Practical Query Answering for Horn-SHIQ? . In Proc. DL , 2012 .

5. Faddoul , J. , Farsinia , N. , Haarslev , V. , and Moller, R. A Hybrid Tableau Algorithm for ALCQ . In Proc. DL , 2008 .

6. Glimm , B. , and Ogbuji , C. SPARQL 1.1 Entailment Regimes . W3C Recommendation 21 March 2013 , http://www.w3.org/TR/sparql11-entailment/, 2013 .

7. Glimm , B. , Rudolph , S. , and Volker J. Integrated Metamodeling and Diagnosis in OWL 2 . In Proc. ISWC , 257 - 272 , 2010 .

8. Glimm , B. , Horrocks , I. , Motik , B. , Stoilos , G. , and Wang , Z. HermiT: An OWL 2 Reasoner . J. of Automated Reasoning , 53 ( 3 ): 245 - 269 , 2014 .

9. Golbreich , C. , and Wallace , E K. OWL 2 Web Ontology Language New Features and Rationale (Second Edition) . W3C Recommendation 11 December 2012 , http://www.w3.org/TR/owl2-new-features/, 2012 .

10. Haarslev , V. , Hidde , K. , Moller, R., and Wessel , M. The RacerPro knowledge representation and reasoning system . Semantic Web Journal , 3 ( 3 ): 267 - 277 , 2012 .

11. Homola , M. , Kl 'uka, J., Svatek , V. , and Vacura , M. Typed High-Order variant of SROIQ-Why Not? In Proc. DL , 2014 .

12. Henkin , L. Completeness in the theory of types . J. Symbolic Logic , 15 : 81 - 91 , 1950 .

13. Homola , M. , Kl 'uka, J., Svatek , V , and Vacura , M. Towards Typed Higher-Order Description Logics . In Proc. DL , 2013 .

14. Horrocks , I. , Kutz , O. , and Sattler , U. The Even More Irresistible SROIQ . In Proc. KR , 57 - 67 , 2006 .

15. Horrocks , I. , and Sattler , U. A Tableau Decision Procedure for SHOIQ . J. of Automated Reasoning , 39 ( 3 ): 249 - 276 , 2007 .

16. Horrocks , I. , and Sattler , U. Decidability of SHIQ with complex role inclusion axioms . Arti cial Intelligence , 160 ( 1 ): 79 - 104 , 2004 .

17. Horrocks , I. , Sattler , U. , Tobies , S. Practical Reasoning for Very Expressive Description Logics . Logic Journal of the IGPL , 8 ( 3 ): 239 - 263 , 2000 .

18. Iban ~ez-Garc a , Y., Lutz , C. , and Schneider , T. Finite Model Reasoning in Horn Description Logics . In Proc. KR , 2014 .

19. Kazakov , Y. Consequence-driven reasoning for Horn-SHIQ ontologies . In Proc. IJCAI , 2040 - 2045 , 2009 .

20. Krotzsch, M. , Rudolph , S. , and Hitzler , P. Complexities of Horn Description Logics . ACM Transactions on Computational Logic , 14 ( 1 ):2: 1 - 2 : 36 ,, 2013 .

21. Kubincova P , Kl'uka J , Homola M . Towards Expressive Metamodelling with Instantiation . In Proc. DL , 2015 .

22. Lenzerini , M. , Lepore , L. , and Poggi , A. Practical query answering over Hi(DLLiteR) knowledge bases . In Proc. DL , 2014 .

23. Matuszek , C. , Cabral , J. , Witbrock , M. , and DeOliveira, J. An Introduction to the Syntax and Content of Cyc . In AAAI Spring Symposium , 2006 .

24. Motz , R. , Rohrer , E. , and Severi , P. Reasoning for ALCQ Extended with a Flexible Meta-Modelling Hierarchy . In Proc. JIST , 47 - 62 , 2014 .