subproperty of inverse object property expression triggers HermiT bug

[balhoff]

There is a HermiT bug related to handling a subproperty axiom where the superproperty is an inverse expression: phillord/hermit-reasoner#8

In RO http://purl.obolibrary.org/obo/ro/releases/2018-05-11/ro.owl capable of and enables are inferred by HermiT to be equivalent to each other.

To see this you need to classify RO with HermiT in Protege, and wait quite a while for it to complete (maybe an hour or so... I didn't pay close attention).

'enables' is asserted to be a subproperty of 'capable of'.

'enabled by' (inverse of 'enables') is asserted to be a subproperty of inverse('capable of'). That is the trigger for the HermiT bug. I'm not sure that we need this axiom, and we should probably avoid this pattern until the bug in HermiT is fixed.

If you remove that axiom, and create a new property X, and assert X to be the inverse of 'capable of', and 'enabled by' to be a subproperty of X, then the equivalence is not inferred.

[balhoff]

Note: making this change also dramatically reduces reasoning time to 1 minute or less.

Edit: That was the case for the data file I was looking at which contained a subset of RO. The full RO still takes a while to classify.

[cmungall]

Interesting! We use hermit as part of the release process, but we do not explicitly ask for things like equivalent OPs so we miss this (and this is presumably why it takes seconds rather than hours).

We need to overhaul the RO release process to use ROBOT, I see we are still using OORT.. Also this points to additional checks for ROBOT. We already do a test for "unsatisfiable" OPs which is non-standard but turns out to be really useful (e.g. #233) we should make sure we are comprehensive with OP tests, eg. testing for equivalence

[balhoff]

Subproperty of an inverse expression is also used with anabranch of. But it seems to be okay, I guess because it doesn't itself have an inverse.