Why HermiT considers asymmetric sub-property to symmetric property consistent?

Question

Following the definition of symmetric and asymmetric properties in OWL 2 and the explanation in Inheritance of property characteristic by sub-properties I would assume that the declaration of an asymmetric property as sub-property to a symmetric property would result in an inconsistency detected by the reasoner (HermiT 1.3.8.413), but that is not the case in Protégé 5.2.0. Any explanations for this?

HermiT infers from the assertions below correctly the range of :isNeighbourto be :Word and :W1 :isNeighbour :W2, and detects an inconsistency when :W1 :folllows :W2. The same is true for Pellet and Fact++ 1.6.5 in Protégé 5.2.0.

:isNeighbour a owl:SymmetricProperty; rdfs:domain :Word . 
:follows a owl:AsymmetricProperty; rdfs:subPropertyOf :isNeighbour . 
:W1 a :Word . 
:W2 a :Word . 
:W2 :follows :W1 .

This code seems to be a sensible formal representation of text (words are (symmetric) neighbours when they follow each other (asymmetric)), but in the definition of OWL it seems to be inconsistent as every assertion using the property :follows should consistently allow the assertions made with the superclass :isNeighbour. I'm not sure if the Reasoners are just less strict than OWL or I've a misunderstanding of OWL.

Answer 1

Some property characteristics are "top-down inherited" through property hierarchy, whereas some are not:

• P rdfs:subPropertyOf Q means ∀x∀y(P(x,y) → Q(x,y)) (1)

• Q a owl:SymmetricProperty means ∀x∀y(Q(x,y) → Q(y,x)) (2)

Do (1) and (2) entail ∀x∀y(P(x,y) → P(y,x))? You have already find a countermodel. You could replace "words" with "natural numbers" for solidity.

Actually, symmetricity is "down-top inherited".

P.S. Demystifying OWL for the Enterprise by M. Uschold says that the subproperty of a symmetric property is symmetric, which is not correct.