gavel-owl 0.0.2

An extension for gavel introducing OWL translations.

An extension for gavel introducing OWL translations.

Installation

pip install gavel-owl

Usage

This plugin extends gavel by a new owl dialect. This enables the various features of gavel to be used with owl ontologies. These functionalities use the java-based OWL-API. Therefore, you have to start the java backend in order to use most owl-based functionalities. The gavel-owl plugin provides a single command to do that:

python -m gavel start-server

After the server has been started successfully, you can translate an existing owl ontology to first-order logic in tptp syntax using:

python -m gavel translate owl tptp your-ontology.owl

You can also submit arguments to fist-order prover Vampire consisting of the translation of a given owl ontology as premises and conjectures formulated in tptp using:

python -m gavel owl-prove your-premises.owl your-conjectures.tptp

The running java backend can be terminated:

python -m gavel stop-server

There are several commands available that can be accessed via:

python -m gavel COMMAND [ARGUMENTS]

• start-server: starts a subprocess that connects the Python program to its Java components. Other functions such as translate will only run if this connection has been established beforehand. The optional arguments -jp and -pp can be used for custom ports. Otherwise, the default ports will be used. -jp and -pp can be used for all other commands (except prove) analogously.

• translate: A Gavel function that translates the contents of a given file from one language, e.g. OWL, to another language, e.g. TPTP. If the option –save is used, the translation is stored in the given file, else it is gets displayed in the command line.

• check-consistency: uses the OWL reasoner Hermit to determine whether a given ontology is consistent or not.

• owl-prove: takes two arguments, an OWL file and a TPTP file. It uses Vampire to prove the conjectures provided in the TPTP file based on the translation of the OWL file. If the –steps flag is set, it will return the proof steps, otherwise it will only return the reasoner’s result.

• stop-server: Ends the Java connection established by start-server.

• prove: a function from Gavel that takes the name of a FOL prover and a TPTP file and returns the prover’s result for the given problem.

For further options use:

python -m gavel [COMMAND] --help

Development

To run all the tests run:

tox

Note, to combine the coverage data from all the tox environments run:

Windows	set PYTEST_ADDOPTS=--cov-append tox
Other	PYTEST_ADDOPTS=--cov-append tox

Changelog

0.0.0 (2020-11-23)

• First release on PyPI.