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

Date: Mon, 20 May 2002 10:51:54 -0400

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

Cc: www-webont-wg@w3.org

Message-Id: <20020520105154G.pfps@research.bell-labs.com>

Date: Mon, 20 May 2002 10:51:54 -0400

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

Cc: www-webont-wg@w3.org

Message-Id: <20020520105154G.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: Mon, 20 May 2002 16:24:02 +0200 [...] > > So what is the situation with respect to these formulae. Well, there > needs > > to be a development of the theory, but let's assume that this has been > > done. > > > > So let's take as given that > > > > 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 [ owl:complementOf :R ] > > follows. > > > > But our theory includes the implication > > ?x a ?y , ?x a [owl:complementOf :y] -> FALSE > > so using modus ponens again > > Ae/ FALSE > > > > Now the proof theory allows the deduction of the opposite of the > > assumption, so > > f/ not ( :R a :R ) > > > > follows. > > > > And so on. > > > > Nowhere is there any indication that anything not permitted has happened. > > > > So, what is the problem with the above derivation? It seems to be just as > > VALID or SOUND as any other derivation. > > Well, in a sense it seems like you are building > two mutual dependent proofs, actually more like > cyclic proof graphs if that term would exist??? > We are just trying to write a finite proof tree > for :R a :R (and we can't write down such a fpt) > > -- > Jos I don't see any circularity here. Where do you think that the circularity arises? peterReceived on Monday, 20 May 2002 10:52:06 UTC

*
This archive was generated by hypermail 2.4.0
: Friday, 17 January 2020 23:04:30 UTC
*