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

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

From: <jos.deroo@agfa.com>
Date: Wed, 7 Jun 2006 21:29:46 +0200
To: connolly@w3.org
Cc: public-cwm-talk@w3.org, public-cwm-talk-request@w3.org
Message-ID: <OF3B09A55D.8AB147BE-ONC1257186.00696414-C1257186.006B1107@agfa.com>

Dan Connolly wrote:
[...]
> I got a brief explanation form TimBL in IRC (quoted
> here without permission)...

without?? :-)

> <DanC> by the way, yosi, do you know why cwm doesn't spit out :gives
> on :Inference?
> <DanC> and why does check.py think that's OK?
> * DanC still doesn't understand the proof checking algorithm
> <yosi_s> I'm not swapped in on cwm's proof checking right now
> <yosi_s> I've stepped back to try to figure out what it should be doing
> <timbl> It doesn't spit out gives on an inference as it  it is obvious
> from the stuff it does spit out, and it takes a lot of space.  I woul
> drecommend a --why=f   option for a fastidious proof
>
> Hmm... I suppose if the {...} is OK on a Parsing line, it
> should be OK on a GMP/Inference line too.

Is it then a bit like in
http://eulersharp.cvs.sourceforge.net/eulersharp/2006/02swap/etc5.ref?revision=1.68
Also in there instead of r:rule [...]; r:binding [...]
we just have the substituted r:rule [...]
(I lost on the separate bindings in cases where
there are variable predicates as the underlying
prolog renamed some variables)
Am also still correcting the log:notIncludes of a
log:conclusion case and experimenting with e:findall
(like the prolog one but here in an explicit scope) 


-- 
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Wednesday, 7 June 2006 19:30:01 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 8 January 2008 14:11:02 GMT