Inverses cause false property equivalences

[ignazio1977]

phillord#8

Defining a property, another property that is inverse of the first one, and then declaring a subproperty of the first also as subproperty of the inverse of the second (which is redundant but legal) causes HermiT to think the subproperty is equivalent to the inverse. This is due to inverse property inferences based on property inclusion, but not precise enough to detect that subproperty of an inverseOf expression is not enough to guarantee bidirectional inclusion.

Example:

Prefix: : <http://example.org/>
    Ontology: <http://asdf>
    ObjectProperty: hasBigPart
        SubPropertyOf: hasPart, inverse (partOf)
    ObjectProperty: hasPart
        InverseOf:  partOf
    ObjectProperty: partOf
        InverseOf: hasPart
        Characteristics: Transitive

hasBigPart is inferred to be equivalent to hasPart. For that to be true, another inclusion is needed.

The issue is that HermiT rewrites inverseOf axioms into bidirectional, independent inclusions (so as to normalize inverses that are not written explicitly but declared via inclusions), but when it builds the inverses map it considers the appearance of one inverseOf expression sufficient to infer the bidirectional inverse relation, which would, in the example above, justify the property equivalence. However, that's wrong - both sides of the inclusion are required for this inference.

[ignazio1977]

Fix in version 5 before closing