- 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