HermiT is the only reasoner we know of that fully supports the OWL 2 standard, and that correctly reasons about properties as well as classes. It is based on a novel \hypertableau" calculus that addresses performance problems due to nondeterminism and model size|the primary sources of complexity in state-of-the-art OWL reasoners. HermiT also incorporates a number of novel optimizations, including an optimized ontology classi cation procedure. Our tests show that HermiT performs well compared to existing tableau reasoners and is often much faster when classifying complex ontologies.
HermiT is an OWL reasoning system based on a novel hypertableau calculus
[
Our tests show that HermiT is as fast as other OWL reasoners when
classifying relatively easy-to-process ontologies, and usually much faster when
classifying more di cult ontologies. Moreover, HermiT is currently the only reasoner
known to us that fully supports the OWL 2 standard: it supports all of the
datatypes speci ed in the standard, and it correctly reasons about properties as
well as about classes. Most other reasoners support only a subset of the OWL
2 datatypes [
HermiT also 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 [
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 [
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 K = (R; T ; A). All basic reasoning tasks, including subsumption checking, can be reduced to testing the satis ability of such a knowledge base. For example, K j= A v B i (R; T ; A [ fA u :B(s)g) is not satis able, where s is a \fresh" individual (i.e., one that does not occur in K).
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 (an abstraction 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, and the knowledge base K is unsatis able if and only if all choices lead to a contradiction.
Or-Branching This \case based" procedure for handing disjunctions is
sometimes 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, even
if the corresponding axiom is equivalent to a Horn clause, and so inherently
deterministic. Such indiscriminate application of the v-rule can be a major source
of ine ciency, and this has been addressed by various absorption optimizations
[2, Chapter 9], including role absorption [
HermiT's hypertableau algorithm generalizes these optimizations by rewriting description logic axioms into a form which allows all such absorptions be performed simultaneously, as well as allowing additional types of absorption impossible in standard tableau calculi. Furthermore, HermiT actually rewrites DL concepts to further reduce nondeterminism, and is thus able to apply absorptionstyle optimizations much more pervasively.
And-Branching The introduction of new individuals in the 9-rule is
sometimes called and-branching, and it is another major source of ine ciency in
tableau algorithms [
HermiT also tries to further reduce the size of the generated model using a technique called individual reuse: when expanding an existential 9R:C, it rst attempts to re-use some existing individual labeled with C to construct a model, and only if this model construction fails does it 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 the e cient handling of nominals. HermiT therefore uses an optimised nominal introduction rule that reduces nondeterminism, and is more conservative in its introduction of new nominals.
Caching Blocking Labels Anywhere blocking avoids repetitive model construction in the course of a single satis ability test. HermiT further extends this approach to avoid repetitive construction across an entire set of satis ability tests. Conceptually, instead of performing n di erent tests by constructing n di erent models, it performs 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, however, not compatible with ontologies containing nominals, 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 satis ability test is costly because it computes a substantial part of a model of the TBox; all subsequent satis ability tests reuse large parts of that model.
Classi cation Optimizations 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 subsumption tests, each of which can potentially be expensive. To obtain
acceptable levels of performance, various optimizations have been developed that
reduce the number of subsumption tests [
HermiT employs a novel classi cation procedure, and exploits the unique
properties of the system's new calculus to further optimise the procedure. In
particular, when it tries to construct a model I of K [ fA(a)g (in order to
determine the satis ability of A), HermiT is able to exploit the information in I
to derive a great deal of information about both subsumers and non-subsumers
of A, information that can be e ciently exploited by the new classi cation
procedure [
To evaluate our reasoning algorithm in practice, we compared HermiT with the
state-of-the-art tableau reasoners Pellet 2.3.0 [
We selected a number of standard test ontologies, and measured the time needed to classify them using each of the mentioned reasoners. Unlike Pellet and FaCT++, HermiT does not include a dedicated reasoner for any tractable fragment of OWL 2. Hence, we mainly focus on ontologies that exploit most or all of the expressive power available in OWL 2. All tests were performed on a 2.7 GHz MacBook Pro with 8 GB of physical memory. A classi cation attempt was aborted if it exhausted all available memory (Java tools were allowed to use 2 GB of heap space), or if it exceeded a timeout of 20 minutes.
The majority of the test ontologies were classi ed very quickly by all three reasoners. For these \trivial" ontologies, the performance of HermiT was comparable to that of the other reasoners. Therefore, we consider here only the test 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 (see Table 1 for details of these ontologies).
Table 2 summarizes the results of our tests on these \interesting" ontologies. Since HermiT has no special handling for tractable fragments of OWL 2, the perOntology Name
EMap (Feb09) GO Term DB (Feb06)
DLP ExtDnS 397
LUBM (one university) Biological Process (Feb09)
MGED Ontology RNA With Individual (Dec09)
NCI Thesaurus (Feb09)
OBI (Mar10)
FMA Lite (Feb09) FMA-constitutional part (Feb06)
GALEN-doctored GALEN-undoctored
GALEN-module1
GALEN-full
formance of HermiT on such ontologies may not be competitive. For example,
FaCT++ shows advantages when classifying ontologies which fall into a
predened syntactic fragment for which it uses a more e cient reasoning technique
[
We have described HermiT, an OWL reasoner based on novel algorithms and optimizations. HermiT fully supports the OWL 2 standard, and shows signi cant performance advantages over other reasoners across a wide range of expressive real-world ontologies. Although not always the fastest, HermiT exhibits relatively robust performance on our tested ontologies, and as shown in our results, it never failed to classify an ontology in the test corpus that was successfully handled by one of the other reasoners. HermiT also includes support for some non-standard ontology features, such as description graphs.
We are continuing to develop HermiT, and to explore new and re ned
optimization techniques. We also continue to extend its functionality: the latest
version, for example, provides support for the SPARQL 1.1 query language [
Acknowledgments This work was supported by the EU FP7 project SEALS and by the EPSRC projects ConDOR, ExODA, and LogMap.