HermiT

From semanticweb.org

HermiT
Hermit homepage
Status:	alpha
License:	LGPL
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 currently fully handles the DL SHIQ, but support for SHOIQ is planned.

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.