HermiT is a new OWL reasoner based on a novel \hypertableau" calculus. The new calculus addresses performance problems due to nondeterminism and model size|the primary sources of complexity in state-of-the-art OWL reasoners. The latter is particularly important in practice, and it is achieved in HermiT with an improved blocking strategy and and an optimization that tries to reuse existing individuals rather than generating new ones. HermiT also incorporates a number of other novel optimizations, such as a more e cient approach to handling nominals, and various techniques for optimizing ontology classi cation. Our tests show that HermiT is usually much faster than other reasoners when classifying complex ontologies, and it is already able to classify a number of ontologies which no other reasoner has been able to handle.
Reasoning services for Description Logic ontologies, such as subsumption testing
and classi cation, are usually performed by testing the consistency of a
number of knowledge bases derived from the original ontology [
HermiT is a Description Logic reasoning system based on an entirely new architecture which addresses both of these sources of complexity. HermiT implements a \hypertableau" calculus which greatly reduces the number of possible models which must be considered (down to only a single possibility for a significant subset of ontologies). HermiT also incorporates the \anywhere blocking" strategy, which limits the sizes of models which are constructed. Finally, HermiT makes use of a novel and highly-e cient approach to handling nominals in the presence of number restrictions and inverse roles; we expect that this will allow ontology authors to make much freer use of nominals than has been possible to date. This combination of fundamental algorithmic improvements also enables a range of additional optimizations.
Our tests show that HermiT is as fast as other DL reasoners when classifying relatively easy-to-process ontologies, and usually much faster when classifying more di cult ontologies. In fact, HermiT can classify a number of ontologies which no other reasoner has previously been able to handle.
The HermiT system also serves as a platform for prototypical
implementations of new language features. For example, HermiT already includes support
for reasoning with ontologies which include description graphs [
HermiT is available as an open-source Java library, and includes both a Java API and a simple command-line interface. We use the OWL API both as part of the public Java interface and as a parser for OWL les; HermiT can process ontologies in any format handled by the OWL API, including RDF/XML, OWL Functional Syntax, KRSS, and OBO. 2
On OWL ontology O can be divided into three parts: the property axioms, the class axioms, and the facts. These correspond to the RBox R, TBox T , and ABox A of a Description Logic knowledge base. 2.1
To show that a knowledge base K = (R; T ; A) is satis able, a tableau algorithm constructs a derivation|a sequence of ABoxes A0; A1; : : : ; An, where A0 = A and each Ai is obtained from Ai 1 by an application of one inference rule. The inference rules make the information implicit in the axioms of R and T explicit, and thus evolve the ABox A towards a (representation of a) model of K. The algorithm terminates either if no inference rule is applicable to some An, in which case An represents a model of K, or if An contains an obvious contradiction, in which case the model construction has failed. The following inference rules are commonly used in DL tableau calculi.
{ t-rule: Given (C1 t C2)(s), derive either C1(s) or C2(s). { u-rule: Given (C1 u C2)(s), derive C1(s) and C2(s). { 9-rule: Given (9R:C)(s), derive R(s; t) and C(t) for t a fresh individual. { 8-rule: Given (8R:C)(s) and R(s; t), derive C(t).
{ v-rule: Given an axiom C v D and an individual s, derive (:C t D)(s). The t-rule is nondeterministic: if (C1 t C2)(s) is true, then C1(s) or C2(s) or both are true. Therefore, tableau calculi make a nondeterministic guess and choose either C1 or C2 If choosing C1 leads to a contradiction, the algorithm must backtrack and try C2; this procedure is known as reasoning by case. The knowledge base K is unsatis able if and only if all choices fail to construct a model. We next discuss several sources of complexity in this procedure, and how HermiT addresses them. (i) (ii) (iii) (iv) a0
R b1
R
a1 :A 8R::A t A 8R::A t A 8R::A t A 8R::A :A 8R::A 8R::A :A an 1
R bn
R an
A 8R::A t A 8R::A t A 8R::A t A 8R::A :A 8R::A
:A 8R::A :A Or-Branching Handing disjunctions through reasoning by case is often called or-branching. The v-rule is the main source of or-branching, as it adds a disjunction for each TBox axiom to each individual in an ABox and can be a major source of ine ciency [1, Chapter 9]. For example, let T1 and A1 be a TBox and an ABox as speci ed in (1).
T1 = f9R:A v Ag A1 = f:A(a0); R(a0; b1); R(b1; a1); : : : ; R(an 1; bn); R(bn; an); A(an)g (1) The ABox A1 is graphically shown in Figure 1. The individuals occurring in the ABox are represented as black dots, an assertion of the form A(a0) is represented by placing A next to the individual a0, and an assertion of the form R(a0; b1) is represented as an R-labeled arrow from a0 to b1. Initially, A1 contains only the concept assertions shown in line (i ).
To satisfy the axiom in T1, a tableau algorithm applies the v-rule, thus adding
the assertions shown in line (ii ) of Figure 1. Tableau algorithms are usually free
to choose the order in which they process the assertions in an ABox; tableau
systems often use advanced heuristics to try to nd an order that exhibits good
performance in practice [
The axiom 9R:A v A, however, is not inherently nondeterministic: it is equivalent to the Horn clause R(x; y) ^ A(y) ! A(x), which can be applied bottom-up to derive the assertions A(bn); A(an 1); : : : ; A(a0) and reveal a contradiction on a0. These inferences are deterministic, so we can conclude that K1 is unsatisable without any backtracking. This example suggests that the processing of TBox axioms in tableau algorithms can be unnecessarily nondeterministic.
Various absorption optimizations [1, Chapter 9] have been developed to
address this problem. The basic absorption algorithm tries to rewrite TBox axioms
into the form B v C where B is an atomic concept. Then, instead of deriving
:B t C for each individual in an ABox, C(s) is derived only if the ABox
contains B(s); thus, the absorbed axioms can be applied in a \more deterministic"
way. This technique has been extended in several ways. Role absorption [
HermiT's hypertableau algorithm generalizes these absorption optimizations by rewriting description logic axioms into a form which allows standard absorption, role absorption, and binary absoprtion to be performed simultaneously, as well as allowing additional types of \absorption" impossible in standard tableau calculi. In the hypertableau calculus, an axiom A u B u 9R:C v D would only introduce D(s) if the ABox already contained A(s), B(s), R(s; t), and C(t) for some t. Furthermore, HermiT actually rewrites DL concepts to further reduce nondeterminism. Testing satis ability of the concept :A t B causes nondeterministic application of the t-rule in standard tableau reasoners; HermiT transforms this concept into an expression equivalent to A v B, and is thus able to apply absorption-style optimizations much more pervasively than standard tableau reasoners can.
And-Branching The introduction of new individuals in the 9-rule is called
andbranching, and it is another major source of ine ciency in tableau algorithms
[
T2 = f A0 v A2 = f A0(a) g 2 S:A1; : : : ; An 1 v 2 S:An; An v A1 g (2)
At-least restrictions are dealt with in tableau algorithms by the -rule, which is quite similar to the 9-rule: from n R:C(s), the -rule derives R(s; ti) and C(ti) for 1 i n, and ti 6 tj for 1 i < j n. Thus, the assertion A0(a) implies the existence of at least two individuals in A1, each of which imply the existence of at least two individuals in A2, and so on. Given K2, a tableau algorithm thus constructs a binary tree, shown in Figure 2a. Each individual at depth n is an instance of An; because of the GCI An v A1, this individual a S
S S
S
S
S (a) Without blocking (b) Ancestor Blocking
(c) Anywhere Blocking must be an instance of A1 as well, so we can repeat the whole construction and generate an even deeper tree. Clearly, a nave application of the tableau rules does not terminate if the TBox contains existential quanti ers in cycles.
To ensure termination in such cases, tableau algorithms employ blocking [
Standard tableau algorithms only allow individuals to be blocked by their ancestors|this is called ancestor blocking. This causes the derivation for K2 to terminate but results in the exponentially-large construction shown in Figure 2b, where blocking is indicated by dashed lines. HermiT extends this blocking strategy such that an individual can be blocked by (almost) any other individual. On K2 our improved anywhere blocking approach results in the construction shown in Figure 2c. Anywhere blocking can reduce the size of generated models by an exponential factor, and this substantially improves real-world performance on many di cult and complex ontologies.
Although anywhere blocking can often prevent the creation of multiple copies of identical individuals, it is not uncommon for tableau procedures to produce models containing a great many very similar individuals. If an expression 9R:C occurs in di erent parts of a partially-constructed model, then multiple individuals labeled with C will be created, and if the structures surrounding these new individuals di er in any way then one will not block the other. In many cases this results in unnecessary replication. HermiT takes advantage of this observation through individual reuse: when we expand an existential 9R:C we rst attempt to re-use some existing individual labeled with C to construct a model, and only 1 The de nition of \identical" depends upon the logic used. if this model construction fails do we introduce a new individual. This approach allows HermiT to consider non-tree-shaped models, and drastically reduces the size of models produced for ontologies which describe complex structures, such as ontologies of anatomy. \Reused" individuals, however, are semantically equivalent to nominal concepts, and thus performance gains due to individual reuse are highly dependent upon e cient handling of nominals.
Nominal Generation In logics which include both inverses and number restrictions, nominal concepts|concepts which refer to a particular individual in the ABox|make the blocking rules more complex. Because each nominal has a unique identity, it cannot be copied, and thus cannot appear in a part of a subtree which occurs multiple times in a model due to blocking. In fact, the combination of inverse roles and number restrictions can limit the number of neighbors of a nominal node, making them \unique" and uncopyable as well; these neighbors can impose uniqueness constraints on neighbors of neighbors, and so on. In order to ensure the correctness of blocking, it is necessary to identify precisely which individuals can be copied and which are unique.
Standard tableau algorithms identify unique individuals, called root individuals, recursively, beginning with the individuals in the initial ABox. Whenever there are number restrictions and inverse roles which limit the number of neighbors of such a root individual, the tableau N N -rule guesses exactly how many such neighbors will exist in the nal model and constructs an appropriate number of root individuals. Number restrictions on these new individuals can cause another application of the N N -rule to produce new root neighbors-of-neighbors, and so on. This procedure will eventually terminate, but each possible \guess" for each N N -rule application must be explored if a model cannot be found, and each application can produce a large number of new individuals, leading to larger models. A single large number in a number restriction can make reasoning using the N N -rule completely impractical.
HermiT addresses this problem by replacing the N N -rule with an N I-rule which does not introduce new root individuals but instead simply labels existing individuals as roots. By keeping track of unique identi ers for each root individual this approach is able to ensure correctness of the algorithm without increasing the sizes of the models constructed. 2.2
DL reasoning algorithms are often used in practice to compute a classi cation
of a knowledge base K|that is, to determine whether K j= A v B for each pair
of atomic concepts A and B occurring in K. Clearly, a nave classi cation
algorithm would involve a quadratic number of calls to the subsumption checking
algorithm, each of which can potentially be highly expensive. To obtain
acceptable levels of performance, various optimizations have been developed that
reduce the number of subsumption checks [
satis ability of a concept A in knowledge base K, HermiT creates the knowledge base K0 = K [ fA(a)g, where a is a new individual, and attempts to construct a model of K0. If A is satis able, then the construction will yield a model I. HermiT is able to exploit the information in I to derive information about A beyond its satis ability.
If the assertion B(a) does not occur in I, then it is clearly possible for an individual to be a member of A without being a member of B, thus we can conclude A 6v B. If the assertion B(a) does occur in I, and the derivation of B(a) does not depend on any nondeterministic choice (and thus B(a) would appear in any model), this proves that A v B. HermiT's ability to minimize nondeterminism often makes it possible to perform most of the classi cation of a concept A using only a single satis ability check.
Caching Blocking Labels HermiT's anywhere blocking technique, described in Section 2.1, avoids the creation of identical sub-models in the course of a consistency test; we further extend this approach to avoid the creation of identical sub-models across an entire set of consistency tests. Conceptually, instead of performing n di erent tests by constructing n di erent models, we perform a single test which constructs a single model containing n independent fragments. Although no two fragments are connected, the individuals in one fragment can block those in another, greatly reducing the size of the combined model.
In practice, tests are not actually performed simultaneously. Instead, after each test a compact representation of the model generated is retained for the purpose of blocking in future tests. This nave strategy is not compatible with ontologies containing nominals, however, which could connect the models from independent tests.
This optimization has been key to obtaining the results that we present in Section 3. For example, on GALEN only one subsumption test is costly because it computes a substantial part of a model of the TBox; all subsequent subsumption tests reuse large parts of that model. 2.3
HermiT includes some nonstandard functionality that is currently not available
in any other system. In particular, HermiT supports reasoning with ontologies
containing description graphs. As shown in [
We selected test ontologies from the Gardiner ontology suite [
We measured the time needed to classify each test ontology using all of the mentioned reasoners. All tests were performed on a 2.2 GHz MacBook Pro with 2 GB of physical memory. A classi cation attempt was aborted if it exhausted all available memory (Java tools were allowed to use 1.5 GB of heap space), or if it exceeded a timeout of 20 minutes.
The majority of the test ontologies were classi ed in under a second by HermiT, and under ten seconds by Pellet and FaCT++. For these \trivial" ontologies, the performance of HermiT was comparable to that of the other reasoners. Therefore, we consider here only the tests results for \interesting" ontologies| that is, ontologies that are either not trivial or on which the tested reasoners exhibited a signi cant di erence in performance.
Table 1 summarizes the results of tests on the \interesting" ontologies. In most cases, HermiT performs as well as or better than the other reasoners.
HermiT performs worse than Pellet and FaCT++ on the DLP ExtDnS ontology. This ontology includes a substantially more complex RBox than most other ontologies in the test suite, with 384 role axioms. The tested version of HermiT implements transitivity through axiom rewriting; our analysis revealed that HermiT's poor performance on DLP ExtDnS is due to ine ciencies in this rewriting. We are currently working to develop more e cient role encodings.
HermiT also performs worse than Pellet and FaCT++ on the MGED ontology. This ontology contains nominals, as well as a moderately complex ABox (over 600 assertions). Since the ontology uses nominals, the ABox must be taken into account when classifying the ontology. HermiT is not yet optimized for ABox reasoning.
Di erent versions of GALEN have commonly been used for testing the
performance of DL reasoners. The full version of the ontology (called GALEN-full)
cannot be processed by any of the reasoners. To simplify the ontology, we
extracted a module (called GALEN-module1) from GALEN-full using the
techniques from [
no reasoner was able to classify it either. Similarly, no reasoner could classify FMA-constitutional part. Our analysis has shown that, due to a large number of cyclic axioms, on these ontologies reasoners construct extremely large ABoxes and eventually exhaust all available memory. Our individual reuse technique is designed to address this issue; the above tests were conducted using a version of HermiT which did not include this optimization.
Because of the failure of DL reasoners to process GALEN-full, various simpli ed versions of GALEN have often been used in practice. As Table 1 shows, these ontologies are still challenging for state-of-the-art reasoners. HermiT, however, can classify them quite e ciently; in fact, HermiT is the only reasoner that can classify GALEN-original. All the other reasoners, including HermiT-Anc, quickly run out of memory on GALEN-original; this suggests that, by drastically reducing the sizes of generated ABoxes, anywhere blocking can mean the di erence between success and failure on complex ontologies.
On ontologies that can be processed by both HermiT and HermiT-Anc, both reasoners show comparable performance, suggesting that the ABoxes generated on these ontologies are not particularly large. On some of these ontologies (e.g., BP XP OBOL and OWL Guide Food), other reasoners can perform signi cantly more slowly; this suggests that the increase in HermiT's performance is mainly due to the hypertableau rule application strategy and reduced nondeterminism. Thus, while the hypertableau strategy may not be as important as anywhere blocking in determining the practical limits of DL reasoners, it can still lead to signi cant performance improvements in practice.
We have described HermiT, a new reasoner for SHOIQ+ (and OWL) based on novel algorithms and optimizations. HermiT shows signi cant performance advantages over other reasoners across a wide range of real-world ontologies. In several cases, HermiT is able to classify ontologies that no other reasoner can process. HermiT also includes support for some non-standard ontology features, such as description graphs.
We intend to continue to develop HermiT to track the emerging OWL 2.0 standard, including extended datatype support. We expect the performance of HermiT to continue to improve as we re ne our optimization techniques, including the development of heuristics to maximize the bene t of our individual reuse technique.
In our future work, we intend to extend the ABox reasoning capabilities of HermiT with both a more expressive ABox query interface as well as new optimization techniques which allow reasoning with extremely large ABoxes.