W3C home > Mailing lists > Public > www-webont-wg@w3.org > May 2002

Re: ISSUE: DAML+OIL semantics is too weak

From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
Date: Mon, 20 May 2002 16:24:02 +0200
To: pfps@research.bell-labs.com
Cc: "www-webont-wg" <www-webont-wg@w3.org>
Message-ID: <OF158DF6C3.507F1A4B-ONC1256BBF.004D7BAE@agfa.be>

> I'm still trying to understand this table.  I'll add in some extra
> information to see if I can clarify it.
>
>      Premise     ->     Conc.
> *     a       a->b     b       Deducing b from a and a->b
> *                    using modus ponens
>  ----------------------------------------------------
>  (1) False     True     False       VALID     UNSOUND
>  (2) False     True     True        VALID     UNSOUND
>  (3) True      False    False       INVALID   UNSOUND
>  (4) True      True     True        VALID     SOUND

Right


> > and having that
> >   :R a [ owl:complementOf :R ]
> > is the same proposition as
> >   not(:R a :R)
> > we have the case
> >   not(p) -> p
> > so only (2) or (3) are to be considered
> > but both are UNSOUND
>
> 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
Received on Monday, 20 May 2002 10:25:10 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:50 GMT