The signature of a proof is a list of all the Predicates and Terms that appear inside the proof's outer layer (boxes inside a proof may have larger signatures then the proof as they may declare skolem terms). The signature of a proof controls what Predicates and Terms can be used inside it as for example in a proof which is given a^b and has a conclusion of a it makes no sense for the line a | d to appear as d is not in either the given lines or the conclusion.
There are two ways to set up a proof's signature in Pandora
- Simply adding the given and conclusion lines to a new proof will setup the signature of that proof to be all the Predicates, Functions, Constants and Variables used in these lines.
- Alternatively you can specify the Proof's signature before you add any lines to your proof using the Specify Signature menu item on the Apply menu. This opens a dialogue window that allows you to specify the signature you are going to use before adding any line to your proof. After you have specified a signature in this way any given lines you add and your conclusion line will then be checked against the signature and rejected if they contain Predicates or Terms that are not already in it.
See Using the Signature Window for more details.
To see the signature of the current proof click the Global Signature menu item in the view menu. Or if you want to see the signature of a particular box in your proof select a line in that box and click on Local Signature menu item in the view menu.
|