HermiT
From semanticweb.org
| HermiT | |
|---|---|
| Hermit homepage | |
| Status: | alpha |
| Last release: | 0.9.3 (Dec 12, 2008) |
| 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.
