Re: ISSUE: DAML+OIL semantics is too weak

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

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

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

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.

I really wonder if you can write a final proof tree
with non-assumed leafs?

--
Jos

Received on Monday, 20 May 2002 13:18:22 UTC