Hoolet1 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.
Basing the reasoner on a first order translation means that it is easy to extend the implementation to cover extensions to OWL. For example, SWRL defines a simple rule language that extends OWL.
Hoolet has been extended to handle rules through the addition of a parser for an RDF rule syntax and an extension of the translator to handle rules. This is again a straightforward translation based on the semantics of SWRL rules.
A prototype implementation of Hoolet is available for download. It consists of a graphical front end that allows loading of ontologies and rule sets, along with a reasoner. Note that this prototype is for Linux only due to the the bundled reasoner.
The application needs no installation, other than unpacking of the
archive. Once unpacked, there should be a directory
hoolet. Within that directory, the hooletGUI
script will run the application. It is used as follows:
- Give an OWL Ontology URL and load it (click the open icon). Note that this will clear the current ontology and any rules.
- (Optionally) Give a rules URL and load it. It expects any classes or properties used in the rules to be in the loaded ontology. There are samples in directory ontologies. It has a simple ontology with some of my family tree and a collection of rules.
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 (little wheel) will try and find all the people. All classes/properties etc are assumed to be in the namespace given. If it can't find classes or properties it will complain.
To activate rules, go to the rules pane and select some rules. The up and down arrows move rules between the active set to the inactive set. Any queries will be posed w.r.t the ontology and the active rules. So for example, try asking the query:
with no active rules. Answer will be NO. If you then
activate the rule about siblings, and then ask, answer will be
YES.
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.
Thanks to Andrei Voronkov and Alexandre Riazanov for permission to distribute Vampire. Note that the current implementation employs a very naive approach to the translation and should be considered an abuse of Vampire — the performance of Hoolet should not be taken as an indicator of the general performance of Vampire!
