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

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