8.4.EM. Exercise machine

• Click on the Any arg button to produce a random exercise.
• Click on the Valid arg button to produce an entailment that holds.
• Click on the Develop button to produce the next stage of an answer.
• Click on the Back up button to go back a stage.
• To control the direction in which the derivation is developed, select a line (by clicking or using the Up and Down buttons) and click on the Gap, Main, or Auxiliary button to choose it as the gap to develop, a resource to exploit or goal to plan for, or a second resource for a detachment rule. Clicking with the shift key down will remove any selection.
• The Edit arg button will open a window with spaces for editing the premises and conclusion or typing your own. You may use either English or ascii notation (see below for a key)—or mix them. For English entry of quantifiers, use all and some; you can use st in place of the colon in a restricted universal but you should group the restriction with the quantifier symbol using parentheses as in symbolic notation.
• The text box at the right can be used to enter a term to use in exploiting generalizations. You will need to use the return key to have your choice accepted (and watch the box because it is automatically erased after certain operations). With some browsers you will also be able to use a menu to choose a term; you need to select a gap before any choices are listed.
• Other menus at the right let you (i) choose whether the derivation is displayed in symbols, in a basic set of ascii characters (see below), or in English (with some extra parentheses), (ii) choose to limit examples to earlier chapters, and (iii) choose the size of type for the display.
• There is also a checkbox that allows you to choose whether or not detachment rules will be used in the answer; to generate answers that do not use them, click on the box to uncheck it.