MadMode

The proof generation feature of cwm has been in development for a long time. The idea goes back at least as far as the section on proofs and validation in the original 1998 Semantic Web Roadmap, where we find sees of the proof-based access control idea that is now funded under the policy aware web project:

The HTTP "GET" will contain a proof that the client has a right to the response.

And in the TAMI project, we're looking at proofs as part of an audit mechanism for accountable datamining.

The cwm development process incorprates aspects of extrememe programming: test-driven development and a variation on pair programming; when somebody has a new feature working, somebody else in the group tries to (a) reproduce the test results and (b) review the tests, if not the code. When the pair agree that the tests are OK, we claim victory in a small group setting, and if that goes well, we make a release or at least send mail about the new feature. This typically takes a week or two or three.

In the case of cwm --why, I have been evaluating the tests since at least as far back as this December 2002 check-in comment on swap/test/reason/Makefile, and I still haven't made up my mind:

date: 2002/12/30 15:00:35; author: timbl; state: Exp; lines: +9 -6
--why works up to reason/t5. GK and SBP's list bugs fixed.

I have tried and failed to understand many times when Tim explained the simplicity of the reason proof ontology. I think I'm finally starting to get it. I'm nowhere near being certain it's free of use/mention problems, but I'm starting to see how it works.

The InferenceWeb folks have all sorts of nifty proof browsing stuff, and they're working with us in the TAMI project. In our meeting last August, they explained PML well enough that TimBL started on to-pml.n3, some rules to convert cwm's proof structures to PML. The rest of the integration task has been starved by work on SPARQL and Paulo moving to UTEP and all sorts of other stuff, but we seem to be moving again.

I tried running one of my versioning proofs through to-pml.n3 and then looking at it with the InferenceWeb proof browser, but I haven't got the PML structure right and it doesn't give very detailed diagnostics.

I made some progress by loading one of the PML examples into tabulator (alpha) and loading my swap/reason style proof in there and using the outline view to browse the structure. (It turns out that TimBL started coding the tabulator one day when he was having trouble reading a proof. GMTA ;)I discovered that PML is striped:

• NodeSet
  • isConsequentOf
    • InferenceStep
      • hasAntecedent
        • NodeSet
          • ...

... where the swap/reason ontology just has Step objects and hangs the conclusions off them.

That was the key to some big changes to to-pml.n3. I don't have the output working in the PML browser yet, but Paolo sent me a pointer to a PML primer, which seems to have the remaining clues that I need.

See also: help checking/reading some proof related to versioning? to cwm-talk.