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

#Processed by Id: cwm.py,v 1.180 2005/11/02 00:06:26 timbl Exp 
        #    using base foo:
        
#  Notation3 generation by
#       notation3.py,v 1.185 2005/11/02 00:06:26 timbl Exp

#   Base was: foo:
     @prefix : <http://www.w3.org/2000/10/swap/reason#> .
    @prefix gmp: <file:/tmp/gmp.n3#> .
    @prefix log: <http://www.w3.org/2000/10/swap/log#> .
    @prefix n3: <http://www.w3.org/2004/06/rei#> .
    
     @forSome <#_g0> .
      [      a :Conjunction,
                    :Proof;
             :component  [
                 a :Inference;
                 :binding  [
                     :boundTo  [
                         n3:uri "file:/tmp/gmp.n3#socrates" ];
                     :variable  [
                         n3:uri "file:/tmp/gmp.n3#who" ] ];
                 :evidence  (
                 [
                         a :Extraction;
                         :because <#_g0>;
                         :gives {gmp:socrates     a gmp:Man .
                        } ] );
                 :rule  [
                     a :Extraction;
                     :because <#_g0>;
                     :gives { @forAll gmp:who .
                    {
                        gmp:who     a gmp:Man .
                        
                        }     log:implies {gmp:who     a gmp:Mortal .
                        } .
                    } ] ],
                    <#_g0>;
             :gives { @forAll gmp:who .
            gmp:socrates     a gmp:Man,
                        gmp:Mortal .
            {
                gmp:who     a gmp:Man .
                
                }     log:implies {gmp:who     a gmp:Mortal .
                } .
            } ].
    
    <#_g0>     a :Parsing;
         :because  [
             a :CommandLine;
             :args "['/home/connolly/w3ccvs/WWW/2000/10/swap/cwm.py', '/tmp/gmp.n3', '--think', '--base=foo:', '--why']" ];
         :source <file:/tmp/gmp.n3> .
    
#ENDS