From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>

Date: Sat, 18 May 2002 14:43:33 +0200

To: pfps@research.bell-labs.com

Cc: "www-webont-wg" <www-webont-wg@w3.org>

Message-ID: <OF7FC1DDD0.B0914844-ONC1256BBD.0042ADD1@agfa.be>

Date: Sat, 18 May 2002 14:43:33 +0200

To: pfps@research.bell-labs.com

Cc: "www-webont-wg" <www-webont-wg@w3.org>

Message-ID: <OF7FC1DDD0.B0914844-ONC1256BBD.0042ADD1@agfa.be>

> > [...] > > > > > > 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? From the table Premise -> Conclusion ---------------------------------------------------- (1) False True False VALID UNSOUND (2) False True True VALID UNSOUND (3) True False False INVALID UNSOUND (4) True True True VALID SOUND and having that :R a [ owl:complementOf :R ] is the same proposition as not(:R a :R) we have the case not(p) -> p so only (2) or (3) are to be considered but both are UNSOUND So we aim at (4)'s but in our backing up with running cose (just FYI) we don't work with the not()'s but instead try to prove that the the premise is true and have the other rule as candidate but then we are no longer on an a so called "Euler path" and don't derive from vicious circles. > > 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. I agree, that would make no difference. It's just that we call such a non-true premise implication (and an INVALID implication) an UNSOUND proof argument. > > (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.) OK, I now see some problems, thanks. The point was to count the number of ?p instance pairs so I have to make sure to count the proof tree conclusions that are different (the cardinality of the proof tree set). I think about that infinity... -- JosReceived on Saturday, 18 May 2002 08:47:44 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:56:43 UTC
*