gavel-owl 0.2.0

An extension for gavel introducing OWL translations.

An extension for Gavel introducing OWL and FOWL (OWL with FOL annotations) translations as well as related functionality regarding OWL and FOWL ontologies.

Installation

The latest released version can be installed with:

pip install gavel-owl

The latest development version can be installed with:

pip install git+https://github.com/gavel-tool/python-gavel-owl.git@dev

For the development version, you need to install the jar-file manually. This is done by running mvn install in the java directory. Copy the resulting jar-file from java/target/java-1.0-SNAPSHOT.one-jar.jar to src/gavel_owl/jars/api.jar (be sure to use the one-jar-file, not the regular jar-file).

Usage

This plugin extends gavel by two new dialects, owl and fowl. This enables the various features of gavel to be used with owl / fowl 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

In order to translate an owl ontology with first-order annotations into tptp syntax, you can use:

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

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. The following options are avaiable for translate:

  • --clif-properties (only for input dialect fowl) This option accepts arbitrary many IRIs or labels of OWL annotation properties. The values of annotation axioms using these properties will be interpreted as CLIF axioms. If this option is set with no arguments, the tool will not look for any CLIF axioms. If this option is not set, it will default to https://github.com/gavel-tool/python-gavel-owl/clif_annotation as an annotation property.

  • --tptp-properties (only for input dialect fowl) This is analogous to clif-properties. Here, the default value is https://github.com/gavel-tool/python-gavel-owl/tptp_annotation.

  • --shorten-names -n If this flag is set, the short form of IRIs will be used.

  • --readable-names (only for input dialects fowl and owl) This flag replaces IRIs with labels (if available) or shortened IRIs.

  • --no-annotations -a This flag can be set to avoid rendering annotations in the output dialect. For the translation from fowl to tptp, these annotations contain the OWL axiom or FOL annotation the is the origin of the corresponding FOL axioms.

  • --jp (only for input dialects fowl and owl) Sets the Java port for the connection to FOWL’s Java server. This should be the same number used for start-server. The default value is 25333.

  • --pp (only for input dialects fowl and owl) Sets the Python port for the connection to FOWL’s Java server. This should be the same number used for start-server. The default value is 25334.

  • --verbose -v (only for input dialect fowl) If this flag is set, additional information on the translation process will be put in the command line, such as the mapping between OWL entities and FOL names.

  • --save -s This option specifies the path for saving the translation result. If save is not set, the result will be put out to the command line.

  • --save-dol (only for input dialect fowl) This argument can be used to set a path under which to store the DOL-file generated from the annotated ontology.

  • --tptp-input (only for input dialect fowl) Use this argument in combination with one or multiple filenames to add TPTP files to the ontology. The axioms in these files are treated like TPTP annotations.

  • --clif-input (only for input dialect `` fowl``) Similar to --tptp-input, but for CLIF files. CLIF annotations are ignored. Advanced features such as imports or modules are not supported.

• 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.

• prove-ontology-entailment: Checks if an OWL ontology can be entailed from another. It returns the result based on OWL reasoning and based on FOL reasoning using the fowl translation.

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.