walking thru a proof with cwm --why

I'm getting up to speed on the cwm/n3 proof representation.

I started with this in /tmp/gmp.n3:

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

socrates a Man.
{ ?who a Man } => { ?who a Mortal }.
---8<---

and asked cwm:

cwm.py /tmp/gmp.n3 --think --base=foo: --why >,gmp-pf.n3

results are attached.

Then I can run check thusly:

$ python check.py -v10 ,gmp-pf.n3
     Length of proof formula: 24
     Proof looks OK.   5 Steps
     @prefix : <file:/tmp/gmp.n3#> .
    @prefix log: <http://www.w3.org/2000/10/swap/log#> .

     @forAll :who .

    :socrates     a :Man,
                :Mortal .
    {
        :who     a :Man .

        }     log:implies {:who     a :Mortal .
        } .

Tim sketched some rules to convert cwm's proof format to pml...

http://www.w3.org/2000/10/swap/test/reason/to-pml.n3
 <- http://www.policyawareweb.org/2005/ftf2/paw-mtg

I hope to look into that more presently.

I saw some interest from Jos about proof formats... Oh for more
time... gotta run...

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