Re-engineering of PANDORA

Proposed by Krysia Broda and Gabrielle Sinnadurai

Brief Description

PANDORA is currently implemented in JAVA 1.1.2. Although it has proved to be very robust, it needs updating to use current JAVA technology, such as SWING. The project is therefore to make this up-dating, and to use the opportunity to improve one or two features. The original code and report is available for your use and re-use.

Main Desired Improvements in order of priority

  1. Update to SWING.
  2. Allow proofs to be exported in a text format (one suitable format already exists). This would allow the possibility (beyond the scope of this group project) of introducing auto-testing at a later stage, as well as import of text proofs into PANDORA for graphical display.
  3. Correct one or two minor problems with the use of the rules for existential introduction and equality substitution in backwards mode.
  4. Allow the user to specify names of predicates, constants, etc in advance of their use, to help protect against typos.
  5. Allow instantiation of more than one outermost universal quantifier.

[:-)] We think all of you might enjoy this project [;-)]

Up Home