- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Mon, 20 May 2002 13:35:08 -0400
- To: jos.deroo.jd@belgium.agfa.com
- Cc: www-webont-wg@w3.org

From: "Jos De_Roo" <jos.deroo.jd@belgium.agfa.com> Subject: Re: ISSUE: DAML+OIL semantics is too weak Date: Mon, 20 May 2002 19:17:45 +0200 > > > > a/ ?x a :R -> ?x a [ owl:complementOf ?x ] > > > > b/ ?x a [ owl:complementOf ?x ] -> ?x a :R > > > > > > > > have been derived. > > > > > > > > Now assume that > > > > Ac/ :R a :R > > > > (Why? Well because this is how this proof theory makes progress.) > > > > > > > > Then from modus ponens, a/ and Ac/ > > > > Ad/ :R a :R > > > > follows. > > No, it is :R a [ owl:complementOf :R ] > that follows per MP > :R a :R > ?x a :R -> ?x a [ owl:complementOf ?x ] > |- > :R a [ owl:complementOf :R ] My messages http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0143.html and http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0146.html read Ad/ :R a [ owl:complementOf :R ] on the line that you quote as > > > > Ad/ :R a :R How did that get changed in your message? > > > > But our theory includes the implication > > > > ?x a ?y , ?x a [owl:complementOf :y] -> FALSE > > > > so using modus ponens again > > > > Ae/ FALSE > > OK per MP > :R a :R > :R a [ owl:complementOf :R ] > ?x a ?y , ?x a [owl:complementOf :y] -> FALSE > |- > FALSE > > > > > Now the proof theory allows the deduction of the opposite of the > > > > assumption, so > > > > f/ not ( :R a :R ) > > > > follows. > > which is :R a [ owl:complementOf :R ] > but you had derived that already > assuming :R a :R I guess I was not clear enough. Being more explicit, the proof would proceed along the following lines: | :R a :R Assumption | :R a [ owl:complementOf :R ] From a/, using modus ponens | FALSE From ?x a ?y, ?x a [owl:complementOf :y] -> FALSE :R a :R -> FALSE Discharging the assumption not(:R a :R) modus tolens [...] > > I don't see any circularity here. Where do you think that the circularity > > arises? > > Yes, assuming :R a :R you can derive per MP > :R a [ owl:complementOf :R ] > > but what you have assumed should become > a (finite) branch of the final proof tree. > > So let's now assume :R a [ owl:complementOf :R ] > and then per MP > :R a [ owl:complementOf :R ] > ?x a [ owl:complementOf ?x ] -> ?x a :R > |- > :R a :R > > but what we have assumed should become > a (finite) branch of the final proof tree > and all we have can be substituted, so > :R a :R > ?x a :R -> ?x a [ owl:complementOf ?x ] > |- > :R a [ owl:complementOf :R ] > ?x a [ owl:complementOf ?x ] -> ?x a :R > |- > :R a :R > > and that is circular. Well, it is possible to make assumptions, and as long as they are discharged appropriately, which is done above, they don't need justification. > I really wonder if you can write a final proof tree > with non-assumed leafs? Well, of course. I'll put together a fairly detailed derivation shortly. > -- > Jos peter

Received on Monday, 20 May 2002 13:35:20 UTC