From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Mon, 20 May 2002 07:59:11 -0400

To: jos.deroo.jd@belgium.agfa.com

Cc: www-webont-wg@w3.org

Message-Id: <20020520075911U.pfps@research.bell-labs.com>

Date: Mon, 20 May 2002 07:59:11 -0400

To: jos.deroo.jd@belgium.agfa.com

Cc: www-webont-wg@w3.org

Message-Id: <20020520075911U.pfps@research.bell-labs.com>

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. peterReceived on Monday, 20 May 2002 07:59:22 UTC

*
This archive was generated by hypermail 2.4.0
: Friday, 17 January 2020 23:04:30 UTC
*