If you are using pandora for a complex proof that involves the use of a lot of symbol names (e.g. predicate, functon names) then you can use Pandora's Signature Editor Window to enter the signature of your proof before you enter any given or conclusion lines. When a signature is specified this way all the given and conclusion lines you enter will then be checked against the signature you entered and rejected if they include any symbol names that have not already been specified.

To specify a signature in this manner you first need to start a new proof and before you enter any given lines select Specify Signature from the Edit Menu.
This will display the Signature Editor Window, which if you have started a new proof should show no items in any of the four list boxes headed Constants, Variables, Predicates and Functions.

The window contains four list boxes which list all the items currently in the signature by their type (e.g. constants or variables).
Below these list boxes are four edit boxes in which you can enter the name of a symbol you wish to add to the signature. Each box is for adding a different type of signature Item, with the function and predicate boxes also having a separate arity box in which you can specify the symbol's arity. After you have entered the name and arity (if required) of a symbol click on the Add button next to the box to add the item to the signature. It will then appear in the apropriate list box in the top half of the window.

You can undo adding an item to the signature by clicking on the Undo button in the bottom of the window, or you can revert the signature back to the state it was in when you first opened the editor window by clicking on the Reset Signature button.

After you have entered you signatureyou can go back to the main pandora window and carry on with you proof using it by clicking on Accept Signature or cancel you changes by clicking on cancel

Also see

Signatures