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 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