Basic Usage

Basic Usage

We will demonstrate basic usage by going through a basic deduction. For more advanced usage, first ensure you have read this page, then see [Advanced Usage] and [Settings].

When you first start the Proof Assistant, you will see the main window:

Starting a new Proof

To start a new proof, click File -> New. This will bring up the New Proof dialog:

• Use the top textbox to input any premises, separated by commas.
• Use the second textbox to input exactly one conclusion. You will not be able to create a proof without a conclusion.
• Clicking on a symbol in the symbol panel will insert it into the currently focussed textbox. You can also use = and + in relevant sequents.
• "Quick change arities" allows you to change the arities for any functions or terms. See [Settings] for more information.

Note: Ensure your formulas match the syntax indicated by the [Style Guide], and that your brackets match.

Let's prove that (p&q), r --> (q&r):

To start the proof, press the OK button.

Completing Proofs

Upon starting a proof, the premises and conclusion will be displayed in the main screen, known as the "Proof Panel". This is where work on the proof is done. If a proof gets too large for the Proof Panel, scrollbars will appear. You may also resize the window to fit the proof.

In completing the proof, we will keep track of two lines:

• The current goal, which can be any unjustified line. This is a line we are working towards.
• The current resource, which can be any justified line in scope of the current goal. This is the line we are working from.

To begin, click on a line to select as the current goal. The line will change to green, indicating it is the current goal. Any rules relevant to this goal (generally introduction rules) will appear as buttons to the right of the goal. Clicking one of these buttons will apply the associated rule to the proof.

If you wish to, you can select a current resource by clicking on a relevant line. The line will change to red. Any justified line above the current goal can be selected as a current resource, however relevant rules will be deactivated if the current resource is out of scope. All relevant rules will appear as buttons to the right of the current goal.

You cannot select a current resource without first selecting a current goal.

Let's select a resource in our example:

Some rules will complete automatically while others will require further input. If we select &E, we will have to choose which conjunct(s) we want:

We don't need p, so let's select q. The rule is applied and we see the result:

Now let's apply &I. Since both q and r are available resources, choosing &I finishes the proof:

Don't worry if you make a mistake - undo and redo are implemented, and available under the Edit menu.

Saving and Opening Proofs

• To save a proof, click File -> Save. Proofs are stored as plain text .ndp files.
• To open a proof, click File -> Open. Locate the relevant .ndp file to open it.

Exporting Proofs

There are a number of options for exporting proofs. They can be found under File -> Export.

• To TeX code exports the proof in a format useable in LaTeX documents.
• To plain text presents the proof rendered into plain text
• To .png will save the proof as a PNG image, with a transparent background.
• Copy proof to clipboard will copy an image of the proof to the system clipboard.