Consequence-based reasoners are typically significantly faster than tableau-based reasoners for ontology classification. However, for more expressive DL languages like ALCH O, consequence-based reasoners are not applicable, but tableau-based reasoners can sometimes require an unacceptably long time for large and complex ontologies. This paper presents a weakening and strengthening approach for classification of ALCH O ontologies, using a hybrid of consequence- and tableau-based reasoning. We approximate the original ontology Oo by a weakened version Ow and a strengthened version Os, both are in a less expressive DL ALCH and classified by a consequence-based main reasoner. The classification from Ow is sound but possibly incomplete with respect to Oo, while that from Os is complete but possibly unsound. The additional subsumptions derived from Os may be unsound so are further verified by a tableau-based assistant reasoner. A prototype classifier called WSClassifier is implemented based on this hybrid approach. The experiments results show that for classifying many large and complex ALCH O ontologies, WSClassifier's performance is significantly faster than tableau-based reasoners.
The target of classification is to calculate all the subsumption relationships between
atomic concepts implied by the input ontology. (Hyper)Tableau-based [
In this paper we introduce a hybrid reasoning approach for classification of ontologies in the DL ALCH O, using a consequence-based main reasoner MR and a tableau-based assistant reasoner AR. MR provides sound and complete classification over the DL ALCH which is less expressive than ALCH O, while AR provides sound and complete classification over ALCH O. Suppose MR reasoning is much faster than AR. We try to classify an ontology Oo using MR to do the major work, and AR to do auxiliary work. We produce a weakened version Ow by removing from Oo the nominal axioms that are beyond ALCH , and a strengthened version Os by adding to Ow a set of strengthening axioms O+ in ALCH that compensate for the removed axioms. Os and Ow are in ALCH and are classified by MR producing Hw and Hs, correspondingly. Hw, Ho and Hs are classification results of Ow, Oo and Os, respectively. Subsumptions in Hw are sound but may not be complete w.r.t Oo, whereas subsumptions in Hs are complete but may not be sound. Unsound subsumptions in Hsn Hw are detected by AR and filtered out. Those that remain are added to Hw resulting in the sound and complete classification of Oo. We call this approach weakening and strengthening (WS).
We have implemented a prototype WSClassifier by applying the proposed WS
approach and evaluated it. Our previous study on WS approach and application to
ALCH OI ontologies [
The rest of the paper is organized as follows: Section 2 gives an overview of our hybrid classification procedure for ALCH O ontologies and prove its completeness. Section 3 introduces computation of strengthening axioms and Section 4 contains the related work. Section 5 is our partial empirical results and conclusion. Finally, we put all the proofs of lemmas and theorems in Appendix B and complete evaluation in Appendix C. 2
The syntax and semantics of ALCH O follows DL conventions. In this paper, we use A; B; E; F for atomic concepts, C; D for concepts, R; S for roles, a; b for individuals, H; K for conjunctions of atomic concepts, and M; N for disjunctions.
Algorithm 1 describes our hybrid procedure for classifying Oo. It consists of three stages: (1) a normalization stage (line 1) during which the ontology is rewritten to simplify the forms of axioms in it; (2) a main classification stage (lines 2 to 8) in which Ow and Os are generated and classified using the MR; and (3) a verification stage (lines 9 to 17) in which the subsumptions arising from just the Os are verified using AR. We use notations C and Co to denote the set of atomic concepts in Oo before and after normalization, respectively, and C>;? = C [ f>; ?g.
In the normalization stage, the ALCH O ontology Oo is rewritten to contain only
axioms of forms d Ai v F B j, A v 9R:B, 9R:A v B, A v 8R:B, R v S , or Na fag.
The procedure extends normalization in Frantisˇek et al. [
In the verification stage, there are some cases we hand over the classification work
to AR: (1) Na v ? 2 Hs; (2) E v ? 2 Hs but Oo 6j= E v ?, then for every F 2 C>;?,
E v F 2 Hs, while likely only few of them are in Hw, thus Hs n Hw may be huge; (3)
the fraction k Hs n Hw k = k C k is greater than a threshold d. In the latter two cases,
Algorithm 1: HybridClassify(Oo)
the estimated work for the stage is more than using AR to classify Oo. For (3) we set
d = 1:5 in our implementation based on the experiments in [
In the main classification stage, the major work is to generate the ALCH ontologies Ow and Os. Ow is produced by simply removing all the nominal axioms of the form Na fag from Oo. Since Ow Oo, Oo j= Ow and so Hw Ho, i.e. the classification result of Ow is sound w.r.t. Oo.
Example 1. Consider the following normalized ontology Oo;ex which we will use as a running example: (1) A v C (5) D v G (2) A v 9R:E (3) E v Na
(4) C v 8R:D (6) A v 9S :Na (7) N:a::::f:g (8) 9S :D v F a Classification result of Oo;ex is Ho;ex = fA v F; A v C; E v Na; D v Gg, where A v F is implied by axioms (1) – (4),(6) – (8). The weakened version Ow;ex of Oo;ex is obtained by removing nominal axiom (7). And its classification result Hw;ex = fA v C; E v Na; D v Gg. We can see that A v F, which requires (7) to imply, is missing in Hw;ex. We will see later how we add strengthening axioms to get A v F in Hs;ex.
The most di cult part of the procedure is to find Os which entails no fewer subsumptions than Oo. A su cient condition is that for any A; B 2 C>;? such that Os 6j= A v B, there exists a model I of Os satisfying A u :B, and it can be transformed to a model I0 of Oo satisfying A u :B. Since Os is obtained from Ow by adding strengthening axioms, every model I of Os satisfies all axioms in Oo except possibly the nominal axioms, which require the interpretation of each Na 2 NP to have exactly one instance, whereas for an arbitrary model I of Os, NaI could have zero or multiple instances. However, if for each Na, NaI , ; and all the instances are “identical”, they can be replaced by a single instance. Concretely, these instance have the same label set: Definition 1 Given an interpretation I = (4I; I), an atomic concept A is called a label of an instance x if x 2 AI. The set of all the labels of x is named the label set of x in I, denoted by LS (x; I).
Such a replacement is called a condensation – it condenses all of the di erent instances into one instance, and thus it transforms I into a model that satisfies the nominal axiom for Na. If such a condensation can be done for all nominal placeholders, then we can create a model for Oo.
The strengthening axioms are designed to make these condensations possible. They have the form Na v X and Na u X v ? computed by Algorithm 4, and thus they force X to be a label of the nominal instance Na, or not to be one, respectively. By “manipulating” labels of nominal instances through these strengthening axioms, we can force them all to be identical in certain models, so that the condensations can occur.
The models we construct for transformation are variants of the canonical model
constructed for ALCH ontologies [
Due to space limitation, we only list the important definitions, lemmas, property and theorems in the paper, all their proofs are in Appendix B. Here we briefly introduce some notations used later. We write O+ for any intermediate (including final) version of strengthening axioms, O+w for the corresponding intermediate (including final) version of strengthened ontology where O+w = Ow [ O+. We write Os for the final version of strengthened ontology. Given E; F 2 C>;? such that O+w 6j= E v F, a canonical model I[O+w; F] of O+w is constructed by first computing a saturation SO+w of O+w and then defining a model based on a total order F . The definition of construction of the canonical model is in Appendix A. The computation of saturation is as follows: Given O+w, the saturation SO+w is initialized as
finit(A) j A 2 Cg [ finit(Na) j Na 2 NPg
Then SO+w is expanded by iteratively applying the inference rules in Table 1 and adding
the conclusions into SO+w until reaching a fixpoint. During this process, existing axioms
in SO+w are used as premises and axioms in O+w are used as side conditions. SO+w contains
axioms of the forms init(H), H v M t A and H v M t 9R:K. Note Table 1 is modified
from Table 3 in [
Definition 3 Given a model I of an ALCH O ontology O, a concept L in O and an individual name xL, we define a condensation function condense(L; xL; I) that transforms I into an interpretation I0 = (4I0 ; I0 ) as follows: 1). Let n be a fresh instance which is not in 4I, and r be a replacement function x 2 LI otherwise r(x) = <>>8 n
>>: x 2). 4I0 = fr(x) j x 2 4Ig 3). For each concept A, role R and individual o in O, AI0 = fr(x) j x 2 AIg; RI0 = f(r(x); r(y)) j (x; y) 2 RIg; oI0 = r(oI); xIL0 = n We say that each x 2 LI is condensed into n. We also say I is condensed to I0.
in O+w if either X or :X is a conjunct of a potentially supporting context H of A in Ow. + The set of all PS of A in O+w is denoted by PS[A;O+w].
Example 2. (PS) Consider the ALCH ontology Ow;ex in Example 1, it can be seen as an ontology Ow;ex where Oe+x = ;, and NP = fNag. The potentially supporting contexts + of Na are Na; E and E u D. So PS[Na;Ow;ex] = fNa; D; Eg.
Property 6 We say O+w is decisive if for each Na 2 NP, each X 2 PS[Na;O+w], either O+w j= Na v X or O+w j= Na u X v ? holds.
Lemma 8 Let I be a model of an ALCH O ontology O satisfying E u :F; E; F 2 C>;?, where L is a condensing label in I. Then I0 = condense(L; xL; I) is a model of O[fL = fxLgg satisfying E u : F.
Lemma 9 Given some O+w and F 2 C>;?, if in I[O+w; F] every Na 2 NP is a condensing label, then for each E 2 C>;? s.t. O+w 6j= E v F, there is a model of Oo satisfying E u :F. Theorem 10 If the O+w we compute satisfies: (1) O+w is decisive and (2) all Na 2 NP are satisfiable in O+w. Then the classification result of O+w is complete w.r.t. Oo. Proof. Let E; F 2 C>;? be concepts such that O+w 6j= E v F. Since conditions (1) and (2) of Lemma 7 are satisfied, all Na 2 NP are condensing labels in the canonical model I[O+w; F]. By Lemma 9, the model can be condensed to a model I0 of Oo for E u :F, proving Oo 6j= E v F. So the classification result of O+w is complete w.r.t. Oo.
In the next section, we demonstrate how we will compute an O+w satisfying condition (1) in Theorem 10 i.e., is decisive. Such an O+w can also satisfy condition (2) in most cases as in our experiments, therefore completeness is achieved. If in a few cases that such an O+w ends up not satisfying condition (2), then we hand over the work to AR. The classification result is still complete. 3
In this section we show how to create a decisive O+w. The property suggests that the strengthening axioms should be of the form Na v X or Na u X v ?. We first briefly introduce the strengthening axioms selection function chooseStrAxiom. Based on that, we explain an initial idea to create a decisive O+w. Then, we introduce how to compute OPS[Na;O+w] which is an overestimation of PS[Na;O+w] from O+w without doing saturation, and give the naive and improved algorithms to compute O+.
Definition 11 A strengthening axiom selection chooseStrAxiom is a function that takes an Na 2 NP, X 2 Co, and Ow and returns: 1. ; only if Ow j= Na v X or Ow j= Na u X v ?; 2. a choice between Na v X or Na u X v ?.
Initial idea for computing a decisive O+w: To create such an ontology, a straightforward idea is to start from Ow, generate saturation SOw of Ow, obtain PS[Na;Ow] from SOw for all Na 2 NP. For each pair hNa; Xi, X 2 PS[Na;Ow], we add a strengthening axiom determined by chooseStrAxiom function into O1+. Then, add O1+ into Ow and obtain O1w+. Next, we generate saturation again based on O1w+. Since the impact of O1+, PS[Na;O1w+] PS[Na;Ow]. Then we repeat the above process until a fixpoint at which PS[Na;Oiw+1+] = PS[Na;Oiw+] for all Na 2 NP, we call the final Oi+1+ as O+, final Oiw+1+ as Os which is decisive. However to implement such a procedure generating the saturation for PS[Na;O+w] is costly. Thus, instead of PS[Na;O+w], we compute the overestimated PS[Na;O+w] called OPS[Na;O+w].
supporting concepts we compute such that OPS[Na;O+w] PS[Na;O+w] for each Na 2 NP.
We use Algorithm 2 to compute OPS[X;O+w]. Based on Definition 4 and 5, PS[X;O+w] includes all the atoms of H such that H v M t X 2 SO+w . Without a real procedure generating the saturation for PS[X;O+w] as explained above, we actually compute OPS[X;O+w] based on analyzing the relationships among the premises, side conditions and conclusions of the inference rules in Table 1. The procedure of Algorithm 2 can be divided into three parts: 1. (line 2 to 9) We first conduct a search in the converse direction of all possible derivation paths(Definition 16 in Appendix B) of a conclusion H v M t X for all possible Hs. In the search we maintain a set Pri[X;O+w]. Each concept W 2 Pri[X;O+w] may be necessary to the derivation of X, and appears prior to X in the derivation path. More precisely, W corresponds to some potential intermediate conclusion H v M0 t W which is a necessary conclusion for deriving H v M t X. Since for any context H, H v A is the only conclusion that can be derived from init(H), at least one of such A, which is a conjunct of H, is in Pri[X;O+w]. We write CHX for such A. Pri[X;O+w] contains at least one conjunct CHX for any potentially supporting context H of X. 2. (lines 10 to 13) Check each concept W 2 Pri[X;O+w] to see whether it can be a conjunct CHX of some potential supporting context H of X. If it can, we find the first conjunct CH1 of H from CX . CH1 (see H in Lemma 13 in Appendix B), which is either in U
H or NP in line 11 or the filler of concepts in Exists from line 12 to 13, is the initial concept H starts from. 3. (line 14 to 17) Find all the other conjuncts of H based on CH1 by searching along the derivation paths.
OPS[A;O+w]
PS[A;O+w].
Lemma 13 Given O+w and a concept A, OPS[A;O+w] returned by Algorithm 2 preserves Example 3. (OPS) Consider again the ontology Ow;ex in Example 1.
The Execution of Alg. 2: getOPS(Ow;ex; Na; fNag; fA; C; D; E; F; Gg) Line 2 to 9 Line 11 Line 13 Line 16 Line 18
Pri[Na;Ow;ex] = fNa; Eg OPS[Na;Ow;ex] = fNa; Eg Exists = f9R:Eg OPS[Na;Ow;ex] = fNa; E; Dg
Return OPS[Na;Ow;ex] = fNa; E; Dg, Pri[Na;Ow;ex] = fNa; Eg OPS[Na;Ow;ex] = PS[Na;Ow;ex] = fNa; E; Dg so OPS[Na;Ow;ex] PS[Na;Ow;ex] For each X 2 OPS[X;Oiw+], we will use function chooseStrAxiom to return a strengthening axiom. Note in Definition 11 for chooseStrAxiom, how can we know Ow j= Na v X or Ow j= Na u X v ?? Actually in Algorithm 1, line 4 (we used getNominalStrAx, if using getNominalStrAxNaive, it is the same) executes getOPS(Ow; Na; NP; U) internally before line 3. Then for each Na 2 NP, each X 2 OPS[Na;Ow], we add a testing axiom Xa v Na u X into Ow in the first round classification and obtain Hw, where Xa is a fresh concept for Ow. In Algorithm 1 and Definition 11, we ignore this detail and only mention using Ow just for simplifying explanation. If Xa v ? is found in Hw, then we simply say Ow j= Na u X v ?. If Na v X or Na u X v ? is implied by Hw, we do not add any strengthening axiom for X into Oi+1+. We remove the extra testing results from Hw in line 5 of Algorithm 1. When choosing between Na v X and Na u X v ?, we use the heuristics that if X corresponds to a union concept before normalization, and Na v X is not implied, then we add Na u X v ?. For other cases, we add Na v X. Example 4. For the concepts in OPS[Na;Ow;ex], since none of the 4 axioms Na v E, Ea v ?, Na v D or Da v ? is in Hw;ex, and assume E and D do not associate union concepts before normalization, we add Na v E and Na v D as strengthening axioms O1ex+.
Using OPS[X;O+w] instead of PS[X;O+w], we design a naive Algorithm 3 based on the above Initial Idea to generate O+ for O+w so that O+w is decisive. The execution process is as follows: 1). O0+ = ;. 2). Compute OPS[Na;Oiw+] for 8Na; Na 2 NP for the Oi+. 3). Oi+1+ = fchooseStrAxiom(Na; X) j 8Na; X; Na 2 NP; X 2 OPS[Na;Oiw+]g In each loop, we add the new Oi+ into Ow and generate Oiw+. When the process converges, Oi+1+ = Oi+. Since Oi+1+ is computed from OPS[Na;Oiw+], and OPS[Na;Oiw+] PS[Na;Oiw+] for all Na and for any i, thus Algorithm 3 guarantees that O+w is decisive. Theorem 14 Let O+ be strengthening axiom produced from Algorithm 3, O+w = Ow [O+ is decisive. Algorithm 3: getNominalStrAxNaive (Naive algorithm for computing strengthening axioms) Theorem 15 Let O+ be strengthening axioms computed from Algorithm 4, O+w = Ow [ O+ is decisive.(Proof see Appendix B, the following is just an intuitive explanation) Algorithm 4 improves Algorithm 3 by avoiding repetitive search process. In each loop of Algorithm 3, Algorithm 2 getOPS bases on the axioms of the input Oiw+1+ to compute OPS[Na;Oiw+1+] for Na, where only search on Oiw+1+ n Oiw+ is new, the majority work – search on Ow is repeated in each iteration, while Algorithm 4 improves this and only executes getOPS based on Ow for once in line 3. In Algorithm 2 and 3, a strengthening axiom can take e ect only in the following situation: If = fNb v Xg 2 Oiw+, X 2 Pri[Na;Oiw+], then Nb 2 OPS[Na;Oiw+]. If chooseStrAxiom(Na; Nb) return Na v Nb in Oiw+1, then Na 2 OPS[Nb;Oiw+1+]. That means because of , in the end, OPS[Na;O+w] = OPS[Nb;O+w]. In Algorithm 4, without really computing each of Oiw+ and repeatedly search on them, we achieve similar results based on the merge criteria in line 6 and the merge operation from lines 7 to line 7. Assume Nb 2 gi:nominals and Na 2 g j:nominals, X 2 gi:ops \ g j:pri , ; in line 6. Then, X 2 gi:ops means Nb v X will possibly be a strengthening axiom, X 2 g j:pri means X is possibly in Na’s Pri, then gi and g j are merged into one group, and finally OPS[Na;O+w] = OPS[Nb;O+w], too, similar with Algorithm 3.
Example 5. In Algorithm 3, Oe1x+ = Oe2x+. Thus, the loop from line 2 to 9 repeats twice. In Algorithm 4, since NP = fNag, the merge process from line 6 to 7 does not happen. For both algorithms, that means Oe1x+ does not have impact in later saturation.
Note the naive Algorithm 3 is only used for demonstrating our initial idea. In our
implementation, we used the improved Algorithm 4. All three Algorithms 2, 3 and 4
have polynominal complexity. In Algorithm 2, the number of iterations in all levels of
loops are bounded by the number of axioms or concepts in Ow, and thus have
polynomial complexity. In Algorithm 3, the number of iterations is bounded by the size of O+,
which is also polynomial. In Algorithm 4, the merge loop can only continue for at most
jjNPjj times. So all the algorithms are polynomial of the size of Ow and terminate.
Algorithm 4: getNominalStrAx (Calculate strengthening axioms for nominals)
Optimization techniques for ontology classification have been extensively studied in
the literature [
In the area of hybrid reasoning, Romero et al. [
Our approach generally belongs to theory approximation [
We have implemented our prototype hybrid classifier WSClassifier in Java. The
classifier uses ConDOR as the main ALCH reasoner and HermiT as the assistant reasoner
for DL ALCH O. WSClassifier adopts a well-known preprocessing step to eliminate
transitive roles [
We have presented a hybrid reasoning technique for soundly and completely classifying an ALCH O ontology based on a weakening and strengthening approach. The input ontology is approximated by two ALCH ontologies, one weakened Ow and one strengthened Os, which are classified by a fast consequence-based reasoner. The subsumptions of Ow and Os are a subset and a superset of the subsumptions of the original ontology, respectively. Subsumptions implied by Os but not by Ow are further checked by a (slower) ALCH O reasoner. This approach is possibly applied to di erent language classes, each requiring di erent strengthening axioms. The implementation can be improved with heuristics for a tighter OPS[Na;O+w] and better strengthening axioms.
Given F 2 C>;? and O+w, our target is to construct a model I[O+w; F ] for O+w satisfying E u :F for any E 2 C>;? such that O+w 6j= E v F. We write I for I[O+w; F ] when the parameters are not important. The construction is done by first computing a saturation SO+w of O+w and then defining a model based on it. SO+w contains axioms of the forms init(H), H v M t A and H v M t 9R:K derived using the inference rules. (1) Computation of saturation
Given an ALCH ontology O+w, the saturation SO+w is initialized as
finit(A) j A 2 C>g [ finit(Na) j Na 2 NPg Then SO+w is expanded by iteratively applying the inference rules in Table 1 and adding the conclusions into SO+w until reaching a fixpoint. An inference rule is applied by using existing axioms in SO+w as premises and axioms in O+w as side conditions. We write O+w ` for every 2 SO+w derived from O+w. The inference process is obviously sound, i.e. if O+w ` then O+w j= . (2) Model construction
We define a total order F over all the concepts in O+w such that F has the least order. If F is ? or >, the order can be any arbitrary order. We define the domain 4I of I[O+w; F] as
4I := fxH j init(H) 2 SO+w and H v ? < SO+w g where xH is an instance introduced for H. 4I is nonempty because if O+w is consistent, > v ? < SO+w . Since init(>) 2 SO+w , x> exists.
To define the interpretation for atomic concepts, we first construct the label set LS (xH; I) for each instance xH. In this section, we write IH for LS (xH; I). Let Ai be the concept with the ith order from the smallest to the largest according to F . For convenience we write M F Ai if for each disjunct A in M, A F Ai. Let IiH be a sequence where I0H := ;, and IiH is defined as
>>>8 IiH [ fAig if there exists M IiH := <>>> O+w ` H v M t Ai and M \ IiH 1 = ; > >:>> IiH 1 otherwise
F Ai such that The last element of the sequence is defined as LS (xH; I). With the LS (xH; I) defined, the interpretation of an atomic concept A is defined as
AI := fxH j A 2 LS (xH; I)g The roles are interpreted to satisfy the axioms H v M t 9R:K. For each role R and each H such that xH 2 4I, define
IRH := fK j 9M : O+w ` H v M t 9R:K; M \ IH = ;g A conjunction K is said to be maximal in LS R(xH; I) if there is no K0 2 IRH with a superset of conjuncts of K. Since H v ? < SO+w , by R? rule we have K v ? < SO+w . 9 And by Rinit rule we have init(K) 2 SO+w . So xK is well-defined. The interpretation of roles is defined as
RI :=
[ f(xH; xK ) j K is maximal in IRH0 g
R0vO+w R
The inference rules in Table 1 is modified from Table 3 in [
+ Since F has the least order in F , by the definition of LS (xE; I) we know xE < FI. Thus xE 2 (E u :F)I, and I[O+w; F] satisfies E u :F.
B
Lemma 7 Given O+w and Na 2 NP, if (1) O+w is decisive, and (2) O+w 6j= Na v ?. Then for any F 2 C>;?, Na is a condensing label in I[O+w; F].
Proof. For simplicity we write I for I[O+w; F] in this proof. Since init(Na) 2 SO+w and O+w 6j= Na v ?, by the construction of I, xNa exists and xNa 2 NaI. Hence it is equivalent to show that for each xH 2 NI, LS (xH; I) = LS (xNa ; I).
a
We first show that for each H such that xH 2 NI, xNa 2 HI. Since xH 2 NI, H is a
potentially supporting context of Na. Let H = din=1 aCHi, where CHi is A or :A. Saince O+w
is decisive, we have the following two cases:
– O+w j= Na v CHi holds for all CHi; 1 i n, then O+w j= Na v H. Since xNa 2 NaI,
xNa 2 HI.
– There exists some i such that O+w j= Na u CHi v ?, then O+w j= Na u H v ?. By
Lemma 3 of paper [
Next we prove LS (xNa ; I) LS (xH; I) by contradiction. Assume LS (xNa ; I) * LS (xH; I), let X be the concept in LS (xNa ; I) n LS (xH; I) with the smallest order. Since X 2 LS (xNa ; I), there exists N F X such that O+w ` Na v N tX and N \LS (xNa ; I) = ;. * Ow ` Na v N t X ) O+w j= Na v N t X
+ * xH 2 NaI ^ xH < XI ) xH 2 NI ) LS (xH; I) \ N , ; In the above proof, if N = ?, a contradiction arises with xH 2 NI. Otherwise, let Y 2 + LS (xH; I) \ N, there must exist N0 F Y s.t. Ow ` H v N0 t Y and LS (xH; I) \ N0 = ;.
+ * Ow ` H v N0 t Y and xNa 2 HI ) xNa 2 (N0 t Y)I * N0 F Y and Y 2 N and N
F X ) N0 F X Since X is the smallest in LS (xNa ; I) n LS (xH; I), N0 F X and LS (xH; I) \ N0 = ;, we have LS (xNa ; I) \ N0 = ; (it is trivially true if N0 = ?), and xNa < N0I. Given xNa 2 (N0 t Y)I, we have Y 2 LS (xNa ; I), this contradicts with N \ LS (xNa ; I) = ;. So we conclude that LS (xNa ; I) n LS (xH; I) = ; and LS (xNa ; I) LS (xH; I).
Finally we need to prove LS (xH; I) LS (xNa ; I). For each X 2 LS (xH; I), there exists N F X such that O+w ` H v N t X and N \ LS (xH; I) = ;.
* LS (xNa ; I)
LS (xH; I) ) N \ LS (xNa ; I) = ; ) xNa < NI Thus we conclude X 2 LS (xNa ; I).
Lemma 8 Let I be a model of an ALCH O ontology O satisfying Eu:F; andE; F 2 C>;?, where L is a condensing label in I. Then I0 = condense(L; xL; I) is a model of O [ fL fxLgg satisfying E u :F.
Proof. By the definition of condensing label, we have: (1) LI , ;; (2) for all x 2 LI, LS (x; I) are the same. By (1) and the definition of r in condense(L; xL; I), we have LI0 = fxIL0 g, so the axiom L fxLg is satisfied. By (2), we can further prove LS (x; I) = LS (r(x); I0) holds for all x 2 4I. Next we need to prove I0 j= from I j= for any axiom in O. We do a case-by-case analysis for every possible form of : – – – – – –
= d Ai v F B j Assume x0 2 (d Ai)I0 , there exists x 2 4I s.t. x0 = r(x). Since LS (x; I) = LS (x0; I0), we have x 2 \iAiI, so x 2 [ jB Ij. Hence x0 2 (F B j)I0 .
= A v 9R:B Assume x0 2 AI0 , there exists x such that x0 = r(x) and x 2 AI. Since I j= , there exists y 2 4I s.t. (x; y) 2 RI and y 2 BI. So (x0; r(y)) 2 RI0 and r(y) 2 BI0 . Hence x0 2 (9R:B)I0 .
= 9R:A v B Assume x0 2 (9R:A)I0 , there exists y0 such that (x0; y0) 2 RI0 and y0 2 AI0 . So there exists (x; y) 2 RI s.t. x0 = r(x) and y0 = r(y). Since r(y) 2 AI0 , y 2 AI. Because I j= , x 2 BI and thus x0 2 BI0 .
= A v 8R:B Assume x0; y0 2 4I0 s.t. (x0; y0) 2 RI0 and x0 2 AI0 , there exists x; y 2 4I s.t. x0 = r(x), y0 = r(y) and (x; y) 2 RI. Since LS (x; I) = LS (x0; I0), we have x 2 AI. Because I j= , y 2 BI, hence y0 2 BI0 .
= Na fag By I j= we have NaI = faIg. According to the definition of the function condense() we have NI0 = fr(aI)g = faI0 g.
a = R v S If (x0; y0) 2 RI0 , there exists x; y 2 4I s.t. x0 = r(x), y0 = r(y) and (x; y) 2 RI. Since I j= , (x; y) 2 S I and so (x0; y0) 2 S I0 .
So I0 j= O [ fL = fxLgg holds. Assume x 2 (E u :F)I, since LS (x; I) = LS (r(x); I0) we know r(x) 2 (E u :F)I0 , so (E u :F)I0 , ;.
Lemma 9 Given some O+w and F 2 C>;?, if in I[O+w; F] every Na 2 NP is a condensing label, then for each E 2 C>;? s.t. O+w 6j= E v F, there is a model of Oo satisfying E u :F. Proof. Let fLi fxLi ggin=1 be all nominal axioms in Oo. We prove I[O+w; F], which satisfies E u :F for each non-subclass E 2 C>;? of F, can be transformed to a model In of On = O+w [ fLi fxLi ggin=1 such that (E u :F)In , ; by induction on n.
By assumption for n = 0, I0 = I[O+w; F]. We need to show a model Ik of Ok satisfying E u :F can be transformed to a model Ik+1 of Ok+1 satisfying E u :F. This step is proved by applying Lemma 8 where I = Ik, O = Ok, L = Lk and xL = xLk .
Then we have transformed the model I[O+w; F] to a model In of On satisfying E u :F where kNPk = n. Since On Oo, we have In j= Oo and (E u :F)In , ;. Definition 16 In a saturation SO+w , the derivation path of a conclusion of the form H v M or H v N t 9R:K is the sequence of all the inference steps IS1H; : : : ; ISHm in the context H, where: (1) 2 ISHm:conc, and (2) for any n < m, ISnH occurs before ISnH+1 in the saturation process. Lemma 17 Given O+w, a concept A 2 C, and an axiom 2 SO+w of the form H v M t A or H v M t A t 9R:K, then there exists a conjunct B of H such that B 2 Pri[A;O+w]. Proof. According to line 1 and 5 of Algorithm 2, A 2 Pri[A;O+w]. Let IS1H; : : : ; ISHm be the derivation path of . We prove the lemma by induction over m.
If m = 1, then IS1H:rule is R+A, and by the side condition of R+ , A is a conjunct of A H. So the lemma holds where B = A 2 Pri[A;O+w]. Next we show the lemma holds when m = k, if it holds for all m < k. Since 2 SO+w , there must exist some step ISpH such that A is a disjunct of the axiom in the conclusion but not in the premise. In this case, ISpH:rule can only be R+A, Rn or R , so we can perform a case analysis as follows.
u 9 Case 1 Similarly to the case m = 1, we can choose B = A to prove the lemma. Case 2 ISpH:rule=Rnu In this case ISpH:sc has a single axiom of the form d Ai v F B j.
By line 7 there exists some Ai s.t. Ai 2 Pri[A;O+w]. Since H v Ni t Ai 2 ISpH:prem, its derivation path IS1H; : : : ; ISpH0 must satisfy p0 < p k. By applying the inductive hypothesis to m = p0 and H v Ni t Ai, there exists H’s conjunct B s.t. B 2 Pri[Ai;O+w]. Since Ai 2 Pri[A;O+w], according to the Algorithm 2, we can see that Pri[Ai;O+w] Pri[A;O+w]. So B 2 Pri[A;pO+w], and the lemma is proved.
Case 3 ISpH:rule=R9 In this case ISH:sc has axioms of the forms R vO S and 9S :Y v A, and one of the premises ISpH:prem is of the form H v M0 t 9R:(din=1 CKi0 ), which is derived by the process:
R+ H v M1tA0 A0v9R9:CK!10 H v M1 t 9R:CK10
R8=R9 RvOS Yv8S:Z=9S:Zv!Y H v M0 t 9R:(l CKi0 ) i=1 The first inference step has a side condition of the form A0 v 9R:CK10 and a premise of the form H v M1 t A0. By line 8 to 9, A0 is added to Pri[A;O+w] where W = A and Z = CK10 . Let IS1H; : : : ; ISpH0 be the derivation path of H v M1 t A0. We can see p0 < k since H v M1 t A0 must be derived before the kth step. By the inductive hypothesis, there exists H’s conjunct B s.t. B 2 Pri[A0;O+w]. Since A0 2 Pri[A;O+w], Pri[A0;O+w] Pri[A;O+w]. So B 2 Pri[A;O+w], and the lemma is proved.
Lemma 13 Given O+w and a concept A, OPS[A;O+w] returned by Algorithm 2 preserves OPS[A;O+w] PS[A;O+w].
Proof. By Lemma 17, we have shown that there is at least one conjunct B of H in Pri[A;O+w]. Since H’s conjuncts are all collected during the derivation of init(H), we discuss the two cases how init(H) is derived, and how H’s conjuncts are added in each case: – If init(H) is introduced at initialization stage, then B is the only conjunct in H belonging to C>;? or NP, and is added to OPS[A;O+w] in line 11 of Algorithm 2 where W = B and U = C>;?. – If init(H) is introduced by Rinit rule, then there is a premise of the form H v M t 9R:H, where H is a context di erent from H. Let H = dn i=1 CHi, the derivation process of H v M t 9R:H is: n n H v M1tA
R+
9 ! H v M1 t 9R:CH1 Av9R:CH1
R8=R9 RvOS Yv8S:Z=9S:Zv!Y H v M t 9R:(l CHi) i=1 The side condition of the first step is A v 9R:CH1. We first prove 9R:CH1 2 Exists, where Exists is the set produced in the loop from lines 10 to 13. If B is CH1, then 9R:CH1 is added to Exists in line 13 where W = B. If B is a conjunct of H other than CH1, then B becomes a conjunct after an application of R8 rule, in such case the side condition is R v S and Y v 8S :B, so 9R:CH1 is added to Exists in line 12 where W = B. O Next we show the lemma holds for all three types of conjuncts C of H: 1. If C is added to the conjuncts of H by R+ rule, then C = CH1 and is added to 9
OPS[A;O+w] in line 15. 2. If C is added to the conjuncts of H by R8 rule, then C is added to OPS[A;O+w] in line 16. 3. If C is added to the conjuncts of H by R9 rule, then C is of the form :Z, and Z is added to OPS[A;O+w] in line 17.
Hence the lemma is proved.
Theorem 14 Let O+ be strengthening axioms computed from Algorithm 3, the ontology O+w = Ow [ O+ is decisive.
Proof. Since in the last round of the loop On+ = On 1+, we know that for each Na 2 NP and X 2 OPS[Na;Onw+] = OPS[Na;Onw 1+], chooseStrAxiom(Na; X) On+ Onw+. And because PS[Na;Onw+] OPS[Na;Onw+], thus O+w = Onw+ is decisive.
Theorem 15 Let O+ be strengthening axioms computed from Algorithm 4, the ontology O+w = Ow [ O+ is decisive.
Proof. For each Na 2 NP, we write gNa for the final group that Na belongs to after executing lines 6 to 7 of Algorithm 4. We will prove that OPS[Na;O+w] gNa :ops. From lines 10 to 17 of Algorithm 2, we can see that each concept X is added to OPS[Na;O+w] because of some W 2 Pri[Na;O+w] in line 10, for which we write WX. And according to the loop in lines 2 to 9, WX is added to Pri[Na;O+w] through a search path Na = W0 ! W1 ! : : : Wn = WX, where Wi 1 ! Wi; 1 i n represents Wi is added to ToProcess while processing Wi 1 in the loop where W = Wi 1. Note that in Algorithm 2, the only case that a strengthening axiom 2 O+ is used is when is of the form Nb v X0 and used in line 7. Let W s be the set of Wi such that Wi is added into ToProcess from W = Wi 1 in line 7 using such a strengthening axiom = Nb v X0. We prove the lemma by induction over the size m = kW sk of W s. The inductive hypothesis is:
For each X 2 OPS[Na;O+w] and Na 2 NP, let WX 2 Pri[Na;O+w] be the concept that causes X to be added into OPS[Na;O+w], Na = W0 ! W1 ! : : : Wn = WX be the search path of WX, and W s0 be the set of Wi such that Wi 1 ! Wi uses a strengthening axiom. If kW s0 k < m then X 2 gNa :ops. – m = 0 In this case WX 2 Pri[Na;Ow] and X 2 OPS[Na;Ow]. By line 4 we see X is in the initial group of Na, and is merged into gNa :ops while executing lines 6 to 7. – m = k Let im = minfi j Wi 2 W sg. In this case we have Wim 1 = X0 and Wim = Nb.
It is easy to see that X is also added to OPS[Nb;O+w] through the same WX and a search path Nb = Wim ! : : : Wn = WX, whose kW s0 k is k 1. By applying the inductive hypothesis to X and Nb, we know X 2 gNb :ops. And since X0 2 Pri[Na;Ow], X0 2 gNa :pri. So gNa :pri \ gNb :ops , ;, and gNa and gNb must be the same group according to the merge criteria in line 6 of Algorithm 4. So X 2 gNb :ops = gNa :ops.
Hence PS[Na;O+w] OPS[Na;O+w] gNa :ops for each Na 2 NP in O+w. According to the construction of O+ in line 11 of Algorithm 4, we conclude O+w = Ow [ O+ is decisive. C
We have implemented our prototype hybrid reasoner WSClassifier in Java using OWL
API. The reasoner uses ConDOR r.12 as the main ALCH reasoner and HermiT 1.3.6
as the assistant reasoner for DL ALCH O. WSClassifier adopts a well-known
preprocessing step to eliminate transitive roles [
We evaluated WSClassifier and other reasoners on all large and complex ontologies
available to us, on the ORE dataset and on some proposed variants. The only large and
complex ontologies included are FMA-constitutionalPartForNS(FMA-C)1 and
modified versions of Galen in which some concepts starting with a lower case letter and
subsumed by SymbolicValueType are modeled as nominals. The ontologies
containing “EL” in the name are constructed based on Galen-EL2. Galen-EL-n1Y and
GalenEL-n2Y were provided [
For FMA-C which is the only real-world large and complex ontologies with nominals we have access to, WSClassifier finished classification in 21.2 seconds, while HermiT used 140,882 seconds. Other reasoners did not finish classification on it in 9 days. From the results of Table 2 we can see, excluding ORE dataset, WSClassifier is significantly faster than the tableau-based reasoners on 7 out of 10 ontologies. For the 1 Foundational Model of Anatomy, http://sig.biostr.washington.edu/projects/fm/index.html 2 http://code.google.com/p/condor-reasoner/downloads/list 3 http://www.cs.ox.ac.uk/isg/conferences/ORE2012/ 4 http://isel.cs.unb.ca/~wsong/WSClassifierExperimentOntologies.zip Ontology
Wine
DOLCE Galen-Heart-n1 Galen-Heart-n2 Galen-EL-n1Y Galen-EL-n2Y Galen-EL-n1YE Galen-EL-n2YE Galen-Union-n
FMA-C
FMA-lite remaining 112 ontologies 146 207 3366 3366 23136 23136 23136 23136 23136 41648 75,141 4293 (Hyper) tableau
Hybrid
HermiT Pellet FaCT++ MORe WSClassifier
ORE-dataset (OWL DL & EL,113 ontologies) the following refers to average number Note: The time is measured in seconds. “–” means out of time or memory
: Fact++ terminates unexpectedly while classifying some ontologies in the ORE-dataset other 3 of 10 ontologies – Wine, Galen-EL-YN1 and Galen-EL-YN2, WSClassifier, incurring a relatively small cost, detected that strengthening axioms made some concepts unsatisfiable in Os, and so failed over to HermiT.
We see a major speedup for WSClassifier on ORE’s FMA-lite. On the remaining 112 ORE ontologies, our average reasoning time is longer than other reasoners. Among these ontologies, 51 have nominals, mostly coming from ABoxes, and only 9 of them have strengthening axioms. Of the 9 ontologies, 8 did not produce any new subsumptions in Hs and only 1 which is the variant of Wine ontology introduced new unsatisfiable concepts and fails over to HermiT. Thus the WS approach does not incur much additional work, and most of the additional time is taken on overheads: computing normalized and strengthening axioms, and transmitting the ontology to and from ConDOR, which is necessary since ConDOR cannot be accessed directly through OWL API and consumes about 60% of the time.
WSClassifier outperforms MORe on DOLCE and all the Galen ontologies. For the Galen ontologies, MORe assigns all the classification work to a default configured HermiT; fine-tuning may improve its times. However, MORe computes only subsumptions implied by the TBox, ignoring the ABox, thus its classification result is incomplete for some ontologies with ABoxes, such as Wine.
WSClassifier seems most applicable when the ontologies are large and highly cyclic since then tableau reasoners construct large models and employ expensive blocking strategies. On the other hand consequence-based reasoners do not encounter problems on highly cyclic ontologies, and so can classify even cyclic Ow and Os quickly. If there are no or just a few additional subsumptions derived by Os, AR does not need or just do a little work on the highly cyclic Oo. This improvement is observed for FMA-C which is the only real-world large and complex ontology with nominals we have access to.