-
Notifications
You must be signed in to change notification settings - Fork 3
Description
HermiT is not rejecting a sub property axiom, it is saying the construct used can only occur in an asserted axiom if it is a sub property axiom. This is on accordance with the same owl spec you quoted:
Restriction on owl:topDataProperty. The owl:topDataProperty property occurs in Ax only in the superDataPropertyExpression part of SubDataPropertyOf axioms.
There's an explanation of why the restriction exists in the page. In short, accepting such an axiom invalidates some of the owl semantics.
Pellet and FaCT++ are likely identifying the same issue and deciding to ignore the offending axiom. They might be logging messages to that effect.
It is a good point to ask for reasoners to automatically ignore such axioms - it is likely to be an useful feature. However, it is not wrong for the reasoner to throw of out.
From owlcs/owlapi#786