Is there a difference in OWL between using inverseOf and propertyChainAxiom ([inverseOf <property>])?

Question

Take the following statements as an example:

@base           <http://ex.org/> .
@prefix owl:    <http://www.w3.org/2002/07/owl#> .

<hasPart> a owl:ObjectProperty .
<compatibleWith> a owl:ObjectProperty .

<main> owl:differentFrom <part> .

<main> <hasPart> <part> .

I can reason that <part> is compatibleWith <main> by adding one of these two statements

<compatibleWith> owl:propertyChainAxiom( [owl:inverseOf <hasPart>] ) .

or

<compatibleWith> owl:inverseOf <hasPart> .

In my opinion do these two statements differ semantically for a human, as compatibility is not really an inverse of having a part. The first would rather state if there is a hasPart relationship there is also a compatibleWith relationship in the other direction.

However, I wonder if for a OWL reasoner these two statements are basically equivalent, beside adding the blank node and propertyChainAxiom statment.
Are there additional thinks I could (and maybe do not want to) reason with one statement but not the other?

Answer 1

The difference becomes clear when for example:

<compatibleWith> a owl:SymmetricProperty .

is added.

Using

<compatibleWith> a owl:SymmetricProperty .
<compatibleWith> owl:inverseOf <hasPart> .

also reasons the inverse here:

<part> <hasPart> <main> .

Following up with <hasPart> a owl:InverseFunctionalProperty might even lead to errors if certain parts are different.

---

<compatibleWith> a owl:SymmetricProperty .
<compatibleWith> owl:propertyChainAxiom( [owl:inverseOf <hasPart>] ) .

Does NOT reason that <part> <hasPart> <main> . making a crucial difference here.