Proof Designer has five menus, File, Edit, Strategy, Infer, and Goal, located at the top of the window. Click on the title of a menu to show the menu, and then click on a command in the menu to give the command. You can use the + and − buttons to the right of the menus to adjust the font size. To start writing a proof, select “New Theorem...” from the File menu. For instructions on using the New Theorem command, click here.
As you give commands in Proof Designer, an outline of the proof you are writing will gradually take shape. While you are working on the proof, there will usually be one or more gaps in the proof where additional steps need to be filled in. Each gap will be indented and enclosed in a box, and it will have a pink background and a “?” button in the upper left corner. The gap will say what needs to be filled in at that point in the proof, and then it will give a list of givens—statements that are known to be true at that point in the proof—and the goal of the gap. Usually the goal is a statement that needs to be proven, but occasionally the goal indicates that you need to assign a value to a variable, and you can also have gaps that have no goal at all. Initially, the entire proof consists of a gap whose givens are the hypotheses of the theorem, and whose goal is the conclusion of the theorem.
To add a step to the proof, you click on a given or goal to select it and then give a command from one of the menus at the top of the window. Sometimes you will need to select several items. To do this, simply click on them one after another. You can also select an entire gap by clicking either on the sentence that introduces the gap or in the margin to the left of the gap. If you accidentally select something you didn't want to select, just click on it again to deselect it.
As you give commands, steps will be added to the proof, and the givens and goal lists will be updated. Sometimes a step will be justified by a subproof—a sequence of steps that, together, justify an assertion. Each subproof is indented and enclosed in a box, and has a “∴” button in the upper left corner. Subproofs can be nested inside each other, and a subproof may also contain a gap. You can select a step in the proof by clicking on it. If the step is justified by one or more subproofs, the subproofs get selected as well.
Some commands will add variant forms to givens or goals. A variant of a statement is another statement that is equivalent to the original statement. A variant of a given or goal is listed below the original and indented, and it has an open circle in front of it rather than a bullet. You use a variant just like the original given or goal. In particular, you can select a variant by clicking on it.
You can change the order of the givens in a givens list by pointing to a given, pressing and holding down the mouse button to “grab” it, and then dragging it to a new location in the list. Any variants of the given get moved with it.
If the structure of the proof you are creating gets complicated, you can hide some of the details by clicking on a button in the upper left corner of a subproof or gap. When you click on the button, the details of the subproof or gap are hidden. Click again to show the details again.
You can print your proof by using the Print command in your browser.
Here is a list of all the menu commands. Click on a command to get instructions on how to use the command.