proof step for list built-in is goofy

cwm does something goofy with list:in when it produces
a proof. check.py catches it a la...

   Proof invalid: Built-in fact does not give correct results:
predicate: li1 subject: list:in object: li1 result: None

Using the --report option on check.py that I just merged
into the HEAD, the step looks like:

11: ( "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" ) :in
( "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" ) .
 [by built-in Axiom list:in]

In n3, it looks like:
                                     [
                                             a :Fact;
                                             :gives {

( "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" )
                                                 list:in  (

"http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" ) .
                                            } ]


I think it should be:

11: "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" :in
( "http://www.w3.org/2003/12/rdf-in-xhtml-xslts/grokCC.xsl" ) .
 [by built-in Axiom list:in]


Here's what I was doing when I discovered the bug.
By the way, this exercise is also suffering from
the "something fishy with bnodes in proofs"
problem that I reported to cwm-talk 7 Sep.
http://lists.w3.org/Archives/Public/public-cwm-talk/2006JulSep/0009.html


connolly@dirk:~/w3ccvs/WWW/2004/01/rdxh$ make grddl-rule-test-pf.txt
python ../../../2000/10/swap/cwm.py grddl-rule-tests.n3 grddl-rules.n3
\
                --think  --filter=grddl-rule-goal.n3 --why
>grddl-rule-test-pf.n3
PYTHONPATH=../../../2000/10/swap/..
python ../../../2000/10/swap/check.py --report grddl-rule-test-pf.n3
>grddl-rule-test-pf.txt
                                         Proof failed:  Built-in fact
does not give correct results: predicate: li1 subject: list:in object:
li1 result: None
   Proof invalid: Built-in fact does not give correct results:
predicate: li1 subject: list:in object: li1 result: None


For more context, see...

spec#issue-output-formats formal specification in terms of graphs
Dan Connolly (Wednesday, 18 October)
http://lists.w3.org/Archives/Public/public-grddl-wg/2006Oct/0044.html

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E

Received on Wednesday, 18 October 2006 06:24:07 UTC