Pandora stands for "Proof Assistant for Natural Deduction using Organised Rectangular Areas". Pandora can be used to prove that a <goal> formula follows from the given formulae.
To start a new proof, select "New" from the File menu or alternatively press the "Start New Proof" button on the Welcome screen. The input screen has a section for the givens and goal. The given section allows multiple lines of input, whereas only a single line can be entered for the <goal> section. It is compulsory to have a <goal> for your proof.
When you have input any given(s) and <goal> you can check the validity of your input by pressing the "Check Proof" button. If it is valid, to proceed solving your proof, press the "Start Proof" button.
A Pandora proof contains a sequence of validly applied Natural Deduction rules. To easily distinguish parts of the proof, dashed boxes are used. Where the proof structure requires additional assumptions, solid boxes represent this.
Natural Deduction rules are applied to proof lines. A rule can only be applied forwards to an <empty> line or backwards to a <goal> line. To apply a rule, select a proof line and a Natural Deduction rule button in either order. For some Natural Deduction rules extra lines must be selected after this. This applies the selected rule to the first selected proof line if possible.
When there are no more <goal> lines in a proof box that box will turn green to show that it has been proved. When all of the proof boxes in a proof have been proved, the whole proof will turn green and the proof is completed.
Additional and plentiful help is provided within Pandora.