|Last release:||1.3.7 (March 25, 2013)|
|Affiliation:||University of Oxford|
HermiT is a theorem prover for description logics (DLs). DLs have attracted considerable attention recently since they provide a logical underpinning for the Web Ontology Language (OWL) – the language for building ontologies in the Semantic Web. The reasoner supports all of OWL 2 DL and uses the OWL 2 Direct Semantics.
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.