Hoolet

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.

Using Hoolet

Hoolet reasons over a single ontology and a collection of rules.

Loading Ontologies

Use the Ontology panel to load an OWL ontology. Type the URL of an OWL ontology into the field and click the "Open" button. There are some samples in directory ontologies.

Running Queries

To run queries, go to the Query panel. The box at the bottom allows you to type or select previously run queries. So for example typing:

and then clicking the execute button (the little wheel) will try and find all the known instances of Person. All classes and properties referred to in the query are assumed to be in the namespace given. The current implementation assumes a single namespace. If it can't find classes or properties it will complain.

Queries currently supported include:

satisfiable

Is the entire knowledge base satisfiable?

satisfiable Class

Is Class satisfiable?

subsumes Class1 Class2

Does Class1 subsume Class2?

retrieve Class

Retrieve all known instances of Class.

instance Class Individual

Is Individual an instance of Class?

same Individual1 Individual2

Are Individual1 and Individual2 known to be the same individual?

different Individual1 Individual2

Are Individual1 and Individual2 known to be different individuals?

related Individual1 Property Individual2

Is Individual1 known to be related to Individual2 via Property?

Loading Rules

To load rules, go to the Rules pane and load in rules. Type the URL of a collection of SWRL rules (represented using RDF/XML) into the field and click the "Open" button. Again there are samples in the ontologies directory.

When first loaded in, all rules are inactive. To activate rules, select them. The up and down arrows then move rules between the active set to the inactive set. Any queries will be posed with respect to the ontology and the active rules.

Formats

The application expects ontologies to be represented using OWL in RDF/XML. Rules should be in RDF using the proposed SWRL schema. The format of rules should be reasonably obvious from the samples if you want to try adding your own. This implementation has some minor restrictions:

• Class atoms in rules must be named classes. Note that this does not restrict the expressive power as we can always introduce new named classes in the ontology.

Disclaimers and Acknowledgements

We do not claim that Hoolet is, in any way an effective reasoner: our current simple approach to translation is highly unlikely to scale. However, it does provide a useful tool for use on small illustrative examples.

Thanks to Andrei Voronkov and Alexandre Riazanov for permission to distribute Vampire. Note that the very naive approach to the translation should be considered an abuse of Vampire -- the performance of Hoolet should not be taken as an indicator of the general performance of Vampire!

¹Hoolet: an old Scots word for an OWL.