Subject: Introducing the GraPE Graphical Proof Editor
Newsgroups: gmane.science.mathematics.frogs
Date: 2006-07-03 20:43:25 GMT (1 year, 44 weeks, 2 days, 19 hours and 8 minutes ago)
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.