Re: ISSUE: DAML+OIL semantics is too weak

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?


peter

Received on Monday, 20 May 2002 10:52:06 UTC