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 E L++ [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 E L++ 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 E L++, 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 “nondeterministic” 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 E L++. 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].
Concepts: atomic concept top concept bottom concept negation conjunction disjunction existential restriction universal restriction min cardinality max cardinality
Axioms:
Syntax
A > ? :C C u D C t D 9R:C 8R:C >nS:C 6mS:C
Semantics AI (given)
I ;
I n CI CI \ DI CI [ DI fx j RI (x; CI ) 6= ;g fx j RI (x; I n CI ) = ;g fx j jjSI (x; CI )jj ng fx j jjSI (x; CI )jj mg In this section we define the description logics SHIQ and E L+, as well as their fragments Horn SHIQ and E LH. To simplify the presentation and save space, we will not consider ABox assertions in this paper. A description logic vocabulary consists of countably infinite sets NC of atomic concepts, and NR of atomic roles. A SHIQ role is either r 2 NR or an inverse role r with r 2 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 2 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) 2 O or Tra(R ) 2 O. Given an ontology O, let R1 vO R2 be the smallest transitive reflexive relation between roles such that R1 v R2 2 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 2 NC a set AI I , and to every r 2 NR a relation rI I I . The interpretation is extended to roles by (r )I := fhx; yi j hy; xi 2 rI g and to concepts according to the right column of Table 1, where (x; U ) for 2 I I , U I , and x 2 I denotes the set fy j hx; yi 2 ^ y 2 U g, and jjV jj denotes the cardinality of a set V I . An interpretation I satisfies an axiom (written I j= ) if the respective condition to the right of the axiom in Table 1 holds; I is a model of an ontology O (written I j= O) if I satisfies every axiom in O. We say that is a (logical) consequence of O, or is entailed by O (written O j= ) 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
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, 9R:C1, 8R:C1, >nS:C1, 6mS:C2, and C2 v D1 if C occurs positively (negatively) 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, 8R:C, >nR:C with n > 1, or 6mR:C occurs negatively in O. 2.3
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(9R:C) = 9R:AC ; st(8R:C) = 8R: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 2 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 j= iff O0 j= . CR2 CR4
A v A A v B A v C
A v D A v 9r:B A v 9s:B : r v s 2 O CR3 CR5
A v B A v C
A v B A v 9r:C : B v C 2 O
: B v 9r:C 2 O A v 9r:B
A v D
B v C : 9r:C v D 2 O The description logic E L+ is one of the few description logics for which standard reasoning problems are decidable in polynomial time. E L+ allows only for concepts constructed from atomic concepts A and the top concept > using conjunction C u D and existential restriction 9r:C, where r is an atomic role. The axioms of E L+ 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 E L+ and SHIQ called E LH, which allows only for (simple) role inclusions of the form r v s. It can be easily seen that every E LH ontology is a Horn SHIQ ontology since it cannot contain concepts of the form :C, C t D, 8R:C, >nR:C, or 6mR:C.
In [5], a polynomial time classification procedure has been presented for the
description logic E L++, which extends E L+ 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 E LH.
The rules are applied to a normalised E LH ontology O that is obtained from the input
ontology by structural transformation and simplification. Structural transformation for
E LH produces only axioms of the form (
The completion rules in Table 2 derive new axioms of the form A v B and C v 9r: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
Horn SHIQ extends E LH by allowing many new constructors, notably, inverse roles, functionality restrictions, and positive occurrences of universal restrictions. These con1 In [5], instead of deriving new axioms A v B and C v 9r: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 E LH and E L++ 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 E LH can be extended to handle the new Horn SHIQ constructors.
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 8R:B , 9R :A v B:
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 v 9R:B and C v 8S:D can interact in two ways. First, the
following inference (
A v 9R:B B v 8R :D (
A v D
It is easy to see using equivalence (
A v 9S:B
C v 9S:D A u C v 9S:(B u D)
A v 61S:>
A v 9S:B B v 9S :C B v 61S :> (
A v C
In Section 4, we generalize inferences (
A v 9R:B C v 8R:D
A u C v 9R:(B u D)
(
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 9S:D implies
C v 8S:D, the following analogs of inferences (
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
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, 9R:A, 8R:A, or 61S:A. We denote by d Ai a (possibly empty) conjunction of atomic concepts. The empty conjunction is abbreviated to >.
Lemma 1. Every Horn SHIQ ontology O can be transformed into an ontology O0 containing only axioms of the forms: (n1) d 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, 9R:C, 8R:C, >nS:C, or 61S:C, and C2 only of the form >, ?, A, C u D, C t D, 9R: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 9S:Bi, Bi v AC , 1 1 i < j n, where Bi are fresh atomic concepts. i n, Bi u Bj v ?,
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 – st(9R:C) = 9R:AC v A ) – st(>1S:C) = >1S:AC v A ) AC v A, AD v A;
AC v 8R :A; ) AC v 8S :A.
It is easy to show using Proposition 1, that O0 j= containing no new symbols. iff O j= for every axiom tu 4.2
After normalization, we apply a well-known technique, which allows the elimination of
transitivity axioms. Transitivity axioms of form (n3) in Lemma 1 can interact only with
axioms d Ai v 8R:B of form (n1) through role inclusions (n3). The transformation
introduces a triple of axioms (
BT v 8T:BT
BT v B
(
Lemma 2. Let O be consisting of axioms of forms (n1)–(n3) in Lemma 1, and O0 be
obtained from O by adding axioms (
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 BT , 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 BT in J as (B u 8T:B)I . Trivially, the last two
axioms in (
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
that I satisfies all axioms (n1)–(n3). In particular, I satisfies the axioms of the form
d Ai v 8R:B since I remains to be a model of axioms (
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 9R: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 (
M v ?
N v ? R3 M v 9R1:N M v 8R2:A
M v 9R1:(N u A)
: R1 vO R2 R4 R5
M v 9R1:N1 M v 9R2:N2 M v 61S:B
N1 v B
N2 v B M v 9R1:(N1 u N2) : R1 vO S
R2 vO S
M v 9R1:N N v 8R2:A
M v A
: R1 vO R2 R6
M v 9R1:N1 M v B N1 v 9R2:(N2 u A) N1 v 61S:B N2 u A v B : R1 vO S
M v A M v 9R2 :N1 R2 vO S 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 j= M v B iff M v ? 2 O0 or M v B 2 O0, and (ii) O j= M v 9R:N iff M v ? 2 O0 or there exists M v 9R1:N1 2 O0 such that R1 vO R and N1 v B 2 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 ? 2= O0. If is empty, then M v ? 2 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 = fwM j M v A 2 O0; w 2 g – The roles are interpreted with smallest relations satisfying all role inclusions such that if M v 9R:N 2 O0 and M v 9R:N 0 2= O0 for every super-conjunct N 0 of N , then for every w 2 , either hwM; wi 2 RI and w 2 AI for every A 2 N , or otherwise hwM; wM N i 2 RI .
Intuitively, the interpretation I is a forest where nodes are labeled with non-contradictory conjunctions M 2 and every node has a successor node for every non-contradictory conjunction N 2 . Roles can connect only successive nodes in such a way that all axioms M v 9R:N 2 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 2 RI implies M v 9R1:N 2 O0 for some R1 vO R. Below we demonstrate that I is a model of O (and consequently of O0).
Claim 1 wM 2
+ and M v C 2 O0 imply wM 2 CI .
Now for every axiom d Ai v C of form (n1) in O, if wM 2 AiI then M v Ai 2 O0, and so, M v C 2 O0 by R1. By Claim 1 we then have wM 2 CI . Thus, I satisfies every axiom d 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 j= M v B and M v ? 2= O0 then for every wM 2 +, we have wM 2 BI since I is a model of O. Hence M v B 2 O0 by definition of I. For proving (ii), if O j= M v 9R:N and M v ? 2= O0, then for M 2 +, we have M 2 (9R:N )I . Since M 2 + does not have a predecessor in +, there exists M v 9R1:N1 2 O0 such that R1 vO R and M N1 2 BI for every conjunct B in N . By definition of I, this implies that N1 v B 2 O0 for every conjunct B in N . tu
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 9R: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 E L with functionality), this implies that our procedure is computationally optimal. 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 9R:N has been derived.
The above optimization not only reduces the number of inferences, but also yields a polynomial time classification procedure for E LH ontologies. Indeed, it is easy to see that for E LH 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 9R:B since those rules (including I1 and I2) never form conjunctions of several concepts. 5
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 9R:B. These dependencies are used, e.g., for expressing partonomy relations between anatomical units, for example: BasilarArtery v 9isBranchOf: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 E L+ does not exhibit this problem since it does not build models but performs inferences according to Table 2. Axioms of the form A v 9R: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 E L+.
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 ontologies, which are sufficient for Galen. We compared the results with the model-building 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 complexities. 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 E L+ 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.