From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Sat, 18 May 2002 06:29:23 -0400

To: jos.deroo.jd@belgium.agfa.com

Cc: www-webont-wg@w3.org

Message-Id: <20020518062923Y.pfps@research.bell-labs.com>

Date: Sat, 18 May 2002 06:29:23 -0400

To: jos.deroo.jd@belgium.agfa.com

Cc: www-webont-wg@w3.org

Message-Id: <20020518062923Y.pfps@research.bell-labs.com>

From: "Jos De_Roo" <jos.deroo.jd@belgium.agfa.com> Subject: Re: ISSUE: DAML+OIL semantics is too weak Date: Fri, 17 May 2002 21:56:42 +0200 > [...] > > > > 1) there is one thing I would like to reiterate > > > suppose we have a paradoxical pair such as e.g. > > > > > > I1 = { ?x a :R } log:implies { ?x a [ owl:complementOf ?x ] } . > > > I2 = { ?x a [ owl:complementOf ?x ] } log:implies { ?x a :R } . > > > > This says that a resource belongs to :R iff it does not belong to itself. > > > > So, does :R belong to :R, and what can be gained from this? > > Well, if :R belongs to :R then :R does not belong to :R, which cannot be, > > so no model of the above has :R belonging to :R. > > However, if :R does not belong to itself then :R belongs to :R, which > > cannot be, so no model of the above has :R not belonging to :R. > > Therefore the two implications above have no models. > > > > > then deriving a contradiction from that is indeed a > > > VALID inference but it is not a SOUND inference and > > > > The above reasoning is SOUND. > > SOUND reasoning means that the derived formulae semantically follow from > > the assumptions, i.e., that if you can derive X from A1, ..., An, > > then A1, ..., An entails X. But I1, I2 has no models, so I1, I2 entails X > > for any X, so deriving any X from I1, I2 is indeed SOUND reasoning. > > All we wanted to say is that > { :R a [ owl:complementOf :R ] } log:implies { :R a :R } . > or simplified > :R a :R . > > could be argued, but ***according to that rule*** the > premise is FALSE and we (in our oldfashioned mode) > call that an UNSOUND argument (although it is VALID) > and we avoid such derivations. I have no idea what the distinction you are getting at here is. There are several possibilities that I see. 1/ A valid implication, like a -> a v b, but the premise is not true, so the conclusion might not be. An argument that purports to derive a v b is incorrect, and any proof system that would sanction it is unsound. 2/ A not-valid implication, like a -> a ^ b, but the premise is true. An argument that purports to derive b is again incorrect, and any proof system that would sanction it is unsound. Neither seems to fit. Could you please clarify your meaning for me? > I agree that we have to agree on terminology, so how > would you call an argument which is based on assumptions > which are false? Incorrect, or maybe unsound, but I don't see any difference between this kind of argument and an argument that uses an incorrect inference. Maybe you are making a distinction between an argument that uses an invalid implication and an argument that uses a non-true premise. However, there is little difference between the two, as the non-true premise could be the invalid implication. > (and which is something we should avoid I think, > otherwise "if I see 2 suns, my aunt is a car" > and also in case of true premises we can simplify a > proof argument to its conclusion or T -> C as C) > > > 2) yes, more desirable consequences should follow > > > from more implications, but also there should > > > be more rules for deriving inconsistencies > > > such as e.g. > > > > > > { :rule16r1 . > > > ?s ?p ?o . > > > ?s a [ a owl:Restriction; > > > owl:onProperty ?p; > > > owl:minCardinality ?min; > > > owl:maxCardinality ?max; > > > owl:toClass ?C ] . > > > { ?s ?p ?o . ?o a ?C } math:entailCount ?n . > > > ?n math:lessThan ?min > > > } > > > log:implies > > > { ?s :inconsistentWith owl:Restriction } . > > > > > > where math:entailCount is just something to count > > > how many times we can entail its subject graph > > > from what was given > > > > The above DAML+OIL restriction says that the set of resources that have > > atleast ?min fillers for ?p that belong to ?C is the same as the set of > > resources that have atmost ?max fillers for ?p that belong to ?C. From > > this weird restriction lots of unusual consequences result. I think that > > it would be much better if you revised your example to eliminate the > > weirdness. I can't determine what is supposed to be happening here > otherwise. > > Oops, that second line > ?s ?p ?o > is there too much, as are other things, so something like > > { :rule16r1 . > ?s a [ a owl:Restriction; owl:onProperty ?p; owl:minCardinality ?min ] . > { ?s ?p ?o } math:proofCount ?n . > ?n math:lessThan ?min } > log:implies > { ?s :inconsistentWith owl:Restriction } . > > (but I have to check with running code and reread DAML+OIL ASAP) > > > Also, I have no idea what > > > > > how many times we can entail its subject graph > > > > means. > > > > Entailment just is, it is not a process that can be performed a number of > > times. > > Well again "proof argument" wise, this is in the sense of > "how many proof trees can we find for { ?s ?p ?o }" > and that number should be less than ?min > Naming things such as math:proofCount > seems to be the more difficult job ;-) Well, if { ?s ?p ?o } follows from some assumptions, most proof systems will have an infinite number of proof trees for it, so I still don't understand what you are getting at here. (It may be that you are trying to say that if ?s has too few known ?p-fillers, then there is a contradiction, but this does not follow, nor do many of its variants follow.) > -- > Jos peterReceived on Saturday, 18 May 2002 06:29:37 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:57:50 GMT
*