With the motivation of reasoning with real-world, complex domain ontologies in the category of OWL 2 Full, in this paper, we study meta-modeling extension in SROIQ, and propose an expressive sub-language of OWL 2 Full, called Hi(SROIQ), where the same names can be used as classes, roles and individuals simultaneously. For accessing meta-knowledge, meta-queries are introduced by allowing variables to occur in the class and role positions in conjunctive queries. In order to take advantage of the highly optimized reasoners for description logics, we provide a sound and complete way of reducing satis ability checking and meta-query answering in Hi(SROIQ) to the corresponding reasoning tasks in SROIQ. Based on this, we conclude that meta-modeling extension in SROIQ does not increase the complexity of reasoning.
Ontology jTBoxj jABoxj jClaj jRolj jIndj jCla \ Indj jRol \ Indj OpenCyc 282,613 2,699,372 119,962 26,832 1,077,732 116,842 26,829 SUMO 7,081 489,949 4,557 898 256,576 3,591 654 FMA 82,834 1,923,155 84,395 170 222,578 78,988 170 CHEBI 224,963 2,656,188 191,293 37 800,308 122,057 17 GO 154,270 622,341 149,026 217 227,050 47,483 177 NCI 180,890 1,305,846 239,504 177 119,115 118,941 173 OGG 70,232 1,068,010 70,127 133 70,557 69,688 105 a syntactic solution, punning would not infer any more entailments than OWL 2 DL. Besides punning, there exist works studying meta-modeling extension in description logics (DLs) based on di erent semantics and application motivations.
Among these works, [5{12] study meta-modeling extension by allowing names to have multiple uses and based on HiLog semantics [4] which takes the same way as the OWL 2 RDF-Based semantics (the de facto semantics of OWL 2 Full) [3] to interpret the multiple uses of names. Concretely, [5], [6] and [10] respectively discuss extending SHOIQ [19], SHIQ [20] and DL-LiteR and provide the languages SHOIQ with meta-modeling, Hi(SHIQ) and Hi(OWL2QL). For SHOIQ with meta-modeling and Hi(SHIQ), complex role axioms and Self restriction which are usually used in biomedical ontologies are not supported. The expressivity of Hi(OWL2QL) is too limited to capture the complex knowledge described in actual complex ontologies. Complex axioms about roles can be captured by Hi(Horn-SROIQ), Hi(SRIQ) and HI(SROIQ) respectively proposed by [7], [8] and [12] and obtained by extending Horn-SROIQ [23], SRIQ [22] and SROIQ [24]. However, Hi(SRIQ), Hi(Horn-SROIQ) and HI(SROIQ) respectively do not support nominals, disjunctions and metamodeling on roles which are heavily used in the KBs listed in Table 1. Moreover, meta-query answering is also discussed in these works except [5, 12].
On the other hand, works [13{18] study typed meta-modeling extension or
extension based on Henkin semantics. Henkin semantics deals with higher-order
structures via hierarchies of power sets. Under this semantics, for a KB K, the
relation (r) K j= a =c b , K j= a b holds, where =c and respectively denote
class equivalence and individual equivalence. However, in both HiLog semantics
and OWL 2 Full RDF-Based Semantics, solely the (() direction of (e) holds.
Henkin semantics may make undesired conclusions be entailed. For example,
consider the following knowledge (
In order to reason with the actual, complex OWL 2 Full ontologies, in this
paper we study meta-modeling extension in the expressive DL SROIQ by allowing
all the names to have multiple uses without any restrictions and based on HiLog
semantics. The contribution can be summarized as follows. (
Compared with [12], besides meta-modeling on roles and meta-query answering, we provide a di erent way of reasoning reduction without increasing the size of the original KBs, however the price is to consider more than one DL KB when reasoning with and querying a Hi(SROIQ) KB. Based on the results in [18], [12] provides a reasoning reduction procedure by adding extra axioms and assertions to the original KB. Besides increasing the sizes of the KBs, this approach cannot be applied to reduce reasoning in Hi(L) to the corresponding reasoning in L, where L is a sub-language of SROIQ without nominals, : and 8. 2 2.1
Hi(SROIQ) is de ned based on SROIQ. Di erent to SROIQ, Hi(SROIQ) has only one name set N for classes, roles and individuals. This means that the same names in N can be used as classes, roles and individuals at the same time. The syntax of Hi(SROIQ) is illustrated in the following de nitions. De nition 1. A Hi(SROIQ) role is either a role name P 2 N or its inverse P . In order not to consider the roles in the form of P , we de ne P = P . A Hi(SROIQ) RBox is a nite set of role axioms with the following forms: S1
Sn vr R; Dis(S1; S2); Ref(R); Irr(R) where S1{Sn and R are roles. The Hi(SROIQ) classes C and D are inductively de ned as follows: 4 https://github.com/Lucy321456/SupplementaryFile/blob/master/DL19-proofs.pdf
C; D ::= A j fog j 9S:Self j :C j C u D j C t D j 9R:C j 8R:C j nS:C j nS:C where A 2 N and o 2 N are respectively called class name and individual, n is a non-negative integer, R and S are roles. A Hi(SROIQ) TBox T is a nite set of class inclusion axioms in the form of C vc D where C and D are classes. A Hi(SROIQ) ABox A is a nite set of individual assertions with the forms:
C(a); R(a; b); :S(a; b); a b; a 6 b where C is a class, both R and S are roles, and a; b 2 N are called individuals.
Hi(SROIQ) does not separate the names for classes, roles and individuals,
thus the symbols vc and vr are used to distinguish between class inclusion
axioms and role inclusion axioms. For simplicity, we use a =l b to abbreviate
these two axioms a vl b and b vl a, where l 2 fc; rg. For decidability, the regular
role hierarchy and simple role restrictions de ned in SROIQ [24] are adopted.
De nition 2. For a Hi(SROIQ) RBox R, we say R is regular if there exists
a partial order (an irre exive and transitive relation) on N [ fn jn 2 Ng
such that: (
Sn vr R; RS1
Sn vr R; S1
SnR vr R
where R is a role and Si R for each 1 i n. Given a Hi(SROIQ) RBox
R, the set of simple roles is inductively de ned as following. A role R is simple,
if (
By De nitions 1{2, Hi(SROIQ) KBs are illustrated in the de nition below. De nition 3. A Hi(SROIQ) KB K = (R; T ; A) is a tuple where R, T and A are respectively regular RBox, TBox and ABox, and all the roles (R=S) occurring in the role positions of the following expressions are simple roles. nR:C;
nR:C; 9R:Self; Dis(R; S); Irr(R); :R(a; b) We use ind(K) to denote the set of all the names used as individuals in A or T , and use nSR(K) to denote the set of all the non-simple roles w.r.t. R.
The following example illustrates a Hi(SROIQ) KB about the knowledge of football teams described in the OpenCyc ontology.
Example 1. Consider the Hi(SROIQ) KB K consisting of the axioms and
individual assertions (
SportsTeam vc :AllStarTeam; Football team vc SportsTeam (
FootballTeam Football team (
Let V be a set of variables so that V\N = ;. The syntax of meta-queries is illustrated in the de nition below. De nition 4. A query atom takes the form of x(y) or x(y; z) 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, x is a tuple of elements in N [ V and each variable in n x occurs in some i. We de ne body(Q) = [i=1f ig and head(Q) = x.
For meta-query Q, a variable x is called a distinguished variable of Q if x occurs in head(Q), and x is called a non-distinguished variable of Q if x solely occurs in body(Q). Moreover, x is called a class variable (role variable) of Q if Q contains an atom x(y) (x(y; z)). If Q does not contain any class or role variables then it becomes a conjunctive query. By allowing variables to occur in the class and role positions, schema knowledge and data can be queried in a uniform way. For example, the query asking for the types of the team BarcelonaDragons can be formally represented as the following meta-query:
?x(BarcelonaDragons) ^ SportsTeamTypeBySport(?x) ! q(?x)
Hi(SROIQ) and meta-queries are interpreted by the -semantics [5] which is based on HiLog semantics.
Syntax Semantics Syntax Semantics
P RV (P V ) C t D CV (C) [ CV (D)
P f(y; x)j(x; y) 2 RV (P V )g C u D CV (C) \ CV (D)
! RV (R1) RV (R1) C vc D CV (C) CV (D)
A CV (AV ) ! vr R RV (R1 Rn) RV (R)
fag faV g Dis(S; R) RV (S) \ RV (R) = ;
9S:Self fxj(x; x) 2 RV (R)g Ref(S) f(x; x)jx 2 V g RV (S)
:C V CV (C) Irr(S) f(x; x)jx 2 V g\ RV (S) = ;
nS:D fxjjfyj(x; y) 2 RV (S)^y 2 CV (D)gj ng C(a) aV 2 CV (C)
nS:D fxjjfyj(x; y) 2 RV (S)^y 2 CV (D)gj ng R(a; b) (aV ; bV ) 2 RV (R)
9R:C fxj9y:(x; y) 2 RV (R) ^ y 2 CV (C)g :S(a; b) (aV ; bV ) 2= RV(S)
8R:C fxj8y:(x; y) 2 RV (R) ! y 2 CV (C)g a b; a 6 b aV = bV ; aV 6= bV
De nition 5. A -interpretation V = ( V ; V ; CV ; RV ) is a tuple where V is a
non-empty set, V , CV and RV are functions such that (
Di erent to the classic semantics of DLs, under -semantics, each name is mapped into a domain element and each domain element is associated with a class extension and a role extension. The motivation is to guarantee that if two names a and b are mapped into the same domain element, i.e., they denote the same semantic entity, then they should have the same class and role extension, i.e., CV (aV ) = CV (bV ) and RV (aV ) = RV (bV ). Such distinguished feature is crucial in enabling Hi(SROIQ) KBs to entail more conclusions compared with punning. However, this feature may cause Hi(SROIQ) KBs to imply the equivalences between non-simple roles and simple roles, as shown in the example below. Example 2. Consider the KB consisting of the following axioms and assertions: RP1 vr P1; P1P2 vr P2; P2P3 vr P3; P3S vr S; SS vr S > vc 5R:>; R
S Obviously, R is a simple role and S is a non-simple role. Under -semantics, the individual assertion R S implies that R and S are equivalent roles, i.e., R =r S holds, as RV (RV ) = RV (SV ) holds for each -model V of this KB.
Such implied equivalences between simple-roles and non-simple roles can lead
to (
For decidability, we only consider the KBs adopting UNSRA. For a tuple u, we use juj and u[i] to denote the length and the i-th element of u, respectively. For a tuple x with length juj, we use [x=u] to denote a substitution. For a KB, tuple or query O, we use O[x=u] to denote the result of replacing each occurrence of x[i] in O with u[i], for 1 i jxj. For a query Q and tuple u with length jhead(Q)j, we use Q(u) to denote Q[head(Q)=u]. The semantics of meta-queries is illustrated in the de nition below.
De nition 7. For a meta-query Q and -interpretation V, a binding of Q over V is a function that maps each name a in Q to aV and each variable in Q to an element in V . We write V; j= Q if (y) 2 CV ( (x)) for each x(y) 2 body(Q) and ( (y); (z)) 2 RV ( (x)) for each x(y; z) 2 body(Q). We write V j= Q if there exists a binding of Q over V such that V; j= Q. For a Hi(SROIQ) KB K, a tuple u consisting of names in K and with length head(Q) is called a certain answer of Q over K if for each -model V of K, V j= Q(u) holds and for 1 i juj, if head(Q)[i] 2 N then u[i]V = head(Q)[i]V holds. We use answer (Q; K) to denote the set of all the certain answers of Q over K. 3
Here, we present the way of reducing -satis ability checking in Hi(SROIQ) to satis ability checking in SROIQ with the aid of punning. Before that, we rst show the translation from Hi(SROIQ) KBs to SROIQ KBs via renaming.
Let C and R be the sets of names for SROIQ classes and roles, respectively. For simplicity, we suppose N is the set of names for SROIQ individuals. Let v c and v r be two bijective functions that respectively map each name in N to an unique name in C and an unique name in R. The translation of Hi(SROIQ) classes, roles, axioms and assertions realized by functions c, r and is illustrated in Fig. 2. For a Hi(SROIQ) KB K, we use dl(K) to denote the KB obtained by replacing each axiom (assertion) in K with ( ). The soundness of punning can be guaranteed by the proposition below.
f
P; P r R1 c
A; fog 9S:Self :C nS:D nS:D 9R:C 8R:C f ( ) v r(P ); v r(P ) Rn r(R1) r(Rn) v c(A); fog 9 r(S):Self : c(C) n r(S): c(D) n r(S): c(D) 9 r(R): c(C) 8 r(R): c(C) f
C t D c C u D f ( ) c(C) t c(D) c(C) u c(D) C vc D c(C) v c(D) R1 Rn vr R r(R1) r(Rn) v r(R) Dis(S; R) Dis( r(S); r(R)) Ref(S); Irr(S) Ref( r(S)); Irr( r(S)) C(a); :S(a; b) c(C)(a); : r(S)(a; b) R(a; b) r(R)(a; b) a b; a 6 b a b; a 6 b Example 3. Consider the Hi(SROIQ) KB K consisting of the following axiom and individual assertions described in the OpenCyc KB.
PrimeMinister HeadOfGovernment vc :Prime minister (
PrimeMinister HeadOfGovernment(MargaretThatcher) (
The incompleteness is caused by the fact that under -semantics, the behaviors of names used as individuals will a ect the same names used as classes or roles, i.e., if a KB implies the assertion a b then the axioms a =c b and a =r b are also implied, whereas under punning, such impact of individuals on classes and roles do not exist anymore. Inspired by the results in [5, 7], next we present an approach of materializing such impact in the original KB in order to obtain completeness. Before this, we rst illustrate a su cient and necessary condition under which -semantics and punning coincide in terms of KB satis ability. Lemma 1. For a Hi(SROIQ) KB K = (R; T ; A), if a 6 b 2 A for each (a; b) 2 ind(K)2 and a 6= b, then K is -satis able i dl(K) is satis able.
Lemma 1 indicates that if all the individuals of K are pairwise nonequivalent
then punning and -semantics are coincide in terms of satis ability checking.
Based on Lemma 1, the basic idea of materializing the impacts of individuals on
classes and roles is to rst guess the equivalence between individuals implied by
a KB, and then for the guessed equivalent individuals, in order not to increase
the size of the original KB, we choose to replace them with the same
representative in the KB rather than add extra class and role equivalent axioms. Note
that the guess of the equivalence between individuals rather than detecting such
equivalence by DL Reasers like [7] is caused by the \uncertainty" of individual
equivalence entailment resulted from number restrictions ( n).
Example 4. Consider the KB K consisting of the following axioms and assertions:
A vc 2R:B; a vc :b; a vc :c; b vc :c; a(b); b(a); c(b) (
A(a); R(a; b); R(a; c); R(a; a); B(a); B(b); B(c) (
For a function f , we use dom(f ) and ran(f ) to denote the domain and range of f , respectively. For a KB, query or tuple O, we use Of to denote the result of replacing each occurrence of a in O with f (a) for each a 2 dom(f ). Next, we formalize the materialization and reduction technique in detail.
De nition 8. For a Hi(SROIQ) KB K, a function E is called a candidate individual equivalence replacing function (CIERF) of K if dom(E) = ran(E) = ind(K) nSR(K) and E(E(a)) = E(a) for each a 2 dom(E).
In De nition 8, E(E(a)) = E(a) requires that the representatives for the
guessed equivalent individuals will not be replaced by other individuals.
Moreover, both dom(E) and ran(E) do not contain non-simple roles, since (
The concrete way of reducing -satis ability checking in Hi(SROIQ) to satis ability checking in SROIQ with the aid of punning and the materialization technique is shown in the following theorem.
Theorem 1. A Hi(SROIQ) KB K is -satis able i there exists a CIERF E of K such that dl([KE]) is satis able.
Note that for a partition P of the set ind(K) nSR(K), choosing di erent representative elements for the sets in P will generate di erent CIERFs of K, thus yielding di erent materialized KBs. Take the KB K in Example 3 as an example. For the following partition P of ind(K) nSR(K):
ffPrimeMinister HeadOfGovernment; Prime minister; MargaretThatchergg totally three CIERFs E1{E3 can be generated by choosing di erent representives for the sole equivalence class in P. Nevertheless, as shown in the lemma below, di erent CIERFs corresponding to the same partition do not a ect the result of satis ability checking, i.e., [KE1]{[KE3] are pairwise equisatis able. Lemma 2. For a Hi(SROIQ) KB K and two CIERFs E1 and E2 of K such that for each (a; b) 2 (ind(K) nSR(K))2 and a 6= b, E1(a) = E1(b) holds i E2(a) = E2(b) holds, then dl([KE1]) is satis able i dl([KE2]) is satis able.
Lemma 2 implies that for each partition P of ind(K) nSR(K), considering one CIERF is su cient. Thus for checking the -satis ability of K, no more than 2jind(K) nSR(K)j2 SROIQ KBs need to be considered. Then based on [13], we can further obtain the complexity of -satis ability checking in Hi(SROIQ). Theorem 2. Checking the -satis ability of a Hi(SROIQ) KB K can be done in N2ExpTime w.r.t. the size of K.
Thus meta-modeling extension in SROIQ does not increase the complexity of reasoning. However, Theorem 1 indicates that checking the -satis ability of a Hi(SROIQ) KB K may need to consider as many as an exponential size of SROIQ KBs w.r.t. jind(K)j. Therefore, we further provide a condition to reduce the number of SROIQ KBs needed to be considered.
Lemma 3. For a CIERF E of a Hi(SROIQ) KB K = (R; T ; A), if there exist (a; b) 2 (ind(K) nSR(K))2 satisfying that E(a) = E(b) and dl(K) j= a 6 b, or that E(a) 6= E(b) and dl(K) j= a b, then dl([KE]) is not satis able. Example 5. Consider the KB K in Example 3 again. Lemmas 2{3 indicate that for a partition P of ind(K) nSR(K), if there does not exist U 2 P such that fPrimeMinister HeadOfGovernment; Prime ministerg U , then for each CIERF E generated from P, dl([KE]) is not satis able. Three out of ve partitions of ind(K) nSR(K) satisfy this condition. Thus, checking the -satis ability of K solely needs to consider the satis ability of two SROIQ KBs rather than ve. 4
Here, we rst present the way of reducing conjunctive query (CQ) answering in Hi(SROIQ) to CQ answering in SROIQ, then we show that meta-query answering in Hi(SROIQ) can be captured by CQ answering.
For the reduction of CQ answering, a naive solution is to use punning. For a CQ Q, we use dl(Q) to denote the result of replacing each atom A(x) in Q with c(A)(x) and each P (x; y) in Q with r(P )(x; y). The soundness of punning in terms of CQ answering is shown in the proposition below.
Proposition 2. For a -satis able Hi(SROIQ) KB K, answer( dl(Q); dl(K)) answer (Q; K) holds for each CQ Q5.
Nevertheless, similarly to -satis ability checking, by punning technique alone, the completeness of CQ answering cannot be ensured.
Example 6. Consider the KB K in Example 1 again. K is -satis able. For the query Q : Football team(?x) ! q(?x), answer (Q; K) = f(BarcelonaDragons)g holds, since F ootball team F ootballT eam implies the axiom F ootball team =c F ootballT eam. However, answer( dl(Q); dl(K)) = ;, as the class equivalence between Football team and FootballTeam is not implied by K under punning.
The incompleteness is also caused by the impacts of individuals on classes and roles. Thus for completeness, the basic idea is to materialize such impacts. The lemma below indicates that the materialization technique designed for satis ability checking can also be adopted to obtain the completeness of CQ answering. Lemma 4. For a -satis able Hi(SROIQ) KB K = (R; T ; A), if a 6 b 2 A for each (a; b) 2 ind(K)2 and a 6= b, then answer (Q; K) = answer( dl(Q); dl(K)) holds for each CQ Q.
By trying each possibility of materializing the impacts of individuals on classes and roles and then intersecting the answers obtained, we can obtain all the certain answers of CQs over -satis able KBs, shown in the theorem below. Theorem 3. For a -satis able Hi(SROIQ) KB K and conjunctive query Q, let E be the set of all the CIERFs E satisfying that dl([KE]) is satis able, then: answer (Q; K) = \E2E fu j u 2 Njhead(Q)j and uE 2 answer( dl(QE); dl([KE]))g
As mentioned earlier, choosing di erent representatives for the sets in a partition of ind(K) nSR(K) will generate di erent CIERFs of K and thus di erent materialized KBs. However, this does not a ect the result of CQ answering. Lemma 5. For a -satis able Hi(SROIQ) KB K, let E1 and E2 be two CIERFs of K so that dl(KE1) and dl(KE1) are satis able and for each (a; b) 2 (ind(K) nSR(K))2 and a 6= b, E1(a) = E1(b) i E2(a) = E2(b). Then for each CQ Q: answer( dl(QE1); dl([KE1]) = answer( dl(QE2); dl([KE2])
Lemma 5 implies that for a partition of ind(K) nSR(K), considering one CIERF is su cient for CQ answering. Thus answering a CQ over K requires no more than 2jind(K) nSR(K)j2 DL KBs to be considered. Therefor we can further obtain the complexity of CQ answering in Hi(SROIQ).
Theorem 4. answer (Q; K) can be obtained in N2ExpTime w.r.t. the total size of a Hi(SROIQ) KB K and a CQ Q without non-distinguished variables.
The decidability of CQ answering in SROIQ is currently unknown [28]. Thus in Theorem 4, just the CQs without non-distinguished variables are considered. Next, we illustrate the way of answering meta-queries in Hi(SROIQ). 5 For a SROIQ KB O and CQ Q, we use answer(Q; O) to denote the set of all the certain answers of Q over O
For a meta-query Q and Hi(SROIQ) KB K, a CRV-Binding of Q over K is a function that maps each class (resp. role) variable of Q to a name occurring in K. The way of answering the meta-queries without non-distinguished variables by materialization is shown in the theorem below.
Theorem 5. For a -satis able Hi(SROIQ) KB K and meta-query Q without non-distinguished variables, let B be the set of all the CRV-Bindings of Q over K. Then answer (Q; K) = [ 2Banswer (Q ; K) holds.
As shown in the example below, if we allow meta-queries to contain nondistinguished variables, the completeness cannot be guaranteed anymore by class and role variable materialization.
Example 7. Consider the -satis able Hi(SROIQ) KB K and meta-query Q: K = (;; fA vc 9P:B t 9P:Cg; fA(a)g)
Q : A(?x) ^ P (?x; ?z)^?c(?z) ! q(?x) Obviously, answer (Q; K) = f(a)g, as for each -model V of K, aV 2 CV (AV ) holds and there exists A0 2 fB; Cg satisfying that aV 2 CV (9P:A0). However, for each CRV-binding of Q over K, answer (Q; K) = ;, as there does not exist any name A0 in K satisfying that for each -model V of K, aV 2 CV (9P:A0) holds.
By Theorems 3-5, we can further obtain the complexity of answering the meta-queries without non-distinguished variables over Hi(SROIQ) KBs. Theorem 6. answer (Q; K) can be obtained in N2ExpTime w.r.t. the total size of a Hi(SROIQ) KB K and meta-query Q without non-distinguished variables. 5
In order to consume the real-world and complex OWL 2 Full ontologies, in this paper, we propose an expressive sub-language of OWL 2 Full, called Hi(SROIQ), and provide a sound and complete way of realizing satis ability checking and query answering in Hi(SROIQ) as well as prove the complexity of reasoning in Hi(SROIQ). Our future work will mainly focus on optimizing the procedure of reasoning in Hi(SROIQ). As Theorems 1 and 3 indicate, reasoning with a Hi(SROIQ) KB may need to consider an exponential number of SROIQ KBs w.r.t. the number of individuals of this KB. Heuristics shall be devised to reduce the number of such SROIQ KBs. On the other hand, identifying fragments L of Hi(SROIQ) so that solely one DL KB needs to be considered when reasoning and querying an L KB would be an interesting direction to explore. Besides, based on the work [29] which concentrates on optimizing SPARQL query answering in SHOIQ, designing heuristics to optimize the procedure of meta-query answering in Hi(SROIQ) is also valuable and signi cant.
We thank the reviewers for their valuable suggestions and comments.This work has been supported by the National Key Research and Development Program of China under grants 2017YFC1700300, 2017YFB1002300 and 2016YFB1000902.