Below, we describe how to construct a proof that logical conjunction is commutative, as illustrated by the following animation. Apart from the first two steps, each step in the animation corresponds to one mouse click or one key press.

- Import the logic you want to use, in this case
`Examples/Satslogik`

for (constructive) propositional logic. Use the**Import...**command from the**File**menu, click on the**Library**button, then on the`Examples`

directory, then on`Satslogik`

. - Add a new definition (e.g., by using the command
**New Declaration**in the**Edit**menu). Here you give the new proof a name, and introduce the propositional variables that occur in the proposition.After pressing the OK button (or the `Return`key), we have the following skeleton definition: - Fill in the type of the propositional variables, which should be
Prop, by clicking on Prop in the menu window.
- Enter the propsition. You can build it in a top-down order by
clicking on the appropriate connectives and propositional
variables in the menu window.
- The last thing to do before we can start working on the proof,
to make the proof appear in natural deduction style,
you have to use the command
**ND Style Proof**from the menu.

To simplify things for students, teachears can prepare exercise files where these steps have already been performed.

In our example, the proposition to be proved is an implication, so a natural first step is an implication introduction, which we can click on in the menu to obtain the following:

When the proof is complete, you might want to save it by using the
command **Save** or **Save As...** in the
**File** menu.

- If you in the
**Options**menu select the alternative**Filter through type checker**, only applicable proof rules will be shown in the menu. - Elimination rules are always applicable, since the allow you to conclude anything. This doesn't meen that using them is always appropriate.
- After using an elimination rule, the new subgoals usually contains some metavariables (?). Most of the time, there is no need to fill in these manually, just go ahead and fill in the next proof rule to use intead.
- Assumptions are referred to by names that are shown with a lambda to the left of the rule where the assumption is discharged. To find out what is assumed click on the name of the assumption next to the lambda.
- You can use
**Undo**to go back one or more steps if you used the wrong proof rules. - You can mark and delete arbitrary parts of your proof, but, you
may then need to use the menu
command
**ND Style Proof**again, to make the new proof appear in natural deduction style. - Proofs presented in Natural Deduction style easily become rather wide.
Top-Down Proof Tree is an alternative proof presentation style that
can be selected in the
**View**menu. See below.

Thomas Hallgren