Home

Proof Assistant Wiki

This wiki contains information on the use of the Proof Assistant. It assumes you have the latest version.

Installing

You need to have Java installed to run the Proof Assistant. You can check that here. The Proof Assistant app is run from a JAR file. As such, no installation is required.

• Download the file ProofAssistant x.y.z.jar (where x,y,z are numbers).
• Run the file by double clicking on it.

The Proof Assistant will create a file called .config to allow for persistent settings. This will be placed in the same folder as ProofAssistant.jar. If you move ProofAssistant.jar, you may wish to move the .config file as well. ProofAssistant.jar can be run from the command line with no arguments, one argument (a .ndp file to be opened) or more than one argument (advanced: a sequent in TeX macro format).

Note: Some versions of OSX use Gatekeeper, which may prevent the JAR file running. If this is the case, Ctrl+Click on the JAR from Finder, and select "Open". See here for more information.

Support

For help using the Proof Assistant, see [Basic Usage], [Advanced Usage] and [Settings].

What should I report?

Create a ticket for absolutely anything. If you think you've found a bug, if you've spotted a spelling mistake, if a rule is missing, create a Ticket. You can check to see if anyone else has the same problem on the Tickets page.

Quick Start Guide

• Download the latest version (you're looking for a JAR file).
• Run the JAR file.
• Create a new proof from the File menu.
• Select an unjustified line as your current goal.
• Optionally select an appropriate justified line as your current resource.
• Use the rule buttons to complete the proof.
• Change proof system (in options) to access more rules.