HermiT
From semanticweb.org
| HermiT | |
|---|---|
| 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 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.
