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: Sat, 18 May 2002 14:43:33 +0200

[...]

> From the table
> 
>     Premise     ->     Conclusion
> ----------------------------------------------------
> (1) False     True     False       VALID     UNSOUND
> (2) False     True     True        VALID     UNSOUND
> (3) True      False    False       INVALID   UNSOUND
> (4) True      True     True        VALID     SOUND


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

Well modus ponens is (roughly) an inference rule something like the
following:

a, a->b |- b

This inference rule can only be used if both a and a->b are present in the
premises, so it can only be used in case (4) above.  In cases (1) and (2)
all you have in the premise set if a->b so modus ponens is not applicable,
and any use of it is not permitted.  In case (3) a->b is not in the premise
set, so, again, modus ponens is not permitted.  As far as deriving b from a
and a->b the only permissable situation is (4).

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

peter

Received on Monday, 20 May 2002 07:59:22 UTC