Re: proof step for list built-in is goofy

Yup, looksas though the same param has been given twice in the proof.

On Oct 18, 2006, at 2:23, Dan Connolly wrote:

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