Consequence-Driven Reasoning for Horn SHIQ Ontologies Yevgeny Kazakov Oxford University Computing Laboratory 1 Introduction Ontologies are formal vocabularies of terms describing specific subjects like chemical elements, genes, or animal species. The terms in ontologies are “defined” by means of relationships with other terms of the ontology using ontology languages. Ontology languages based on Description Logics (DLs) [1], such as OWL [2], are becoming increasingly popular among ontology developers thanks to the availability of ontology reasoners, which provide automated support for visualization, debugging, and querying of ontologies. Classification is a central reasoning service provided by ontology reasoners. The goal of classification is to compute a hierarchical relation between classes. The class hierarchy is used to browse ontologies in ontology editors. Most of the currently-available ontology reasoners are based on so-called model building procedures such as tableau [3] and hyper-tableau [4] calculi. Such procedures classify an input ontology, in general, by iterating over all necessary pairs of classes, and trying to build a model of the ontology that violates the subsumption relation between them. Recent investigations of tractable DLs such as EL++ [5] led to the discovery of another type of reasoning procedures. Instead of enumerating pairs of classes and building counter-models, the procedure derives subsumption relations explicitly using special inference rules. The advantage is that subsumption relations are computed “all at once” in a goal-directed way without costly enumerations. The EL++ language sacrifices many commonly-used constructors, such as inverse roles and functional restrictions, in order to ensure that reasoning is tractable. In this paper we describe a reasoning procedure, which utilizes the core reasoning technique of EL++ , but works for the larger class of so-called Horn SHIQ ontologies. Horn SHIQ ontologies are ontologies expressed in the DL SHIQ, which do not contain “non- deterministic” constructors, such as positive disjunction: A v B t C. Horn SHIQ has originally drawn attention due to its tractable data complexity [6]. Our paper demonstrates that Horn SHIQ ontologies can have a more efficient classification procedure. This paper is organised as follows. In the preliminaries we introduce Horn SHIQ and a completion-based procedure for a fragment of EL++ . In Section 3 we discuss how to extend this procedure for new constructors in Horn SHIQ. In Section 4 we present our reasoning procedure and prove soundness, completeness, and termination. Finally, in Section 5 we present an empirical comparison of a prototypical implementation of our procedure with other reasoners, which demonstrates a substantial performance improvement. This paper is an adapted version of [7]. Name Syntax Semantics Concepts: atomic concept A AI (given) top concept > ∆I bottom concept ⊥ ∅ negation ¬C ∆I \ C I conjunction C uD C I ∩ DI disjunction C tD C I ∪ DI existential restriction ∃R.C {x | RI (x, C I ) 6= ∅} universal restriction ∀R.C {x | RI (x, ∆I \ C I ) = ∅} min cardinality >nS.C {x | ||S I (x, C I )|| ≥ n} max cardinality 6mS.C {x | ||S I (x, C I )|| ≤ m} Axioms: role inclusion R1 v R2 R1I ⊆ R2I role transitivity Tra(R) RI ◦ RI ⊆ RI concept inclusion CvD C I ⊆ DI Table 1. The syntax and semantics of SHIQ 2 Preliminaries In this section we define the description logics SHIQ and EL+ , as well as their frag- ments Horn SHIQ and ELH. To simplify the presentation and save space, we will not consider ABox assertions in this paper. 2.1 The Description Logic SHIQ A description logic vocabulary consists of countably infinite sets NC of atomic concepts, and NR of atomic roles. A SHIQ role is either r ∈ NR or an inverse role r− with r ∈ NR . We denote by R− the inverse of a role R defined by R− := r− when R = r and R− := r when R = r− . The syntax and semantics of SHIQ is summarized in Table 1. The set of SHIQ concepts is recursively defined using the constructors given in the upper part of Table 1, where A ∈ NC , C, D are concepts, R, S roles, and n, m positive integers. A terminology or ontology is a set O of axioms specified in the lower part of Table 1. A role R is transitive (in O) if Tra(R) ∈ O or Tra(R− ) ∈ O. Given an ontology O, let R1 vO R2 be the smallest transitive reflexive relation between roles such that R1 v R2 ∈ O implies R1 vO R2 and R1− vO R2− . For concepts of the form >nS.C and 6mS.C in O the role S must be simple, that is, R vO S holds for no transitive role R. The semantics of SHIQ is defined using interpretations. An interpretation is a pair I = (∆I , ·I ) where ∆I is a non-empty set called the domain of the interpretation and ·I is the interpretation function, which assigns to every A ∈ NC a set AI ⊆ ∆I , and to every r ∈ NR a relation rI ⊆ ∆I × ∆I . The interpretation is extended to roles by (r− )I := {hx, yi | hy, xi ∈ rI } and to concepts according to the right column of Table 1, where ρ(x, U ) for ρ ∈ ∆I × ∆I , U ⊆ ∆I , and x ∈ ∆I denotes the set {y | hx, yi ∈ ρ ∧ y ∈ U }, and ||V || denotes the cardinality of a set V ⊆ ∆I . An interpretation I satisfies an axiom α (written I |= α) if the respective condition to the right of the axiom in Table 1 holds; I is a model of an ontology O (written I |= O) if I satisfies every axiom in O. We say that α is a (logical) consequence of O, or is entailed by O (written O |= α) if every model of O satisfies α. Classification is a key reasoning problem for description logics and ontologies, which requires to compute all subsumptions A v B entailed by O between atomic concepts. 2.2 The Horn Fragment of SHIQ Positive and negative polarities of occurrences of SHIQ concepts in concepts and axioms are defined as follows: – C occurs positively in C; – C occurs positively (negatively) in concepts of the forms ¬C2 , C1 u D1 , C1 t D1 , ∃R.C1 , ∀R.C1 , >nS.C 1 , 6mS.C 2 , and C2 v D1 if C occurs positively (nega- tively) in C1 or in D1 , or negatively (positively) in C2 (when applicable). A concept C occurs positively (negatively) in an ontology O if C occurs positively (negatively) in some axiom of O. Note that it is possible for a concept to occur positively and negatively at the same time in an axiom or an ontology. A SHIQ ontology O is Horn if: – no concept of the form C t D or 6mR.C with m > 1 occurs positively in O; – no concept of the form ¬C, ∀R.C, >nR.C with n > 1, or 6mR.C occurs nega- tively in O. 2.3 Structural Transformation Structural transformation is used to simplify the axioms of the ontology preserving its “structure”. Given a SHIQ ontology O, for every (sub-)concept C in O we introduce a fresh atomic concept AC and define a function st(C) by: – st(A) = A; st(>) = >; st(⊥) = ⊥; st(¬C) = ¬AC ; – st(C u D) = AC u AD ; st(C t D) = AC t AD ; – st(∃R.C) = ∃R.AC ; st(∀R.C) = ∀R.AC ; – st(>nR.C) = >nR.AC ; st(6mR.C) = 6mR.AC . The result of applying structural transformation to O is an ontology O0 that contains all role inclusion and role transitivity axioms in O in addition to the following axioms: – AC v st(C) for every C occurring positively in O – st(C) v AC for every C occurring negatively in O – AC v AD for every concept inclusion C v D ∈ O It can be shown that structural transformation preserves the logical consequences of ontological axioms. Proposition 1. Let O0 be obtained from O by structural transformation. Then for every axiom α containing no introduced atomic concepts AC , we have O |= α iff O0 |= α. AvB IR1 IR2 CR1 :BvC∈O AvA Av> AvC AvB AvC AvB CR2 :BuC vD ∈O CR3 : B v ∃r.C ∈ O AvD A v ∃r.C A v ∃r.B A v ∃r.B B v C CR4 :rvs∈O CR5 : ∃r.C v D ∈ O A v ∃s.B AvD Table 2. The Completion Rules for ELH 2.4 The Description Logic EL+ The description logic EL+ is one of the few description logics for which standard reasoning problems are decidable in polynomial time. EL+ allows only for concepts constructed from atomic concepts A and the top concept > using conjunction C u D and existential restriction ∃r.C, where r is an atomic role. The axioms of EL+ can be either concept inclusions C v D or complex role inclusions of the form r1 ◦ · · · ◦ rn v s. The last are interpreted in I as r1I ◦ · · · ◦ rnI ⊆ sI , where ◦ is a composition of binary relations. For the purpose of this paper, we consider a common fragment of EL+ and SHIQ called ELH, which allows only for (simple) role inclusions of the form r v s. It can be easily seen that every ELH ontology is a Horn SHIQ ontology since it cannot contain concepts of the form ¬C, C t D, ∀R.C, >nR.C, or 6mR.C. In [5], a polynomial time classification procedure has been presented for the de- scription logic EL++ , which extends EL+ with the bottom concept ⊥, nominals, and “safe” concrete domains. The procedure uses a number of so-called completion rules that derive new concept inclusions. In Table 2 we list the completion rules relevant to ELH. The rules are applied to a normalised ELH ontology O that is obtained from the input ontology by structural transformation and simplification. Structural transformation for ELH produces only axioms of the form (1) A v B, (2) A u B v C, (3) A v B u C, (4) A v ∃r.B, (5) ∃r.A v B, and (6) r v s, where A, B, and C are atomic concepts or >, and r, s atomic roles. Axioms A v B u C of form (3) are then replaced with a pair of axioms A v B and A v C of form (1). The completion rules in Table 2 derive new axioms of the form A v B and C v ∃r.D from already derived axioms using axioms in O as side conditions, where A, B, C, and D are atomic concepts or >, and r, s atomic roles.1 In [5] it was shown that the rules IR1–CR5 are complete for classification, that is, a concept subsumption A v B is entailed by O if and only if it is derivable by these rules. 3 From ELH to Horn SHIQ Horn SHIQ extends ELH by allowing many new constructors, notably, inverse roles, functionality restrictions, and positive occurrences of universal restrictions. These con- 1 In [5], instead of deriving new axioms A v B and C v ∃r.D, the completion rules add B to the set S(A) and a pair (C, D) to the set R(r). Thus the set S(A) represents the set of super-concepts of A and the set R(r) represents the pairs of r-existentially related concepts. structors have been disallowed in ELH and EL++ for complexity reasons—in [5, 8] it was shown that adding any of these constructors results in a complexity increase from PTime to ExpTime. In this section we give an informal explanation for this complexity increase and outline how the completion-based procedure for ELH can be extended to handle the new Horn SHIQ constructors. 3.1 Inverse Roles and Universal Restrictions According to the definition in Section 2.2, Horn SHIQ allows for the usage of inverse roles and positive occurrences of universal restrictions. In fact, positive occurrences of universal restrictions can be expressed by means of inverse roles using the equivalence: A v ∀R.B ⇔ ∃R− .A v B. (1) The increase in the complexity of reasoning with inverse roles and universal restric- tions, can be partially explained by a new kind of interaction between these constructors. Axioms of the form A v ∃R.B and C v ∀S.D can interact in two ways. First, the following inference (2) is possible: A v ∃R.B B v ∀R− .D (2) AvD It is easy to see using equivalence (1) that (2) is an instance of CR5 in Table 2. A new kind of interaction is inference (3): A v ∃R.B C v ∀R.D (3) A u C v ∃R.(B u D) In contrast to (2), and all inference rules in Table 2, which have only conclusions of the d A v Bd form or A v ∃R.B, drepeateddapplications of (3) can produce axioms of the form Ai v ∃R. Bj , where Ai and Bj are arbitrary conjunctions of atomic concepts. The number of such axioms is no longer polynomially bounded. Note, however, that there are at most exponentially many (semantically non-equivalent) axioms of this form since the number of different concepts in the conjunctions is always bounded. We will use this property to establish an exponential upper bound for our procedure. 3.2 Functional Restrictions on Roles Horn SHIQ allows for expressing a functional restriction for a simple role S using the constructor 61S.>. Since, for a functional role S, the axiom C v ∃S.D implies C v ∀S.D, the following analogs of inferences (3) and (2) are possible: A v ∃S.B C v ∃S.D A v 61S.> (4) A u C v ∃S.(B u D) A v ∃S.B B v ∃S − .C B v 61S − .> (5) AvC In Section 4, we generalize inferences (2)–(5) and present a sound and complete rules for Horn SHIQ system of inference d d ontologies, d which derives only consequence axioms of the form Ai v B and Ai v ∃R.( Bj ). 4 The Calculus for Horn SHIQ Ontologies In this section we present a consequence-based procedure for classifying Horn SHIQ ontologies. The procedure consists of a preprocessing stage that applies structural transformation, simplifications, and elimination of transitivity, and a saturation stage that applies inferences to derive new axioms. 4.1 Normalization From now on we use A(i) , B(i) to denote atomic concepts, R(i) roles, and S(i) simple roles. We say that a concept d C is simple if it is of the form ⊥, A, ∃R.A, ∀R.A, or 61S.A. We denote by Ai a (possibly empty) conjunction of atomic concepts. The empty conjunction is abbreviated to >. 0 Lemma 1. Every Horn SHIQ ontology O d can be transformed into an ontology O containing only axioms of the forms: (n1) Ai v C, (n2) R1 v R2 , and (n3) Tra(R), where C is a simple concept. The transformation preserves (non)entailment of axioms α over the signature of O and can be performed in polynomial time assuming unary coding of numbers. Proof. By applying structural transformation to O, we obtain an ontology O0 containing only concept inclusions of the form A1 v A2 , A v st(C1 ), and st(C2 ) v A, where C1 occurs positively in O and C2 occurs negatively in O. Since O is a Horn SHIQ ontology, C1 can only be of the form >, ⊥, A, ¬C, C u D, ∃R.C, ∀R.C, >nS.C, or 61S.C, and C2 only of the form >, ⊥, A, C u D, C t D, ∃R.C, or >1R.C. Concept inclusions of the form A v st(C1 ) that are not of form (n1), are transformed to form (n1) as follows: – A v st(¬C) = ¬AC ⇒ A u AC v ⊥; – A v st(>nS.C) = >nS.AC ⇒ A v ∃S.Bi , Bi v AC , 1 ≤ i ≤ n, Bi u Bj v ⊥, 1 ≤ i < j ≤ n, where Bi are fresh atomic concepts. Concept inclusions of the form st(C2 ) v A that are not of form (n1) are transformed to form (n1) as follows: – st(C t D) = AC t AD v A ⇒ AC v A, AD v A; – st(∃R.C) = ∃R.AC v A ⇒ AC v ∀R− .A; – st(>1S.C) = >1S.AC v A ⇒ AC v ∀S − .A. It is easy to show using Proposition 1, that O0 |= α iff O |= α for every axiom α containing no new symbols. t u 4.2 Elimination of Transitivity After normalization, we apply a well-known technique, which allows the elimination of transitivity d axioms. Transitivity axioms of form (n3) in Lemma 1 can interact only with axioms Ai v ∀R.B of form (n1) through role inclusions (n3). The transformation d introduces a triple of axioms (6) for every axiom Ai v ∀R.B of form (n1) and every transitive sub-role T of R, where B T is a fresh atomic concept: d Ai v ∀T.B T B T v ∀T.B T BT v B (6) d Intuitively, B T is used to propagate B to all elements reachable from elements in Ai via a T -chain. Lemma 2. Let O be consisting of axioms of forms (n1)–(n3) in Lemma 1, and O0 be obtained from O by adding axioms (6) as described above and removing all transitivity axioms (n3). Then for every axiom α that does not contain concepts B T and non-simple roles, we have O |= α iff O0 |= α. Proof (sketch). It is sufficient to show that (i) every model I of O can be turned into a model J of O0 by (re-)interpreting concepts B T , and conversely, (ii) every model J of O0 can be turned into a model I of O by (re-)interpreting non-simple roles. Both of these transformations preserve the interpretation of axioms α that do not contain these symbols. For proving (i), we interpret B T in J as (B u ∀T.B)I . Trivially, the last two axioms d in (6) are satisfied in J . The first axiom in (6) is satisfied in J since J satisfies Ai v ∀R.B and T is a transitive sub-role of R. J satisfies the remaining axioms in O0 since they do not contain the new concepts B T . For proving (ii), we interpret every non-simple role R in I as the union of RJ and the transitive closures of T J for every transitive sub-role T of R (T J is not necessarily a transitive relation since O0 does not contain the transitivity axioms). It is easy to show d I satisfies all axioms (n1)–(n3). In particular, I satisfies the axioms of the form that Ai v ∀R.B since I remains to be a model of axioms (6). t u 4.3 The Inference Rules Our procedure for Horn SHIQ ontologies works by saturating the input axioms under the rules in Table 3. The rules are applied to a preprocessed ontology containing axioms of form (n1) and (n2) in Lemma 1, and produce axioms of the form M v C and M v ∃R.N , where M and N are conjunctions of atomic concepts, and C is a simple concept. Rules I1 and I2 produce the initial (tautological) concept inclusions for arbitrary M and A, which are then extended using axioms in O by rule R1. Rules R2–R6 are specific to the kinds of simple concepts implied by the conjunctions. Rule R2 propagates the entailment of bottom backwards over existential restrictions. Rules R3 and R4 deal with universal restrictions and generalize respectively inferences (3) and (2) in Section 3.1. Likewise, rules R5 and R6 with 7 premises, deal with qualified functional restrictions and generalize inferences (4) and (5). Note that in contrast to (5), rule R6 has two conclusions. Rules R3–R6 assume that the closure R1 vO R2 of role inclusions of form (n2) is computed. The inference rules I1–R6 are applied exhaustively until no new axiom can be derived. The resulting ontology O0 is called the saturation of O. I1 I2 M uAvA M v> n M v A1 . . . M v An l M v ∃R.N N v ⊥ R1 : Ai v C ∈ O R2 M vC i=1 M v⊥ M v ∃R1 .N M v ∀R2 .A M v ∃R1 .N N v ∀R2 .A R3 : R1 vO R2 R4 : R1 vO R2− M v ∃R1 .(N u A) M vA M v ∃R1 .N1 N1 v B M v ∃R1 .N1 M v B M v ∃R2 .N2 N2 v B N1 v ∃R2 .(N2 u A) M v 61S.B R1 vO S N1 v 61S.B N2 u A v B R1 vO S − R5 : R6 : M v ∃R1 .(N1 u N2 ) R2 vO S M v A M v ∃R2− .N1 R2 vO S Table 3. Saturation Rules for Horn SHIQ Ontologies 4.4 Soundness and Completeness In this section we demonstrate that our procedure is sound and complete for classification, that is, it derives all subsumptions between atomic concepts in the input ontology. Theorem 1. Let O be an ontology containing only axioms of the form (n1) and (n2) in Lemma 1 and O0 the saturation of O under the rules in Table 3. Then (i) O |= M v B iff M v ⊥ ∈ O0 or M v B ∈ O0 , and (ii) O |= M v ∃R.N iff M v ⊥ ∈ O0 or there exists M v ∃R1 .N1 ∈ O0 such that R1 vO R and N1 v B ∈ O0 for every conjunct B in N . Proof (sketch). It is easy to show that every axiom in O0 is entailed by O since the inference rules in Table 3 derive only logical consequences of the axioms in their premises. In other words, the system of rules is sound. Therefore the “if” direction of points (i) and (ii) are trivial. In order to prove the “only if” direction of points (i) and (ii), we construct a canonical model of O0 . Let Σ be the set of all conjunctions M such that M v ⊥ ∈ / O0 . If Σ is empty, then M v ⊥ ∈ O0 for every M , and so, (i) and (ii) hold. In the remainder of the proof, we assume that Σ is not empty. Let I = (∆I , ·I ) be such that ∆I = Σ + is the set of all finite non-empty words over Σ, and ·I defined as follows: – AI = {wM | M v A ∈ O0 , w ∈ Σ ∗ } – The roles are interpreted with smallest relations satisfying all role inclusions such that if M v ∃R.N ∈ O0 and M v ∃R.N 0 ∈ / O0 for every super-conjunct N 0 of N , then for every w ∈ Σ ∗ , either hwM, wi ∈ RI and w ∈ AI for every A ∈ N , or otherwise hwM, wM N i ∈ RI . Intuitively, the interpretation I is a forest where nodes are labeled with non-contradictory conjunctions M ∈ Σ and every node has a successor node for every non-contradictory conjunction N ∈ Σ. Roles can connect only successive nodes in such a way that all axioms M v ∃R.N ∈ O0 with maximal N are satisfied: if for a node marked with M the connection to its predecessor does not satisfy this axiom, it is connected to its successor marked with N . Rule R3 ensures that N is not contradictory if M is not. Note that hwM, wM N i ∈ RI implies M v ∃R1 .N ∈ O0 for some R1 vO R. Below we demonstrate that I is a model of O (and consequently of O0 ). Claim 1 wM ∈ Σ + and M v C ∈ O0 imply wM ∈ C I . – For C = ⊥, if M v ⊥ ∈ O0 then wM 6∈ Σ + . – For C = A the claim follows from the definition of AI . – For C = ∃R.B, take M v ∃R.N ∈ O0 with the largest N containing B (it exists since M v ∃R.B ∈ O0 ). By definition of RI , we have wM ∈ (∃R.N )I ⊆ C I . – For C = ∀R.B, we show that: (i) hwM, wM N i ∈ RI implies wM N ∈ B I , and (ii) hwN M, wN i ∈ RI implies wN ∈ B I . In case (i) there is M v ∃R1 .N ∈ O0 with R1 vO R. Since M v C ∈ O0 and O0 is closed under R3, we have N = N u B (since N is a maximal conjunction), and so, wM N ∈ B I . In case (ii), there is N v ∃R1 .M ∈ O0 with R1 vO R− . Since M v C ∈ O0 and O0 is closed under R4, we have N v B ∈ O0 , and so, wN ∈ B I . – For C = 61S.B, we show that: (i) hwM, wM Ni i ∈ S I and wM Ni ∈ B I for i = 1, 2 implies N1 = N2 , and (ii) hwN M, wN i ∈ S I , and wN ∈ B I implies hwN M, wN M N1 i ∈ / S I whenever wN M N1 ∈ B I . In case (i) we have M v ∃Ri .Ni ∈ O0 where Ri vO S and Ni v B ∈ O0 , i = 1, 2. Since O0 is closed under R5, we have M v ∃Ri .(N1 u N2 ) ∈ O0 , i = 1, 2. Since each Ni is maximal for M and Ri , i = 1, 2, we have N1 = N1 u N2 = N2 . In case (ii), we have N v ∃R.M ∈ O0 , R vO S − , and N v B ∈ O0 . Assume to the contrary that hwN M, wN M N1 i ∈ S I and wN M N1 ∈ B I . Then hwN M, wN M N1 i ∈ R1I for some R1 vO S such that M v ∃R1 .N1 ∈ O0 , and N1 v B ∈ O0 . Since O0 is closed under R6, we have N v ∃R1− .M ∈ O0 and N v A ∈ O for every conjunct A in N1 . Hence M v ∃R1 .N1 is already satisfied in wN M by its predecessor wN , and so the relation hwN M, wN M N1 i ∈ R1I should not have been created. Now for every axiom Ai v C of form (n1) in O, if wM ∈ AIi then M v Ai ∈ O0 , d and so, M vdC ∈ O0 by R1. By Claim 1 we then have wM ∈ C I . Thus, I satisfies every axiom Ai v C in O of form (n1). The definition of the interpretation of roles in I ensures that every role inclusion of form (n2) is also satisfied in I. Hence, I is a model of O. Now we can finish the proof for the “only if” directions of points (i) and (ii). For proving (i), if O |= M v B and M v ⊥ ∈ / O0 then for every wM ∈ Σ + , we have wM ∈ B since I is a model of O. Hence M v B ∈ O0 by definition of I. For proving I (ii), if O |= M v ∃R.N and M v ⊥ ∈ / O0 , then for M ∈ Σ + , we have M ∈ (∃R.N )I . Since M ∈ Σ does not have a predecessor in Σ + , there exists M v ∃R1 .N1 ∈ O0 + such that R1 vO R and M N1 ∈ B I for every conjunct B in N . By definition of I, this implies that N1 v B ∈ O0 for every conjunct B in N . t u Theorem 1, in conjunction with Lemmas 1 and 2, implies that our procedure based on the rules in Table 3 can be used, in particular, for computing all subsumptions A v B between atomic concepts implied by the input ontology. In other words, the procedure is complete for classification of Horn SHIQ ontologies. Moreover, since the number of axioms of the form M v C and M v ∃R.N is at most exponential in the number of atomic concepts, the procedure is guaranteed to terminate in exponential time. Since deciding concept subsumptions in Horn SHIQ ontologies is ExpTime-complete (in ExpTime since Horn SHIQ is a fragment of SHIQ and ExpTime-hard since, e.g., Horn SHIQ contains EL with functionality), this implies that our procedure is computationally optimal. 4.5 Practical Considerations Theorem 1 actually implies a stronger result than just completeness of the calculus for classification. The rules in Table 3 can, in fact, be used to derive all subsumptions between conjunctions of atomic concepts and (existentially restricted conjunctions of) atomic concepts. For computing just a subset of these relations, e.g., for classification, our procedure can be significantly optimized by applying rules I1 and I2 selectively depending on the goal subsumptions. Specifically, I1 and I2 can be restricted to produce conjunctions N only when either (i) N is the left hand side of a goal subsumption (e.g., for classification, N is an atomic concept from the input ontology), or (ii) an axiom of the form M v ∃R.N has been derived. The above optimization not only reduces the number of inferences, but also yields a polynomial time classification procedure for ELH ontologies. Indeed, it is easy to see that for ELH ontologies the rules R3, R5, and R6 never apply. The remaining rules produce only polynomially many axioms of the form A v C and A v ∃R.B since those rules (including I1 and I2) never form conjunctions of several concepts. 5 Experimental Evaluation The main goal for our consequence-based procedure for Horn SHIQ ontologies, was to reason efficiently with medium-sized ontologies such as Galen [9]. Galen turned out to be very difficult for model-building reasoners since it contains a large number of existential dependencies between classes of the form A v ∃R.B. These dependencies are used, e.g., for expressing partonomy relations between anatomical units, for exam- ple: BasilarArtery v ∃isBranchOf.VertebralArtery. The dependency relation between classes induced by such axioms is very large and highly cyclic. Because of the numerous cycles, model building reasoners fail to produce (a finite representation of) a model since cycle detection mechanisms (blocking) do not appear to be effective in these cases. The reasoner CEL for EL+ does not exhibit this problem since it does not build models but performs inferences according to Table 2. Axioms of the form A v ∃R.B are relatively harmless for CEL since these axioms alone do not result in any inference. Unfortunately, CEL cannot handle the full version of Galen since it does not support functionality and inverse roles, which Galen extensively uses. Thus the main question of our evaluation was whether the reasoner implemented according to the rules in Table 3 can scale well for ontologies outside the polynomial DL EL+ . To evaluate the performance of our procedure, we implemented a prototype reasoner CB [10] using a simplified version of the rules in Table 3 for Horn SHIF ontolo- gies, which are sufficient for Galen. We compared the results with the model-building FaCT++ Pellet HermiT CEL CB GO 15.24 72.02 199.52 1.84 1.17 NCI 6.05 26.47 169.47 5.76 3.57 GalenA− 3166.74 133.25 91.98 3.27 0.26 GalenA 465.35 — 45.72 n/a 0.32 GalenB− — — — 189.12 4.07 GalenB — — — n/a 9.58 Snomed 650.37 — — 1185.70 49.44 Table 4. A comparison of classification times (in seconds): “—” means that the reasoner failed to return the result; “n/a” means that the test could not be performed. reasoners FaCT++ v.1.2.1 [11], Pellet v.1.5 [12], and HermiT v.0.9.3 [13], and the completion-based reasoner CEL v.1.0b [14]. We ran the experiments on a PC with a 2GHz Intelr CoreTM Duo processor and 1.5GB RAM operated by Linux v.2.6.27 with Java VM v.1.6.0. We set time out of 3600 seconds and Java heap space of 1GB for Java-based reasoners. We tested the classification of seven medical ontologies of various sizes and com- plexities. The Gene Ontology (GO) [15] and National Cancer Institute thesaurus (NCI) [16] are fairly large ontologies describing respectively 20465 and 27652 classes, but with a rather shallow structure inducing not many dependencies. We have considered four versions of Galen. GalenA with 2748 classes is based on an early version of Galen [17]. GalenB with 23136 classes is based on a more recent version of Galen [9]. GalenA− and GalenB− are obtained from GalenA and GalenB by removing functionality and inverses. We have also included the results for the very large but simple ontology Snomed, which contains 389472 classes. The results of the experiments are summarized in Table 4. The time measured for CB includes loading, preprocessing, classification of the ontology and computing the transitively reduced and alphabetically sorted concept hierarchy. CB spends most of the time on loading for GO and NCI and on classification for the remaining ontologies, and considerably outperforms the other tested reasoners. In particular, CB is able to classify in just under 10 seconds the largest version of Galen, which could not be classified by the other reasoners. It is worth commenting on the difference in the performance between CEL and CB. Although the rules in Table 3, when restricted to EL+ ontologies, are very similar to those in Table 2, there is a small but important difference. Namely, our procedure has no analogue of rule CR4 in Table 2, which unfolds role inclusions into existential restrictions. Instead, the closure of role inclusions is computed separately and used in the premises of rules R3-R6. This strategy appears to be more efficient in situations when the number of role inclusions is small in comparison to the number of existential restrictions (which is mostly the case), and could explain the test results. References 1. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F., eds.: The Description Logic Handbook. Cambridge University Press (2007) 2nd edition. 2. http://www.w3.org/2004/OWL/ 3. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive description logics. Logic Journal of the IGPL 8(3) (2000) 4. Motik, B., Shearer, R., Horrocks, I.: Optimized reasoning in description logics using hyper- tableaux. In: CADE. Volume 4603 of Lecture Notes in Computer Science., Springer (2007) 67–83 5. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: IJCAI, Professional Book Center (2005) 364–369 6. Hustadt, U., Motik, B., Sattler, U.: Reasoning in description logics by a reduction to disjunctive datalog. J. Autom. Reasoning 39(3) (2007) 351–384 7. Kazakov, Y.: Consequence-driven reasoning for horn SHIQ ontologies. In: IJCAI. (2009) To Appear. 8. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope further. In: Proc. of OWLED 2008. (2008) 9. http://www.co-ode.org/galen/ 10. http://code.google.com/p/cb-reasoner/ 11. http://owl.man.ac.uk/factplusplus/ 12. http://clarkparsia.com/pellet/ 13. http://www.hermit-reasoner.com/ 14. http://lat.inf.tu-dresden.de/systems/cel/ 15. http://www.geneontology.org/ 16. http://www.cancer.gov/ 17. http://www.comlab.ox.ac.uk/people/yevgeny.kazakov/ontologies/ galen-ian-horrocks-original.owl.zip