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

Now that we're starting to have more interoperability
around this http://www.w3.org/2000/10/swap/reason ontology,
I'm trying to understand it.

By the way... I wrote
  http://www.w3.org/2000/10/swap/test/reason/reason-report.n3
which renders proofs in a style that's close to what I
learned in school (http://www.utexas.edu/courses/phl313k/).
There's a step number (well, a label), then the formula
that's established by the step, then a justification,
which refers to earlier steps.

First you generate a proof in the normal way:

swap/test/reason$ python2.4 ../../cwm.py socrates.n3 --think
--filter=soc-goal.n3 --base=foo: --why >,soc-pf.n3

Then you run the report:

swap/test/reason$ python2.4 ../../cwm.py ,soc-pf.n3 reason-report.n3
--think --strings >,socrates-proof-report.n3

The results in full are attached. Much of it is straightforward;
here's an excerpt, lightly edited:

---8<---
0Show :socrates     a :Mortal  [Show]

1_g0 ['../../cwm.py', 'socrates.n3', '--think', '--base=foo:',
'--filter=soc-goal.n3', '--why'] [Invocation]

2_g1 {...} [1_g0, Parsing <socrates.n3>]

3_g_L36C30  :socrates     a :Man . [2_g1, CE]

3_g_L41C37  
   { ?who     a :Man } => { ?who     a :Mortal } . [2_g1, CE]
---8<---

So far, so good: we have { :socrates a :Man } by parsing socrates.n3
and conjunction exploitation, and likewise we
have { ?who     a :Man } => { ?who     a :Mortal }.

Note that the formula in step 2_g1 isn't given explicitly. I
suppose the proof checking algorithm is to fill it in from
the Web at check time, and the implicit policy is that any
sources given on the command line are trusted (though the
check.py code doesn't seem to check that.)

The interesting step in the proof, the rule application, surprised
me a bit:

---8<---
3_g_L41C37  
   { ?who     a :Man } => { ?who     a :Mortal } . [2_g1, CE]

7_g_L28C36 {...} [3_g_L41C37, (3_g_L36C30), GMP ?who := <...#socrates>]

---8<---

The {...} is something that reason-report.n3 conjures up because
the relevant step in ,soc-pf.n3 doesn't have a :gives. It's not
until the next step that you find out what it concluded:

---8<---
3_g_L36C30  :socrates     a :Man . [2_g1, CE]

3_g_L41C37  
   { ?who     a :Man } => { ?who     a :Mortal } . [2_g1, CE]

7_g_L28C36 {...} [3_g_L41C37, (3_g_L36C30), GMP ?who := <...#socrates>]

8_g_L26C18   :socrates     a :Mortal . [7_g_L28C36, CE]
---8<---



I got a brief explanation form TimBL in IRC (quoted
here without permission)...

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

I started looking at the check.py code.
 http://www.w3.org/2000/10/swap/check.py v1.35

I'm tempted to give it a scrub and add doctest style unit tests so
that I know exactly what it's up to.

Shouldn't the parsing steps go in the Truth/Policy/Worldview thing?
Hmm...

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