W3C home > Mailing lists > Public > public-cwm-talk@w3.org > October to December 2009

Re: working on "A Model of Authority in the Web"

From: <jos.deroo@agfa.com>
Date: Mon, 21 Dec 2009 21:43:20 +0100
To: connolly@w3.org
Cc: public-cwm-talk <public-cwm-talk@w3.org>
Message-ID: <OF119325C6.59110CD8-ONC1257693.006EC10F-C1257693.0071D9E2@agfa.com>
Dan Connolly wrote: 
[...]
> It's not sound to go from
>   Exists x. P(x) -> Q(x)
>   P(a)
> to
>   Q(a)

That is indeed unsound but there is no such rule
with an Exists x where x occurs in the conclusion.

[...]

>    * - 30
>      - @forAll :x1, :x2. @forSome :x0 . { :x0 c:says :x2;
> c:speaks_for :x1 . } log:implies {:x1 c:says :x2 . } .
>      - erasure from step 29
>      - 

in this rule :x0 does not occur in the conclusion

We actually make sure that we have "no such rule
with an Exists x where x occurs in the conclusion"
in the latest eye code:
[[
        findall(V,(member(V,PVars), \+member(V,CVars)),PEVars)
]] -- 
http://eulersharp.svn.sourceforge.net/viewvc/eulersharp/trunk/2006/02swap/euler.yap?r1=3226&r2=3225&pathrev=3226


Kind regards,

Jos De Roo | Agfa HealthCare
Senior Researcher | HE/Advanced Clinical Applications Research
T  +32 3444 7618
 http://www.agfa.com/w3c/jdroo/

Quadrat NV, Kortrijksesteenweg 157, 9830 Sint-Martens-Latem, Belgium
http://www.agfa.com/healthcare
Received on Monday, 21 December 2009 20:43:55 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:01:06 UTC