- From: Dan Connolly <connolly@w3.org>
- Date: Thu, 07 Sep 2006 05:42:40 -0500
- To: public-cwm-talk@w3.org
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