Re: more on a same-syntax extension from RDF(S) to OWL

> > > 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