Surnia can check an OWL ontology/knowledge base for inconsistency and entailments. It is implemented as a wrapper around first-order theorem prover (OTTER, for now at least). Unlike Hoolet (which turns the OWL into FOL), Surnia just turns the OWL into triples and mixes in axioms.
