We study a restriction of the classification procedure for EL++ where the inference rule for complex role inclusion axioms (RIAs) is applied in a “left-linear” way in analogy with the well-known procedure for computing the transitive closure of a binary relation. We introduce a notion of left-admissibility for a set of RIAs, which specifies when a subset of RIAs can be used in a left-linear way without loosing consequences, prove a criterion which can be used to effectively check this property, and describe some preliminary experimental results analyzing when the restricted procedure can give practical improvements.
The description logic (DL) E L and its extension E L++ [1] provide the bases of the OWL EL profile of the Web Ontology Language [6] and are distinguished by having tractable worst-case complexity for the standard DL reasoning problems. The nice computational properties of E L-style reasoning procedures such as optimal (polynomial) worst-case complexity and “pay-as-you-go” behavior, are commonly mentioned as main reasons for the improved practical performance of reasoners based on such procedures for large ontologies such as SNOMED CT [2,5,3,8].
Although E L++ admits a polynomial reasoning procedure, different features of E L++ contribute differently to the degree of this polynomial [4]. In particular, the E L++ rule for dealing with complex role inclusion axioms (RIAs) has O(n4) time complexity, which is higher than for other rules. Even for a single transitivity axiom, the rule can result in O(n3) inferences. Although complex role inclusion axioms are not used as commonly as other constructors in existing ontologies such as SNOMED CT, this might change in the future as more OWL EL ontologies emerge.
Inspired by an O(n2) algorithm for computing the transitive closure of a binary relation, in this paper we propose a refinement of the E L++ rule for dealing with complex RIAs. Our main idea is to restrict the rule so that inferences are applied in a left-linear way, that is, only a restricted number of the “initial” axioms can be used in all premises of the rule except for the left-most. To this end, we (i) formulate a notion of left-admissibility describing subsets of complex RIAs that can be used in a left-linear way without losing consequences, (ii) prove a criterion for left-admissibility that can be checked in polynomial time, and (iii) provide an experimental evaluation measuring the proportion of left-admissible RIAs and reduction in the number of inferences for a selection of commonly-used ontologies. C2 (CCvvCiD)in=1 : din=1 Ci v D 2 KB
n > 1 C3 CCvv9RC:0D : C0 v 9R:D 2 KB
C v 9R:D
C v E
D v D0 C5 CC vv 99RS::DD : S v R 2 KB
: 9R:D0 v E 2 KB
C6 (Ci C10vv99RRi::CCni)in=1 : nR1> :1: : Rn v R 2 KB 2
Reasoning in E LR We first introduce a basic classification calculus for the description logic E LR that will serve as a baseline for our study. E LR is the DL that supports only conjunction, existential role restrictions, role hierarchies, and role inclusion axioms, each of which can be used in arbitrary general concept inclusions and role inclusion axioms. We do not require regularity of RBoxes, and E LR can thus be viewed as a fragment of E L++ without top, bottom, nominals, and concrete domains. We use the following notation for role inclusion axioms. Definition 1. A role chain is an expression of the form R1 : : : Rn, n 0; when n = 0 then = is the empty role chain and when n 2 then is a complex role chain. We denote by 1 2 the concatenation of two role chains 1 and 2. A (complex) role inclusion axiom (short RIA) is an expression of the form v R where is a non-empty (complex) role chain and R a role. An RBox R is a finite set of RIAs.
Table 1 shows the rules of a classification calculus for E LR, obtained by restricting the calculus for E L++ [1]. The input to the rules are axioms from an E LR knowledge base that have been normalized as in [1]. The main difference is that we treat n-ary conjunctions/role chains in a single application of C2/C6, corresponding to the implementation we used for experiments. Each rule of inference consists of a premise, a conclusion, and possible side conditions. The calculus derives axioms of the form C v D and C v 9R:D based on an input knowledge base KB, and it is sound and complete for classification in the sense that an axiom C v D is entailed by KB if and only if the exhaustive application of the inference rules can be used to derive C v D. This follows immediately from the according result in [1] since it is easy to see that our rules correspond to the inference rules in that paper: C0 corresponds to the initialization, C1 to CR1, C2 to CR2, C3 to CR3, C4 to CR4, C5 to CR10, and C6 to CR11. 3
One of the simplest examples of complex RIAs is a transitivity axiom:
R R v R: Transitivity axioms occur in many ontologies where they are used to express hierarchical relations between concepts, such as “part-of” or “child-of” hierarchies. Let us consider an ontology containing axioms expressing a simple R-hierarchy: Ai v 9R:Aj
Aj v0 9R:Aj+1 :
i < j < n:
(
i < n: Ai v 9R:Aj ; 1 i < j n; using the following instances of rule C6:
Ai v 9R:Aj Aj v 9R:Ak :
Ai v 9R:Ak
1
i < j < k
n:
There are exactly n (n 1)=2 possible axioms of the form (
The inferences (
C1 v 9R:C2 C2 v0 9R:C3 : R R v R 2 KB:
C1 v 9R:C3
We will call the rule (
n > 1 L3 CCvv0LL9RC:0D : C0 v 9R:D 2 KB L4
C vL 9R:D D vL D0 : 9R:D0 v E 2 KB
C vL E L5 CC vvLL 99RS::DD : S v R 2 R
0 L05 CC vv0LL 99RS::DD : S v R 2 R L6 (Ci C10vvLL99RRi::CCni)in=1 : nR1> :1: : Rn v R 2 R n L
L06 C0 vL 9R1:CC10 v(LC9iR1:Cvn0L 9Ri:Ci)in=2 : nR1> :1: : Rn v R 2 L
It is easy to see that there are exactly (n 1) (n 2)=2 rule applications in (
We use the idea above to formulate a calculus for E LR with a restricted version of rule C6. In order to do that, we need to specify where the “initial” axioms C v0 9R:D come from. Clearly, we cannot take such axioms just from the knowledge base, since otherwise, e.g., we would not be able to derive A v 9R:D for KB consisting of A v 9R:B, B v C, C v 9R:D, and R R v R, as we cannot avoid using B v 9R:D in the second premise of C6. Similarly, we need to allow initial axioms to be produced by C5, since otherwise A v 9R:C cannot be derived for KB consisting of A v 9R:B, B v 9S:C, S v R, and R R v R.
The new calculus for E LR is formulated in Table 2. The calculus is parametrized with a distinguished subset L R of complex RIAs. The RIAs in L can, similar to the transitivity axiom in the example above, only be used in a left-linear version L06 of rule C6. The remaining axioms from R n L can be used without restrictions in rule L6. The initial axioms of the form C v0L 9R:D are produced by rules L3 and L05. We use L in the subscripts of vL and vL 0 to emphasize that these relations depend on L. We implicitly assume that v0L vL; in particular, axioms of the form C v0L 9R:D can also be used as premises of rules L4 and L6 and as the first premise of rule L06. Note that if L = ;, our new calculus coincides with the original calculus for E LR (ignoring the distinction between vL
0 and vL). Clearly, the larger L is, the more restricted our rules are, and so the less inferences are possible. Thus, in the remainder of the paper we are concerned with the problem of finding subsets L of a given R which do not result in lost consequences relative to the original calculus in Table 1. 4
In this section we are concerned with the problem of how to determine, given a set of complex RIAs L R, whether the calculus in Table 2 produces the same consequences as the original calculus in Table 1. In order to study the properties of the calculus in Table 2 for different subsets L of R, consider the smallest relations v0L vL on role chains satisfying the properties in Table 3. Note the similarities between the rules in Table 3 and rules in Table 2. Also note that unlike the derivation relation vL 0 in Table 3 does not 0 in Table 2, the relation vL depend on L and coincides with the closure of the role hierarchy. The following lemma can be easily proved using the correspondence between the rules L3, L5, L05, L6 and L06 and the rules E0, E1, E01, E2 and E02.
Lemma 1. For every subset L R of complex RIAs, all concepts A and B, and every role R, the following two conditions are equivalent:
and Ci 1 v0L 9Ri:Ci (1
The necessary and sufficient condition on L R that guarantees that our new calculus for E LR derives the same consequences as the original calculus, can now be defined as follows: Definition 2. A set of complex RIAs L following condition holds:
if ( i vL Ri)in=1 and R1 : : : Rn v R 2 R, then 1 : : : n vL R.
(
Intuitively, L R is left-admissible if the relation vL is closed under the
unrestricted version of the rule E2 when RIAs R1 : : : Rn v R can be taken not
only from R n L, but from the whole R (note the similarity of (
Example 1. Consider R consisting of the axiom
isPartOf isProperPartOf v isProperPartOf: It is easy to show that the following relations hold for any (of the two) L isPartOf v0L isPartOf isProperPartOf v0L isProperPartOf (by E0); (by E0); isPartOf isProperPartOf vL isProperPartOf (by E2 or E02): The following relation, however, holds only for L = ;: isPartOf isPartOf isProperPartOf vL isProperPartOf (by E2): When L = R, one cannot use E02 to produce (14) from (11) and (13) using (10). Therefore L = R is not left-admissible for R according to Definition 2.
Now suppose R is extended with the transitivity axiom
isPartOf isPartOf v isPartOf: Then, similarly, for any L
isPartOf isPartOf vL isPartOf (by E2 or E02): And now (14) can be produced from (16) and (12) using (10) for any L R. In fact, one can show that any L R will be left-admissible for the extended R. Theorem 1. Let KB be a knowledge base with RBox R, and L R be leftadmissible for R. Then C v D is derivable by rules in Table 1 using KB iff C vL D is derivable by rules in Table 2 using KB.
Proof. The “if” direction of the theorem is straightforward since each rule in Table 2 is a restriction of a corresponding rule in Table 1.
To prove the “only if” direction, assume to the contrary that there exists C v D derivable by rules in Table 1 such that C 6vL D. Without loss of generality, C v D is produced by some rule in Table 1 from some premises Ci v Di, 0 i < n, n 0, such that Ci vL Di. We obtain contradiction by considering all possible cases for such a rule. (10) R: (11) (12) (13) (14) (15) (16)
The only non-trivial case is an application of the rule C6 since all other rules have a direct counterpart in Table 2. In this case Di 1 = 9Ri:Ci (1 i n), C = C0, D = 9R:Cn and R1 : : : Rn v R 2 Rj.1By case (i) ) (ii) of Lemma 1 i v0L 9Rij :Cij (1 j mi) such tahpaptlieCdi0 t=o eCaich1,CCim1iv=L C9iRai:nCdi,Rti1her:e: :exRismtCivL Ri. Define i := Ri1 : : : Rimi .
i i Since i vL Ri (1 i n), R1 : : : Rn v R 2 R, and L is left-admissible, we have i : : : n vL R. By case (i) ( (ii) of Lemma 1 for ((Cij 1 v0L 9Rij :Cij )jm=i1)in=1 using i : : : n vL R we obtain C = C0 = C10 vL 9R:Cnmn = 9R:Cn = D, which contradicts C 6vL D. This proves the theorem. tu 5
(17)
(18)
It is difficult in general to verify the conditions of left-admissibility formulated
in Definition 2 since this requires checking property (
We start with the following sufficient condition for left-admissibility: Lemma 2. Let L
R be sets of complex RIAs that satisfy the property: if v S 2 R and 1 S
The proof of (18) is by induction on the derivation of vL S. In the base case E0 we have = S and the claim 1 S 2 vL R is part of the precondition. In all other cases E1–E02 there exist ( i vL Si)in=1, n 1 such that = 1 : : : n and S1 : : : Sn v S 2 R. By (17) 1 S1 : : : Sn 2 vL R. Now use the induction hypothesis (18) for each i vL Si to iteratively expand the left-hand side of 1 S1 : : : Sn 2 vL R to obtain the claim 1 2 = 1 1 : : : n 2 vL R.
To finish the proof of the lemma, we now show that (18) implies (
The following lemma formulates some useful closure properties of the relation vL, which hold for arbitrary L: Lemma 3. Let L R be sets of RIAs. If 1 vL S1, (Ti v0L Si)in=2, n S1 : : : Sn vL R, then 1 T2 : : : Tn vL R. 1, and Proof. Let = 1 T2 : : : Tn. We will show derivation of S1 : : : Sn vL R. vL R by induction on the We are now ready to formulate our main criterion for left-admissibility: Theorem 2. A subset L R of complex RIAs is left-admissible for an RBox R if and only if the following property holds: if
0 S2 and 1 S2 v S1 2 R, S1 vL 2 v R 2 L, then 1 2 vL R. (19) Proof. The “only if” direction of the theorem can be easily shown using Definition 2 since v S1 2 R and S1 v0L S2 imply vL S2.
To show the “if” direction, we first prove the following strengthening of (19): if
0 S2 and 1 S2
v S1 2 R, S1 vL
The proof of (20) is by induction on the derivation of 1 S2
E0: S2 = R and 1 = 2 = . Then (20) follows from (
E1: 1 S2 2 vL S and S v R 2 R. By the induction hypothesis 1 2 vL S, from which 1 2 vL R follows by E1.
E01: Analogous to the case of E1.
E2: 1 S2 2 = 1 : : : n, ( i vL Ri)in=1 and R1 : : : Rn v R 2 R n L. Let k be such that S2 occurs in k, that is 1 : : : k 1 = 01, k = 010 S2 020, k+1 : : : n = 02 and 1 = 01 010, 2 = 020 02. By the induction hypothesis 010 020 vL Rk, from which 1 2 = 1 : : : k 1 010 020 k+1 : : : n vL R follows by E2.
E02: 1 S2 2 = 1 T2 : : : Tn, 1 vL R1, (Ti v0L Ri)in=2 and R1 : : : Rn v R 2 L.
If S2 occurs in 1, then this is analogous to the case of E2. Otherwise, let k
be such that 1 T2 : : : Tk 1 = 1, Tk = S2 and Tk+1 : : : Tn = 2. By (
Having proved (20), condition (17) now follows by taking S1 = S2 = S in (20) and using rule E0 to derive S v0L S. Therefore L is left-admissible for R. tu
Condition (19) in Theorem 2 can be checked in polynomial time in the size of R. Indeed, there are only polynomially many possible instances of the precondition in (19). For every such precondition, the property 1 2 vL R can be checked in polynomial time by, e.g., applying Lemma 1: 1 2 vL R holds iff C0 vL 9R:Cn is derivable from (Ci 1 v0L 9Ri:Ci)in=1, where R1 : : : Rn = 1 2.
Theorem 2 can help checking if a given set L is left-admissible, but does not explain how to find such a set without exhaustively checking al possible subsets of R. The following sufficient condition will help us quickly find a suitable leftadmissible set of RIAs in practice: Theorem 3. For a set of RIAs R let L(R) be the set of exactly those complex RIAs v R 2 R that satisfy the following condition for all , 1, 2, S1, S2: if v S1 2 R, S1 v0R S2 and 1 S2 2 = , then 1 2 vR R.
(21) Then L(R) is left-admissible for R.
Proof. Note that the relations vL are anti-monotonic in L, that is for L1 L2 we have vL1 vL2 . Let L = L(R). Since L R, we have vL vR, and, since 0 = vR v0L does not depend on L, we have vL 0 . Now it is easy to show that L satisfies (19): Suppose v S1 2 R, S1 v0L S2 and 1 S2 2 v R 2 L. Then v0L = v0R implies S1 v0R S2, so 1 2 vR R by (21). Then vL vR implies 1 2 vL R, so (19) holds. Therefore L = L(R) is left-admissible for R by Theorem 2. tu 6
In this section we present the results of an experimental comparison of applying the calculi in Sections 2 and 3 to several commonly considered E L ontologies that contain complex RIAs, and discuss whether and to which extent our optimized treatment of RIAs can improve the performance of reasoning in practice.
To evaluate the proposed algorithms, we have implemented the calculi described in Sections 2 and 3 in a prototype Java-based reasoner ELK.1 All experiments were conducted using Java 1.6 on a 2:5 GHz quad core CPU with 4GB RAM running Fedora 13 Linux.
Our test ontology suite includes GO,2 FMA-lite,3 and an OWL EL version of GALEN.4 These ontologies contain only (left-admissible) RIAs of the form R v S and R R v R. In order to test which proportion of complex RIAs in realistic ontologies is left-admissible, we additionally considered the two latest versions of GALEN,5 namely GALEN7 and GALEN8, which contain RIAs of the form R v S, R S v R, and S R v R. We reduced these ontologies to E LR by removing all axioms for role functionalities and role inverses and replacing all datatypes by fresh atomic concepts. It is worth noting that the RIAs in GALEN7 and GALEN8 do not satisfy the regularity restrictions of OWL 2 [7] 1 http://code.google.com/p/elk-reasoner/ 2 obtained from http://lat.inf.tu-dresden.de/~meng/toyont.html 3 obtained from http://www.bioontology.org/wiki/index.php/FMAInOwl 4 obtained from http://condor-reasoner.googlecode.com/ 5 obtained from http://www.opengalen.org/sources/sources.html and, for this reason, no OWL reasoner can handle them in the unreduced form. We have excluded SNOMED CT from our experiments for the reason that the only complex RIA it contains is redundant for classification in the sense that rule C6 is never applied on this ontology.
In our experiments, we first normalized all test ontologies using structural transformation, and applied Theorem 3 to identify left-admissible sets of RIAs. Table 4 presents statistics on the number of axioms of each type and the number of left-admissible RIAs for each of the tested ontologies. For GALEN7 and GALEN8, which contain identical complex RIAs, we found a left-admissible subset containing 183 out of the total 385 complex RIAs. In this case, we additionally checked that adding any one of the remaining complex RIAs to the previously found 183 violates the conditions of Theorem 2, showing that the left-admissible subset of RIAs we found is maximal. For the remaining ontologies, the full set of RIAs is left-admissible since transitivity axioms are the only kind of complex RIA. In general, the computation of left-admissible RIAs had no relevant impact on overall performance, running in less than 0:5 seconds in all cases.
For each of the tested ontologies, we computed the saturation under the inference rules of Table 1 and Table 2. Table 4 presents the total number of different conclusions of each type, and the total number of inferences for each rule. In accordance with Theorem 1, both approaches produce the same conclusions. For this reason, the number of applications of each rule C0–C5 coincides with the corresponding number for rules L0–L05. Differences between the two approaches are found in the number of applications of C6 on the one hand, and the combined number of applications of L6 and L06 on the other hand. As can be seen from the results, the effect of our optimization strongly depends on the input ontology, with the largest relative reductions obtained for FMA-lite and GO, and less significant reductions for all versions of GALEN.
Although the reduction in the number of rule application is significant for FMA-lite and GO, this, surprisingly, did not translate to a significant reduction in the running time for our prototype implementation. For FMA-lite, for example, the running time is reduced just from 7:2 to 6:1 seconds (15:3%), which is less than expected for more than 65% reduction in the number of inferences. For other ontologies the reduction in the running time was even less measurable.
One possible explanation for this effect is that a rule application producing a new consequence costs more than a rule application producing a previously derived consequence because the first requires a (relatively expensive) memory allocation. Since our optimized procedure derives exactly the same conclusions, it reduces only the number of inferences of the second kind. Nevertheless, our optimization can give improvement in some cases and should not be difficult to implement (at least for transitivity) in any reasoner based on the original E L calculus [1], such as in CEL/jCEL [2] or Snorocket [5].