Search Mailing List Archives
[protege-owl] How are Quantifiers / Cardinalities enforced by the Pellet Reasoner
tar at ISI.EDU
Thu May 22 14:32:38 PDT 2008
On May 22, 2008, at 11:47 AM, Amrit T wrote:
> I am trying to enforce quantifier / cardinality restriction in a
> simple test ontology <given below>.
> a. With the quantifiers an "existential" quantifier on the property
> requiring someValueFrom both classes 'B' and 'C' is enforced here.
> However in the instance I attach A's individual to only B's
> individual. The resoner doesnt point this out as an inconsistency.
> Why is that?
Because you are not thinking of the restrictions in the proper OWL
way. They are not just constraints, but also INFERENCE RULES. So,
unless you actually have some way of proving that B's individual
CANNOT logically be of type C, then Pellet will in fact, infer that
the individual belongs to class C as well as B. The information that
you provide can be used for inference, and that is what the system does.
> Also if I dont use this property to attach to any of the
> individuals, I only get a red box but still no reasoner
> inconsistency by doing "Check Consistency".
That is because of the open world reasoning assumption. Just because
a value is not asserted in the ontology, it doesn't mean that the
assertion is false. So OWL is quite happy knowing that there is a
filler of the property (which is an inference from the existential
restriction), even if it doesn't happen to know which particular
instance is that filler. One of the expressive power benefits of OWL
is that the reasoner can operate with such vague knowledge that there
is a filler. It doesn't have to be grounded in a concrete individual.
> b. Cardinality restriction of say at least one such relation are not
> detected by the reasoner as an inconsistency if there are no such
> relations. Again what I get is a red box surrounding the widget.
> I am sure there is something wrong in my approach. Please advise.
See above. This is the designed behavior of OWL. The red box is just
a user interface aid and legacy of the Protege frames language.
Consider it a reminder that a filler is present, but unknown. It is
NOT an error or inconsistency.
To get an inconsistency, an OWL reasoner has to be able to prove that
no such individual filler CAN exist. That is much harder to do than
just not knowing what the filler is.
More information about the protege-owl