Overview

HermiT is a theorem prover for description logics (DLs) -- a family of knowledge representation formalisms with many uses. DLs have attracted considerable attention recently since provide a logical underpinning for the Ontology Web Language (OWL) -- the language for building ontologies in the Seamntic Web. For more information about description logics, please refer to The Description Logic Handbook.

The reasoner currently fully handles the DL SHIQ. The support for SHOIQ is on its way, so keep an eye on this Web page. The main supported inference is the computation of the subsumption hierarchy. More precisely, for classes C and D, HermiT can determine whether C is subsumed by D -- that is, whether KB |= C ⊆ D. HermiT can also compute the partial order of classes occurring in an ontology.

HermiT also supports description graphs -- a novel extension to DLs and OWL. For more information about description graphs, please refer to the technical report Structured Objects in OWL: Representation and Reasoning. For instructions on how to use description graphs with HermiT and other related information, please refer to this page.

HermiT implements a novel hypertableau reasoning algorithm. The main aspect of this algorithm is that it is much less nondeterministic than the existing tableau algorithms. We thus hope to obtain a truly scalable DL reasoning system suitable for application in the Semantic Web. A description of the reasoning technique for the DL SHIQ has been published at CADE 2007 in a paper called Optimized Reasoning in Description Logics using Hypertableaux.

Downloading and Compiling HermiT

HermiT's distribution is available here. The prover is available under the GNU Public License (GPL), so you can do with it whatever you want. We would appreciate it, though, if you would tell us should you find the prover useful.

HermiT has been written in Java 1.6. Please download the current version of Java SDK from Sun's Web site.

Hermit uses KAON2 as the API for loading and managing ontologies. You will need to download the current version of KAON2 from its web site and put kaon2.jar into your classpath. Please note that KAON2 is distributed under a different license agreement; please refer to KAON2's Web site for more information.

The downloaded archive contains HermiT.jar, which is a precompiled version of HermiT, and HermiT.src.jar, which contains HermiT's sources. The main class for the HermiT is org.semanticweb.HermiT.

Running HermiT on a File Ontology

Here is how you can use HermiT to check satisfiability of concepts and to classify an ontology stored in a file.

  HermiT hermit=new HermiT();

  // The following line will turn on the individual technique, described in a paper submitted to IJCAR 2008.
  // Comment this line to get the standard behavior.
  hermit.setExistentialsType(HermiT.ExistentialsType.INDIVIDUAL_REUSE);

  // The following will make HermiT print out timing information
  // during classification; you can safely turn this option off.
  hermit.setTimingOn();

  // We now load the ontology. Note that you need to speficy
  // the *URI* to the file, and not the file path.
  hermit.loadOntology("file:/C:/Temp/my_ontology.owl");

  // This is how you can check satisfiability of a concept.
  boolean result=hermit.isSatisfiable("http://my.ontology.com/#SomeObject");

  // This is how to compute the subsumption hierarchy.
  SubsumptionHierarchy subsumptionHierarchy=hermit.getSubsumptionHierarchy();

Using HermiT's API

You can use HermiT in your application through its API. HermiT operates on instances of the org.semanticweb.HermiT.model.DLOntology class. You can construct instances of this class manually and then initialize the reasoner with it. A DLOntology consists of a set of rules and ABox assertions. The classes used to repreesnt parts of a DLOntology are placed in the org.semanticweb.HermiT.model package. They way how to use them should be self-explanatory.

Here is a typical example of how you can use a DLOntology.

  // Construct a DLOntology here
  DLOntology dlOntology= ...;

  // Now construct an instance of HermiT
  HermiT hermit=new HermiT();

  // Intialize HermiT with the DLOntology
  hermit.loadDLOntology(dlOntology);

  // Now you can use the hermit instance in the same way as if the ontology were loaded from the file system
  boolean result=hermit.isSatisfiable("http://my.ontology.com/#SomeObject");
  SubsumptionHierarchy subsumptionHierarchy=hermit.getSubsumptionHierarchy();

You can serialize a DLOntology into a file using the DLOntology.save(File file) method. The resulting file will contain the seralized instance of the ontology. (Standard Java serialization is used, so the resulting file is binary and not human-readable.) You can later load the serialized ontology as follows.

  DLOntology dlOntology=DLOntology.load(new File("myFile.ser"));

Test Data

We provided several test ontologies here. This web page contains the data that we used in our papers for testing HermiT's performance.

Contact

Do not hesitate to contact any of the authors with questions about the prover. We are very happy to discuss reasoning algorithms and implementation techniques.