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