- From: Jeremy Carroll <jjc@hplb.hpl.hp.com>
- Date: Sat, 16 Mar 2002 15:03:28 -0000
- To: "Jonathan Borden" <jonathan@openhealth.org>, <www-webont-wg@w3.org>
Jonathan: > What about: > > :John a :Person . > :John a :Student . > > => > > :John a _:1 > _:1 owl:intersectionOf(:Person :Student) > > ? The basic rule is that the existence has to be asserted and is not part of the solipsistic entailment hence your entailment above does not hold (in my approach). The more conservative: :John a :Person . :John a :Student . _:1 owl:intersectionOf(:Person :Student) ==> :John a _:1 does hold. i.e. if we have not explicitly introduced the particular intersection into the discourse, then it is not in the discourse, and does not appear of its own accord. > > I sincerely hope that: > > owl:oneOf(a b c d) = owl:oneOf(b c d a) Of course this is true, but the solispistic entailments that show it are ones that do not involve asserting the existence of either set, but instead assume the existence of the sets. e.g. _:1 owl:oneOf(a b c d) . _:2 owl:oneOf(b c d a) . _:3 a _:1 . ==> _:3 a _:2 . which seems sufficient for set equality (at least to me). We are only talking about model theoretic entailment not deductive proof at this stage. Any model containing owl:oneOf(a b c d) and owl:oneOf(b c d a) and for which _:3 is in owl:oneOf(a b c d) will have that _:3 is in owl:oneOf(b c d a) including models that do not have any of the intermediate sets. > > and that > > owl:isEquivalentTo(x y) = owl:isEquivalentTo(y x) Yes I think so. (guessing a bit ...) in any model for which owl:isEquivalentTo(x y) the interpretation of x is the interpretation of y. Thus the interpretation of y is the interpretation of x and thus owl:isEquivalentTo(y x). (Have I got that right, or isEquivalentTo(x y) better formalized by saying that the permutation (i(x) i(y)) is (or extends to) an automorphism of the model?). Jeremy
Received on Saturday, 16 March 2002 10:03:44 UTC