|Affiliation:||University of Manchester|
Hoolet is an implementation of an OWL DL reasoner that uses a first order prover. The ontology is translated to collection of axioms (in an obvious way based on the OWL semantics) and this collection of axioms is then given to a first order prover for consistency checking.
We do not claim that Hoolet is, in any way an effective reasoner — such a naive approach is highly unlikely to scale. However, it does provide a useful tool for use on small illustrative examples.
Hoolet is implemented using the WonderWeb OWL API for parsing and processing OWL, and the Vampire prover for reasoning purposes. Other reasoners could also be used — communication with the reasoner is via the TPTP format which is understood by a number of theorem provers.