Version 1.3.3

Proof Assistant 1.3.3 is now available for download! Again, this is in JAR format. After I write this post, I'll update the wiki with release-specific instructions.

This release brings a number of exciting new features. You may have noticed that version 1.3.2 has been skipped. 1.3.2 was in fact a release that I didn't upload - 1.3.3 contains bugfixes for 1.3.2 among other things, so you're spared the worst problems. Because of this, I'll list the features new in both releases.

Note: Proofs saved to .ndp from versions earlier than 1.3.2 are not compatible with versions 1.3.2 and greater. Similarly, proofs saved to .ndp from versions 1.3.2 and greater are not compatible with versions prior to 1.3.2.

You may have noticed that 1.3.1 was around 300KB in size, whereas 1.3.3 is nearly 2MB. This is due to the necessary inclusion of a library for the first new feature:

Proof Systems "Revamp"

One of the largest changes has been to the way available rules are governed. In previous versions, the user would select to use NJ, NK, Q or PA. They could then subsequently select to turn identity boxes, quantifier shortcuts and automatic parameters (among other things) on or off. Thus set up, they could move through the proof using the rules available. This method was limiting, in that users could not define new proof systems, and that undo/redo would not affect the selection of proof system.

In 1.3.3, we have implemented rulesets. The ruleset of a proof is the combination of rules available. You can change your ruleset at any time from the rule palette (accessed under options, or by clicking the current ruleset in the new status bar). The rule palette shows all rules that could apply to the current proof as checkboxes, organised into categories. Simply select or deselect a checkbox to active or deactivate the corresponding rule. You can save rulesets as "presets". The app comes with 5 default presets - NJ, NK, NK+, Q and PA.

NK+ is identical to NK, but with identity boxes and quantifier shortcuts enabled.

In the main proof window, you'll find the new status bar. This tells you what your current rule preset is (or Custom if it's not a preset) and also the current proof system. The current proof system is determined by looking at the rules the proof has used and finding the weakest preset that will support all of those rules. For example, if your current ruleset is Q, but the only rule you have used is conjunction introduction, the current proof system will be NJ (assuming you haven't saved a weaker preset than NJ containing &I).

Arities "Rehash"

The handling of arities has also been redone in 1.3.3. You are now able to change arities during a proof, provided the arities you wish to change are not in lines that have been used. If they are, you must undo until those lines have not been used.

The Arities button in the status bar opens the settings dialogue. The tooltip for this button shows you which arities are used, which are unused and the arity of each. Using incorrect arities can result in badly formed lines. If the lines do not look fine, you may need to restart the proof with the correct arities.

Uneditable Proofs

A new file format, .ndu, has been introduced with 1.3.3. This format is used for an uneditable proof. Any .ndp can be renamed to a .ndu, and any proof can be saved as either. Opening a .ndu file will load the proof and return it to the beginning. Two buttons will appear that will allow you to step through the proof. You will not, however, be able to make any changes to the proof.

Note again that .ndp files saved from versions <1.3.1 and versions >1.3.2 are not compatible.

Minor Features

• You can now undo to before the initial current goal was selected
• Line thicknesses now change with zoom
• The sequent arrow is nicer

Bugfixes

There have been many bugfixes in this release including

• Bad identity box line behaviour with zoom
• Export to TeX and export to text giving negative line numbers for identity box lines and Q axioms
• The term selector panel showing numbers rather than terms