- From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
- Date: Fri, 17 May 2002 21:56:42 +0200
- To: pfps@research.bell-labs.com
- Cc: "jos.deroo.jd" <jos.deroo.jd@belgium.agfa.com>, "hendler" <hendler@cs.umd.edu>, "www-webont-wg" <www-webont-wg@w3.org>
[...] > > 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 agree that we have to agree on terminology, so how would you call an argument which is based on assumptions which are false? (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 ;-) -- Jos
Received on Friday, 17 May 2002 15:57:20 UTC