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.

- File Menu
- Help: Choosing this command displays the main help file.
- New Theorem…
- Revise Theorem…
- Save
- Open…

- Edit Menu
- Strategy Menu
- Infer Menu
- Modus Ponens
- Modus Tollens
- Conjoin
- Split Up
- Addition…
- Disjunctive Syllogism
- Universal Instantiation…
- Existential Instantiation…
- Reflexive Law…
- Goal Menu