From semanticweb.org.edu
Jump to: navigation, search
Hermit homepage
Status: stable
Last release: 1.3.7 (March 25, 2013)
License: LGPL
Affiliation: University of Oxford

HermiT is a theorem prover for description log.css (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 Semant.css.

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.