W3C home > Mailing lists > Public > public-cwm-talk@w3.org > July to September 2006

Re: struggling to understand the cwm/N3/reasons proof checking algorithm

From: Dan Connolly <connolly@w3.org>
Date: Thu, 07 Sep 2006 05:42:40 -0500
To: public-cwm-talk@w3.org
Message-Id: <1157625760.9288.1376.camel@dirk>

On Thu, 2006-09-07 at 02:07 -0500, Dan Connolly wrote:
> [...] I coded it up in python
> inside check.py . It interferes with the normal way that
> check.py works, so I checked it in a branch, for now.
>  check.py,v 1.55.2.1 2006/09/07 06:54:54

I think cwm is doing something fishy with bnodes and proofs.
Consider:

---8<---
@prefix : <gmpbnode#>.
@keywords is, of, a.

dan home [ in Texas ].

{ ?WHO home ?WHERE.
  ?WHERE in ?REGION } => { ?WHO homeRegion ?REGION }.

---8<---

and run cwm --think on it, and then run this version
of check.py on it. The proof report is:

---8<---
1: ...
 [by parsing <gmpbnode.n3>]

2: @forSome :_g1 . :_g1 gmp:in gmp:Texas .
 [by CE on 1]

3: @forSome :_g1 . gmp:dan gmp:home :_g1 .
 [by CE on 1]

4: @forAll :REGION, :WHERE, :WHO . { :WHERE gmp:in :REGION . :WHO
gmp:home :WHERE . } log:implies {:WHO gmp:homeRegion :REGION . } .
 [by CE on 1]

5: ...
 [by GMP on 4, [2, 3]]

6: @forAll gm:REGION, gm:WHERE, gm:WHO. @forSome run:_g1 .
run:_g1 :in :Texas . :dan :home run:_g1; :homeRegion :Texas .
{ gm:WHERE :in gm:REGION . gm:WHO :home gm:WHERE . } log:implies
{gm:WHO :homeRegion gm:REGION . } .
 [by CI on [5, 1]]

---8<---

Step 5 is wrong/unsound. When you conjoin steps 2 and 3, you
have to rename one of the :_g1's.


-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E
Received on Thursday, 7 September 2006 10:42:52 UTC

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