The GraPE Graphical Proof Editor -- Homepage

Overview

GraPE is a tool for structural proof theorists to study deduction systems and to develop proof search strategies for them. GraPE should eventually support step-by-step proof construction, automatic proof search with various strategies, proof transformations and analysis. It is still in an early stage of development. For more information, see Max Schäfer's project report The Design and Implementation of the GraPE Graphical Proof Editor. See also the links in the Background Section.

News

12/17/06

No new release this time. Just wanted to let you know that GraPE is still alive and kicking. If you're interested, check out the newest SVN revision. Be warned, however, that we're in the middle of some major rewrites, and hence some features are currently broken. Thanks for your patience!

07/19/06

Version 0.9.4 released; again, this is only a minor update. Inference rules can now have names containing arbitrary Unicode characters, inference and transformation rules are separated in the rule chooser. Following a suggestion by Robert Rothenberg, system description files are now named according to the schema system-name-backend-name.xml, as in ksg-maude.xml, for example.

07/09/06

Version 0.9.3 released; this is a minor update that fixes some bugs which surfaced during the presentation in Bath. It includes an implementation of Lukasiewicz logic (gl.xml and gl.maude).

System Requirements

To run GraPE you will need to have the following software installed on your system:

• Java 1.5 runtime environment. You can obtain it from java.sun.com.
• Maude 2.2, which you can obtain from the Maude homepage.

Note that GraPE will not work with older versions of Java or Maude, since they miss some features the program depends on.

Download

The latest release of GraPE (currently version 0.9.4) can be downloaded here. Alternatively, you can go to our SourceForge.net project page and click on the large green download button. Then choose the latest release of GraPE.

Installation

1. Download the latest realease of GraPE, a file named grape-<version>.tar.gz, into your installation directory, for instance into /usr/local/lib/ or ~/lib/.
2. Untar the release file; depending on your system, this might more or less look like this:
   hostname:~/lib> tar xfvz grape-<version>.tar.gz
   This will create the directory ~/lib/GraPE-<version>/

Usage

Change to the directory that was created during installation and you will find the file grape.jar which can be run by java. GraPE needs to find some other files in this directory, so it's best to start GraPE from within this directory.

hostname:~/lib> cd GraPE-0.9.4
hostname:~/lib/GraPE-0.9.4> java -jar grape.jar

Help and Reporting Bugs

For some documentation see the README file, provided after installation, and the internal help of the GraPE application.

Please use the facilities at our SourceForge.net project page. Make use of the Help Forum or write an email to one of the developers.

Background -- Proof Editing And Proof Search in Deep Inference

1. Ozan Kahramanoğulları's page about deep inference implementation with Maude.
2. Alessio Guglielmi's page about deep inference and the calculus of structures.

Last change: Dec 17, 2006.