Consequence-Driven Reasoning for Horn SHIQ Ontologies

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) [Baader et al., 2007], such as OWL, 1 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 [Horrocks et al., 2000] and hyper-tableau [Motik et al., 2007] 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++ [Baader et al., 2005] led to the discovery of another type of reasoning procedures. Instead of enumerating pairs of classes and building counter-models, the procedure for EL++ derives subsumption relations explicitly using special inference rules. The advantage of this method is that subsumption relations are computed "all at once" in a goal-directed way without costly enumerations.

1 http://www.w3.org/2004/OWL/

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 a larger class of socalled 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 ⊑ B ⊔ C. Horn SHIQ originally has drawn attention in [Hustadt et al., 2007] due to its tractable data complexity. Our paper demonstrates that Horn SHIQ ontologies also admit for 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.

2 Preliminaries

In this section we define the description logics SHIQ and EL+, as well as their fragments 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:= rwhen 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 ⊑O R2 be the smallest transitive reflexive relation between roles such that R1 ⊑ R2 ∈ O implies R1 ⊑O R2 and R1 ⊑O R2 . It is required that for every concept of the form ⩾nS.C and ⩽mS.C in O the role S is simple, that is, R ⊑O 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 := {〈x, y〉 | 〈y, x〉 ∈ 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 | 〈x, y〉 ∈ ρ ∧ 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 ⊑ 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 ¬C-, C+ ⊓D+, C+ ⊔D+, ∃R.C+, ∀R.C+, ⩾nS.C+, ⩽mS.C-, and C- ⊑D+ if C occurs positively (negatively) in C+ or in D+, or negatively (positively) in C- (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 ⊔ D or ⩽mR.C with m > 1 occurs positively in O;
• no concept of the form ¬C, ∀R.C, ⩾nR.C with n > 1, or ⩽mR.C occurs negatively 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 ⊓D) = AC ⊓AD; st(C ⊔D) = AC ⊔AD
• st(∃R.C) = ∃R.AC; st(∀R.C) = ∀R.AC;
• st(⩾nR.C) = ⩾nR.AC; st(⩽mR.C) = ⩽mR.AC.

The result of applying structural transformation to O is an ontology O′ that contains all role inclusion and role transitivity axioms in O in addition to the following axioms:

• AC ⊑ st(C) for every C occurring positively in O
• st(C) ⊑ AC for every C occurring negatively in O
• AC ⊑ AD for every concept inclusion C ⊑ D ∈ O

It can be shown that structural transformation preserves the logical consequences of ontological axioms.

Proposition 1 Let O′ be obtained fromO by structural transformation. Then for every axiom α containing no introduced atomic concepts AC, we have O |= α iff O′ |= α.

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 ⊓ D and existential restriction ∃r.C, where r is an atomic role. The axioms of EL+ can be either concept inclusions C ⊑ D or complex role inclusions of the form r1 ◦· · ·◦rn ⊑ s. The last are interpreted in I as rI 1 ◦ · · · ◦ rIn ⊆ 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 ⊑ 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 ⊔ D, ∀R.C, ⩾nR.C, or ⩽mR.C.

In [Baader et al., 2005], a polynomial time classification procedure has been presented for the description 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

Table 2: The Completion Rules for ELH

obtained from the input ontology by structural transformation and simplification. Structural transformation for ELH produces only axioms of the form (1) A ⊑ B, (2) A ⊓ B ⊑ C, (3) A ⊑ B ⊓C, (4) A ⊑ ∃r.B, (5) ∃r.A ⊑ B, and (6) r ⊑ s, where A, B, and C are atomic concepts or ⊤, and r, s atomic roles. Axioms A ⊑ B ⊓ C of form (3) are then replaced with a pair of axioms A ⊑ B and A ⊑ C of form (1).

The completion rules in Table 2 derive new axioms of the form A ⊑ B and C ⊑ ∃r.D from axioms in O and other axioms of these forms already derived, where A, B, C, and D are atomic concepts or ⊤, and r, s atomic roles. 2 In [Baader et al., 2005] it was shown that the rules IR1-CR5 are complete for classification, that is, a concept subsumption A ⊑ 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 constructors have been disallowed in ELH and EL++ for complexity reasons-in [Baader et al., 2005; 2008] 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 ontologies allow 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 (1):

2 In the original presentation [Baader et al., 2005], instead of deriving new axioms A ⊑ B and C ⊑ ∃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 concepts that are existentially related via r.

The increase in the complexity of reasoning with inverse roles and universal restrictions, can be partially explained by a new kind of interaction between these constructors. Axioms of the form A ⊑ ∃R.B and C ⊑ ∀S.D can interact in two ways. First, the following inference (2) is possible:

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):

In contrast to (2), and all inference rules in Table 2, which have only conclusions of the form A ⊑ B or A ⊑ ∃R.B, repeated applications of (3) can produce axioms of the form bigsqcap Ai ⊑ ∃R. bigsqcap Bj, where bigsqcap Ai and bigsqcap 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 allow for expressing a functional restriction for a simple role S using the constructor ⩽1S.⊤. Since, for a functional role S, the axiom C ⊑ ∃S.D implies C ⊑ ∀S.D, the following analogs of inferences (3) and (2) are possible:

In Section 4, we generalize inferences (2)-(5) and present a sound and complete system of inference rules for Horn SHIQ ontologies, which derive only consequence axioms of the form bigsqcap Ai ⊑ B and bigsqcap Ai ⊑ ∃R.(bigsqcap Bj).

4 The Calculus for Horn SHIQOntologies

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 C is simple if it is of the form ⊥, A, ∃R.A, ∀R.A, or ⩽1S.A. We denote by bigsqcap Ai a (possibly empty) conjunction of atomic concepts. The empty conjunction is abbreviated to ⊤.

Lemma 2 Every Horn SHIQ ontology O can be transformed into an ontology O′ containing only axioms of the forms: (n1) bigsqcap Ai ⊑ C, (n2) R1 ⊑ 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 O′ containing only concept inclusions of the form A1 ⊑ A2, A ⊑ st(C+), and st(C-) ⊑ A, where C+ occurs positively in O and C- occurs negatively in O. Since O is a Horn SHIQ ontology, C+ can only be of the form ⊤, ⊥, A, ¬C, C ⊓ D, ∃R.C, ∀R.C, ⩾nS.C, or ⩽1S.C, and C- only of the form ⊤, ⊥, A, C ⊓ D, C ⊔ D, ∃R.C, or ⩾1R.C.

Concept inclusions of the form A ⊑ st(C+) that are not of form (n1), are transformed to form (n1) as follows:

• A ⊑ st(¬C)=¬AC ⇒ A⊓AC ⊑ ⊥;
• A ⊑ st(⩾nS.C) = ⩾nS.AC ⇒ A ⊑ ∃S.Bi, Bi ⊑ AC, 1 ≤ i ≤ n, Bi ⊓ Bj ⊑ ⊥, 1 ≤ i < j ≤ n, where Bi are fresh atomic concepts.

Concept inclusions of the form st(C-) ⊑ A that are not of form (n1) are transformed to form (n1) as follows:

• st(C ⊔D)=AC ⊔AD ⊑ A ⇒ AC ⊑ A, AD ⊑ A;
• st(∃R.C)=∃R.AC ⊑ A ⇒ AC ⊑ ∀R-.A;
• st(⩾1S.C)=⩾1S.AC ⊑ A ⇒ AC ⊑ ∀S-.A.

It is easy to show using Proposition 1, that O′ |= α iff O |= α for every axiom α containing no new symbols.

4.2 Elimination of Transitivity

After normalization, we apply a well-known technique, which allows the elimination of transitivity axioms. Transitivity axioms of form (n3) in Lemma 2 can interact only with axioms bigsqcap Ai ⊑ ∀R.B of form (n2) through role inclusions (n3). The transformation introduces a triple of axioms (6) for every axiom bigsqcap Ai ⊑ ∀R.B of form (n1) and every transitive sub-role T of R, where BT is a fresh atomic concept:

Intuitively, BT is used to propagate B to all elements reachable from elements in bigsqcap Ai via a T -chain.

Lemma 3 Let O be consisting of axioms of forms (n1)-(n3) in Lemma 2, and O′ 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 BT and non-simple roles, we have O |= α iff O′ |= α.

Proof (sketch). It is sufficient to show that (i) every model I of O can be turned into a model J of O′ by (re-)interpreting concepts BT , and conversely, (ii) every model J of O′ can be turned into a mode 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 BT in J as (B ⊓ ∀T.B)I . Trivially, the last two axioms in (6) are satisfied in J . The first axiom in (6) is satisfied in J since J satisfies bigsqcap Ai ⊑ ∀R.B and T is a transitive sub-role of R. J satisfies the remaining axioms in O′ since they do not contain the new concepts BT .

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 O′ does not contain the transitivity axioms). It is easy to show that I satisfies all axioms (n1)-(n3). In particular, I satisfies the axioms of the form bigsqcap Ai ⊑ ∀R.B since I remains to be a model of axioms (6).

Table 3: Saturation Rules for Horn SHIQ Ontologies

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 2, and produce axioms of the form M ⊑ C and M ⊑ ∃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 ⊑O 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 O′ is called the saturation of O.

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 4 Let O be an ontology containing only axioms of the form (n1) and (n2) in Lemma 2 and O′ the saturation of O under the rules in Table 3. Then (i) O |= M ⊑ B iff M ⊑ ⊥ ∈ O′ or M ⊑ B ∈ O′ , and (ii) O |= M ⊑ ∃R.N

iff M ⊑ ⊥ ∈ O′ or there exists M ⊑ ∃R1.N1 ∈ O′ such that R1 ⊑O R and N1 ⊑ B ∈ O′ for every conjunct B in N.

Proof (sketch). It is easy to show that every axiom in O′ 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 O′ . Let Σ be the set of all conjunctions M such that M ⊑ ⊥ /∈ O′ . If Σ is empty, then M ⊑ ⊥ ∈ O′ 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 ⊑ A ∈ O′ , w ∈ Σ∗ }
• The roles are interpreted with smallest relations satisfying all role inclusions such that if M ⊑ ∃R.N ∈ O′ and M ⊑ ∃R.N ′ /∈ O′ for every super-conjunct N ′ of N, then for every w ∈ Σ∗ , either 〈wM, w〉 ∈ RI and w ∈ AI for every A ∈ N, or otherwise 〈wM, wMN〉 ∈ 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 ⊑ ∃R.N ∈ O′ 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 〈wM, wMN〉 ∈ RI implies M ⊑ ∃R1.N ∈ O′ for some R1 ⊑O R. Below we demonstrate that I is a model of O (and consequently of O′ ).

Claim 1 wM ∈ Σ+ andM ⊑ C ∈ O′ imply wM ∈ CI .

• For C = ⊥, if M ⊑ ⊥ ∈ O′ then wM ̸∈ Σ+.
• For C = A the claim follows from the definition of AI .
• For C = ∃R.B, take M ⊑ ∃R.N ∈ O′ with the largest N containing B (it exists since M ⊑ ∃R.B ∈ O′ ). By definition of RI , we have wM ∈ (∃R.N)I ⊆ CI .
• For C = ∀R.B, we show that: (i) 〈wM, wMN〉 ∈ RI implies wMN ∈ BI , and (ii) 〈wNM,wN〉 ∈ RI im-
• plies wN ∈ BI . In case (i) there is M ⊑ ∃R1.N ∈ O′ with R1 ⊑O R. Since M ⊑ C ∈ O′ and O′ is closed under R3, we have N = N ⊓ B (since N is a maximal conjunction), and so, wMN ∈ BI . In case (ii), there is N ⊑ ∃R1.M ∈ O′ with R1 ⊑O R-. Since M ⊑ C ∈ O′ and O′ is closed under R4, we have N ⊑ B ∈ O′ , and so, wN ∈ BI .
• For C = ⩽1S.B, we show that: (i) 〈wM,wMNi〉 ∈ SI and wMNi ∈ BI for i = 1, 2 implies N1 = N2, and (ii) 〈wNM,wN〉 ∈ SI , and wN ∈ BI implies 〈wNM, wNMN1〉 /∈ SI whenever wNMN1 ∈ BI . In case (i) we have M ⊑ ∃Ri.Ni ∈ O′ where Ri ⊑O S and Ni ⊑ B ∈ O′ , i = 1, 2. Since O′ is closed under R5, we have M ⊑ ∃Ri.(N1 ⊓ N2) ∈ O′ , i = 1, 2. Since each Ni is maximal for M and Ri, i = 1, 2,

we have N1 = N1 ⊓N2 = N2. In case (ii), we have N ⊑ ∃R.M ∈ O′ , R ⊑O S-, and N ⊑ B ∈ O′ . Assume to the contrary that 〈wNM, wNMN1〉 ∈ SI and wNMN1 ∈ BI . Then 〈wNM,wNMN1〉 ∈ RI 1 for some R1 ⊑O S such that M ⊑ ∃R1.N1 ∈ O′ , and wNMN1 ⊑ B ∈ O′ . Since O′ is closed under R6, we have N ⊑ ∃R1 .M ∈ O′ and N ⊑ A ∈ O for every conjunct A in N1. Hence M ⊑ ∃R1.N1 is already satisfied in wNM by its predecessor wN, and so the relation 〈wNM, wNMN1〉 ∈ RI 1 should not have been created.

Now for every axiom bigsqcap Ai ⊑ C of form (n1) in O, if wM ∈ AIi then M ⊑ Ai ∈ O′ , and so, M ⊑ C ∈ O′ by R1. By Claim 1 we then have wM ∈ CI . Thus, I satisfies every axiom bigsqcap Ai ⊑ 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 ⊑ B and M ⊑ ⊥ /∈ O′ then for every wM ∈ Σ+, we have wM ∈ BI since I is a model of O. Hence M ⊑ B ∈ O′ by definition of I. For proving (ii), if O |= M ⊑ ∃R.N and M ⊑ ⊥ /∈ O′ , then for M ∈ Σ+, we have M ∈ (∃R.N)I . Since M ∈ Σ+ does not have a predecessor in Σ+, there exists M ⊑ ∃R1.N1 ∈ O′ such that R1 ⊑O R and MN1 ∈ BI for every conjunct B in N. By definition of I, this implies that N1 ⊑ B ∈ O′ for every conjunct B in N.

Theorem 4, in conjunction with Lemmas 2 and 3, implies that our procedure based on the rules in Table 3 can be used, in particular, for computing all subsumptions A ⊑ 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 ⊑ C and M ⊑ ∃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 ExpTimehard since, e.g., Horn SHIQ contains EL with functionality), this implies that our procedure is computationally optimal.

4.5 Practical Considerations

Theorem 4 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 ⊑ ∃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 ⊑ C and A ⊑ ∃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 mediumsized ontologies such as Galen. 3 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 ⊑ ∃R.B. These dependencies are used, e.g., for expressing partonomy relations between anatomical units, for example: BasilarArtery ⊑ ∃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 ⊑ ∃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 4 using a simplified version of the rules in Table 3 for Horn SHIF ontologies, which are sufficient for Galen. We compared the results with the modelbuilding reasoners FaCT++ v.1.2.1, 5 Pellet v.1.5, 6 and HermiT v.0.9.3, 7 and the completion-based reasoner CEL v.1.0b. 8 We ran the experiments on a PC with a 2GHz Intel® Core TM 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 complexities. The Gene Ontology (GO) 9 and National Cancer Institute thesaurus (NCI) 10 are fairly big 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. GalenB with 23136 classes is based on a more recent version of Galen. 11 GalenA- and GalenB- are obtained from GalenA and GalenB by removing functionality and inverses. We have also included the results for a very large but simple ontology Snomed, which contains 389472 classes.

3 http://www.opengalen.org/

4 http://code.google.com/p/cb-reasoner/

5 http://owl.man.ac.uk/factplusplus/

6 http://clarkparsia.com/pellet/

7 http://www.hermit-reasoner.com/

8 http://lat.inf.tu-dresden.de/systems/cel/

9 http://www.geneontology.org/

10 http://www.cancer.gov/

11 http://www.co-ode.org/galen/

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.