Jape, sequents, and judgements

I mentioned to Pat Hayes that we're starting to get some traction on 
this semantic web proof checking stuff in the TAMI and PAW projects, and 
he said I should check out Jape <http://jape.org.uk>, a proof editor by 
Richard Bornat and company. It's open source, with a user interface in 
Java and the core engine in ocaml.

I downloaded it and fired it up on my OS X laptop, and it seemed to go 
OK, though I wasn't sure which end was up. I fumbled around the source 
and found natural_deduction_manual.pdf, which is is a tutorial at the 
"first click this, then choose this menu item" level; so I could follow 
along, but I didn't really understand what was going on well enough to 
be able to do a proof of my own.

I looked at the source of the conjecture/proof/rule files; they're sorta 
just text files, but they use some funky unicode characters. I haven't 
really found a description of the syntactic structures. It has a 
somewhat generic approach to syntax, a little like larch. Obviously, I'm 
interested in webizing <http://www.w3.org/DesignIssues/Webize> their 
syntax -- turning the identifiers into URIs, if not putting pointy 
brackets around it. I'd like to see how it maps to MatML or RuleML or 
the cwm proof ontology or PML.

Meanwhile, I did a little surfing around wikipedia** and learned that 
there's more to /natural deduction 
<http://en.wikipedia.org/wiki/Natural_deduction>/ and /sequent calculus 
<http://en.wikipedia.org/wiki/Sequent_calculus>/ than I had previously 
assumed.

They call it a proof calculator, as opposed a proof checker like Isabelle*

*where are my notes on Isabelle? in the swig/rdfig chump somewhere, I think.

** did I mention how much I love wikipedia's math and science articles? 
perhaps the subject of another item.

p.s. this is, in part, an experiment in using Mozilla Thunderbird as a 
blogging tool. See esw:ImmersiveHypertextEditing.