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

On Wed, 2006-06-07 at 10:34 -0500, Dan Connolly wrote:
> 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.

The .n3 version of this report was a nice prototype,
but I need something more robust, so I coded it up in python
inside check.py . It interferes with the normal way that
check.py works, so I checked it in a branch, for now.
 check.py,v 1.55.2.1 2006/09/07 06:54:54
The report needs to be made optional, invoked by a
command-line arg.


> 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

That much is the same, but now you run the report a la:

~/w3ccvs/WWW/2000/10/swap/test/reason$ PYTHONPATH=$swap/.. python
$swap/check.py ,soc-pf.n3

And out comes the normal check.py output, followed by the report:

     @prefix :
<file:/home/connolly/w3ccvs/WWW/2000/10/swap/test/reason/socrates.n3#> .

    :socrates     a :Mortal .


1: ...
 [by parsing <socrates.n3>]

2: :socrates a :Man .
 [by CE on 1 (@@_g_L36C30)]

3: @forAll :who . { :who a :Man . } log:implies {:who a :Mortal . } .
 [by CE on 1 (@@_g_L41C37)]

4: ...
 [by GMP on 3, [2]]

5: :socrates a :Mortal .
 [by CE on 4 (@@_g_L26C18)]

6: ...
 [by parsing <soc-goal.n3>]

7: @forAll so:p . { :socrates so:p :Mortal . } log:implies {:socrates
so:p :Mortal . } .
 [by CE on 6 (@@_g_L53C25)]

8: ...
 [by GMP on 7, [5]]

9: :socrates a :Mortal .
 [by CI on [8]]


The last few steps are a little funny-looking; they're
a bi-product of using --filter to reduce the conclusion
to a goal. Step 5 is the main conclusion.

The @@_g_L36C30 is a diagnostic to help me figure out
why it's not suppressing dups.


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

Received on Thursday, 7 September 2006 07:07:17 UTC