In the main Proof Designer window, you should see a button that says “Write a Proof”. (If you don't, read the instructions for setting up your computer to use Proof Designer.) To start writing a proof, click on the Write a Proof button. (The first time you click on this button, there will be a short delay while certain features of Java start up.)
A dialog box will open, asking you to enter the hypotheses and conclusion of the theorem you want to prove. To enter a hypothesis, type it into the space labeled “Enter hypotheses and conclusion here” and then click the Add Hypothesis button, and it will be added to the list of hypotheses. To enter the conclusion, type it in and click the Set Conclusion button. When typing the hypotheses and conclusion, use ordinary set-theoretic and logical notation. (For a more complete explanation of how to type statements into Proof Designer, click here.) If you change your mind about one of the hypotheses, you can click on it to select it and then click the Cut Hypothesis button to remove it from the list. If you change your mind about the conclusion, just type in a different conclusion and click the Set Conclusion button. The new conclusion will replace the old one. When you have entered the hypotheses and conclusion, click OK.
The dialog box will close, and a new window will open. The window will contain the statement of the theorem you are proving, and a place where the proof will go. As you give commands in Proof Designer, an outline of the proof will gradually take shape in this window. 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 “?” 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, select the first item, and then hold down the shift key on the keyboard and click on additional items to add them to the selection. 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.
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.
Applets are not allowed to print. However, you may be able to print your proof by using one of the Export HTML commands.
Here is a list of all the menu commands. Click on a command to get instructions on how to use the command.