Introducing the GraPE Graphical Proof Editor

Hi,

I would like to announce the availability of a new
release (version 0.9.2) of GraPE, a versatile
GUI-based proof editor with strong support for the
calculus of structures. You can download it from
http://grape.sf.net

Notable features of GraPE include:

  - It is flexible enough to support many different
inference systems; the standard distribution contains
implementations of system BV and a variant of system
SKSg as well as the one-sided Gentzen-Schuette sequent
calculus.

  - It can interface to a Maude interpreter, so you
can use the Maude language to implement new inference
systems or use one of the systems implemented by Ozan
Kahramanogullari
(http://www.computational-logic.org/~ozan/maude_cos.html).

  - It supports not only inference rules to build a
derivation step by step, but also transformation rules
that affect the derivation as a whole, such as proof
search or the elimination of admissible rules (simple
examples are included in the distribution).

Please note that GraPE is still in an early stage of
development; documentation is scant (though improving)
and there surely are many bugs to be squashed.

Development, however, is ongoing, with a 1.0 release
slated for the not too far future. The best way you
can help GraPE is by trying it out and submitting a
bug report when it crashes.

Enjoy!

-- Max

PS: GraPE will be presented at the proof theory
meeting in Bath this week.