Prover comparison for OWL+SWRL
For OWL+SWRL ontologies, compare the reasoning performance of OWL DL and first-order reasoners for the ontology classification problem (i.e. finding all subsumptions that are a consequence of the ontology).
Support for SWRL needs to be implemented in Hets, including sublogic analysis (including OWL without restrictions), and connecting some sublogic-specific provers (e.g. ELK).