- From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
- Date: Tue, 5 Mar 2002 14:43:40 +0100
- To: pfps@research.bell-labs.com
- Cc: "www-webont-wg" <www-webont-wg@w3.org>
> > > I agree that http://www.agfa.com/w3c/euler/owl-rules.n3 does not
sanction
> > > any oneOf consequences. Therefore, you will not get
> > > John a person .
> > > to imply
> > > John a [ owl:oneOf ( John ) ].
> > > from http://www.agfa.com/w3c/euler/owl-rules.n3.
> > >
> > > All this says, however, is that there are desirable inferences that
> > > http://www.agfa.com/w3c/euler/owl-rules.n3 does not sanction, i.e.,
> > > http://www.agfa.com/w3c/euler/owl-rules.n3 is incomplete.
> >
> > good point, I've added
> > { ?L owl:item ?x } log:implies { ?x a [ owl:oneOf ?L ] } .
> > so now
> > the-empty-graph
> > log:entails
> > :John a [ owl:oneOf ( :Frans :John :Mary ) ] .
> > but that still doesn't give us an empty hypothesis to entail
> > _:1 owl:oneOf ( _:2 ) .
> > I will think further...
>
> Actually it does, as this is (assuming I've got the _ and : in the right
> order) a simple existential version of part of
>
> :John a [ owl:oneOf ( :John ) ]
But here it is written in the implied consequent graph
so if one would have written the rule as
{ ?L owl:item ?x } log:implies { ?x a _:1 . _1 owl:oneOf ?L } .
and normalize (eliminate existentials) that to following rules
{ ?L owl:item ?x } log:implies { ?x a [ :skf ?L, ?x ] } .
{ ?L owl:item ?x } log:implies { [ :skf ?L, ?x ] owl:oneOf ?L } .
(using Skolem functional terms)
then the _:c owl:oneOf ( _:r ) entailment follows,
but we haven't written the rule like that...
For ``facts'' such as :John a [ owl:oneOf ( :John ) ] .
there is no problem to write them as
:John a :skc . :skc [ owl:oneOf ( :John ) .
(using Skolem constants) and we happen to also do that.
Maybe we have confused the whole thing with [ ] notation
but it is quite clear that one should not re-re-re-skolemize [ ]'s
--
Jos
Received on Tuesday, 5 March 2002 08:47:30 UTC