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: Dan Connolly <connolly@w3.org>
Date: Mon, 21 Dec 2009 13:35:39 -0600
To: jos.deroo@agfa.com
Cc: public-cwm-talk <public-cwm-talk@w3.org>
Message-ID: <1261424139.5304.9678.camel@pav.lan>
On Mon, 2009-12-21 at 20:07 +0100, jos.deroo@agfa.com wrote:
> Dan Connolly wrote: 
[...]
> Your remark triggered my thinking and I started hacking 
> the proof generation in eye... Thanks for that trigger! 
> 
> The new run of 
[...]
>
> and guess what check --report produces from those... all systems go! 
> 
> check --report pf1.n3 > pf1.report 

This looks like progress, but I don't think we should claim
victory just yet; this proof doesn't actually seems sound, to me.
It's not sound to go from
  Exists x. P(x) -> Q(x)
  P(a)
to
  Q(a)


I think check.py should have disallowed steps such as 31:

   * - 26
     - :Citi_Wide_brochure c:speaks_for :City_Wide .
     - erasure from step 25
     - 
   * - 28
     - :Citi_Wide_brochure c:says
{:City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost
3700; :rate_offset 0.25 . } .
     - erasure from step 27
     - 
   * - 30
     - @forAll :x1, :x2. @forSome :x0 . { :x0 c:says :x2;
c:speaks_for :x1 . } log:implies {:x1 c:says :x2 . } .
     - erasure from step 29
     - 
   * - 31
     - :City_Wide c:says
{:City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost
3700; :rate_offset 0.25 . } .
     - rule from step 30 applied to steps (26, 28)
     - {'x2': '{3}', 'x0':
u'<http://www.w3.org/2001/tag/dj9/refi_ex#Citi_Wide_brochure>', 'x1':
u'<http://www.w3.org/2001/tag/dj9/refi_ex#City_Wide>'}


-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
gpg D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E
Received on Monday, 21 December 2009 19:35:42 UTC

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