Need help?  •  Forgot your password?
This web site will be decommissioned in June 2019. Visit our new site here.

Support

Documentation


Hyperproof

This manual explains the mechanics of operating Hyperproof. Readers who are working through the book from beginning to end will not need to read the manual all at once to use the program. However, many features that make it easy to use Hyperproof are explained here, so it is a good idea to skim this material at some point. Readers who are skipping chapters will need to read this manual with more care.

Launching the program

You launch Hyperproof in the standard way, by double-clicking on its icon. Launching Hyperproof brings up a single window that we call a proof window. More proof windows may be created using the File ▸ New Window (⌘N/Ctrl-N) command or by opening files. There will be one proof window for each proof under construction.

The proof window

The proof window is divided vertically into two main areas, or panels. The situation is displayed in the left panel, and the proof steps in the right panel.

You can adjust the relative sizes of the situation and proof panels by by dragging the line between them to the left or right. You can hide the situation panel entirely, thus giving yourself maximum room in the proof panel, using Situation ▸ Hide Situation (⌘U/Ctrl-U). To show the situation again, choose Situation ▸ Show Situation (⌘U/Ctrl-U). If you are working on a purely sentential proof, you will probably want to hide the situation.

The situation panel displays the situation, which has a toolbar below it. The proof panel contains a main area which displays the proof, with a toolbar at the top and the goal strip at the bottom. If you have just started up Hyperproof, the bottom (goals) strip will not be visible. To see it, choose Goal ▸ Show Goal Strip (⌘T/Ctrl-T). To hide it, and give yourself more room in the proof panel, choose Goal ▸ Hide Goal Strip (⌘T/Ctrl-T).

At the extreme bottom of the proof panel, under the goal strip, is the status bar, where comments and error messages are displayed. The status bar is initially blank, but it is used to present a lot of useful information, especially when proof steps don't check out.

Across the top of the window is the main toolbar containing tools for common operations on the whole proof. Of particular importance on the toolbar is the help button at the extreme top right of the window.

Opening and saving files

You open and save files in Hyperproof in the usual way. To open a file saved on your disk, choose File ▸ Open... (⌘O/Ctrl-O). You will then use the open file dialog box to find the file you want. To start a new file, choose File ▸ New Window (⌘N/Ctrl-N).

To save a file, you either choose File ▸ Save (⌘S/Ctrl-S) or File ▸ Save As.... The difference between these is that the second command allows you to save the file under a new name. If you open a file named File One, make changes, and then save it as File Two, you will end up with two files on your disk: File One, which will be untouched, and File Two, which will contain your changes.

Most of the problem files on the Hyperproof disk are saved as templates or stationery pads. When you open a stationery pad named Proof 1.7, the window will be titled Proof 1.7 Solution. The first time you save it, you will be given a chance to change this name and put the file in another folder, should you so desire. In saving solutions to problems assigned from this book, you usually won't need to change the name, but you may want to put your solutions into another folder to be turned in.

Quitting the program

To quit the Hyperproof application, choose File ▸ Quit (⌘Q/Ctrl-Q).

Editing the situation

The situation may be edited using the toolbar immediately below the displayed situation. This toolbar is shown below.

When you can and can't edit the situation

You can only edit the situation at appropriate points in the proof. All of the editing functions described below are allowed when you are editing the given situation, that is, when the focus slider (the small triangle on the far left of the proof) is pointing at the top situation icon. When you start up Hyperproof or open an existing file, the focus slider always points at the top situation icon.

To edit the initially given situation, Hyperproof must be in author mode, which can be turned on or off by choosing Edit ▸ Author Mode. Hyperproof is in author mode whenever you start a new file; it will not be in author mode when you are working on an exercise whose basic setup you are not supposed to change.

It is only possible to edit the situation when the focus slider is pointing at either a step that contains a situation, or at a step that is empty. Otherwise it is not possible to edit the situation at all. For example, if you are at a step in the proof that contains a sentence, then introducing situation changes at that point is not allowed, and so the editing buttons on the situation toolbar will be dimmed.

At other points in the proof, you will only be able to perform the editing functions that make sense at that point in the proof. For example, at a proof step that allows you to extend the current situation, you will be able to specify new information --- say, by specifying the shape of an unknown block --- but you will not be able to change or take away any of the definite information that is already present in the current situation. For example, at such a step you will not be able to add or delete blocks, or turn a tetrahedron into a dodecahedron.

If you find yourself unable to edit some attribute of the displayed situation using the instructions given below, you should check to see whether the focus slider is pointing at the right step. In general, of course, you should not change any of the given information in an existing problem. If you are trying to edit the given situation but can't make any changes, you should check on the Edit menu to make sure Author Mode has a check next to it.

How to edit the situation

To add a block, click on the New Block button on the far left of the toolbar or choose Situation ▸ New Block. The block will appear in the blank area to the right of the grid. New blocks can only be created when you are focussed on the given situation and author mode is switched on.

To edit a block, it must first be selected. After adding a new block, it is automatically selected, so it can immediately be edited. To select an unselected block, you simply click on it.

You can select multiple blocks by control-clicking the blocks (click on the blocks while holding down the control key. On the Macintosh operating you shift-click instead). When you have selected multiple blocks, editing affects them all.

  • Location: To move a block, simply click on it and drag it to its new location. If you first select several blocks and drag one of them to a new location, all of the selected blocks will move by approximately the same amount.
  • Shape: To change the shape of a selected block, click on one of the shape buttons (indicated with a tetrahedron, cube, and dodecahedron) on the toolbar. To make the shape of the block unknown, click on the button corresponding to its current shape, which acts as a toggle. If several blocks are selected, the change will apply to all of them. If they are not already the same shape, the first click will make them so, and a second will make them all of unknown shape.
  • Size: To change the size of a selected block, click on one of the size buttons (indicated with three variously sized circles). To make the size of the block unknown, click on the button corresponding to its current size.
  • Names: A block may have any number of names, from among a through f and n1 through n9, but each name can belong to at most one block. There are buttons on the toolbar for the names a through f. To name a block, select it and click the appropriate name checkbox. Buttons corresponding to names already assigned to other blocks will be dimmed. If you select more than one block, all name buttons will dim, since you cannot assign the same name to more than one block. To remove a name from a block, select the block and click the button of the name to be removed.

    Name buttons for n1, ..., n9 appear on the popup menu indicated by a downward pointing arrow. To name a block n1, say, select the block and then click down on the arrow on the toolbar. A menu will appear from which you can choose the name n1. Perform the same operation to remove an existing name from a block.

  • Happiness: A block's happiness is indicated by a face on the block. If the block's happiness is unknown, then no face is displayed. To change a block's happiness, select the block and click on one of the mood buttons to make it happy, or not happy. As before, you can return the block to unknown state by clicking again on the button corresponding to its current happiness. You may select multiple blocks and change them all simultaneously.

To delete a block, you must select it and then choose Situation ▸ Delete Block, or hit the Delete key on the keyboard. Several blocks can be deleted at once by first selecting them and choosing Situation ▸ Delete Blocks or hitting Delete on the keyboard. Blocks can only be deleted when you are in author mode and focused on the given situation.

Editing likes information

Information about which blocks like which is shown by arcs. If block a likes block b, an arc appears from a to b, labeled with a red heart and an arrow pointing toward b. If a does not like b, then the arc is labeled with a grey upside down heart. If it is unknown whether a likes b, no arc appears.

If you want to add the fact that one block likes another, first click on the New Likes Arc button toward the right of the toolbar. When this button is depressed, dragging between blocks will create a likes arc. An arc will follow as you drag and affix itself to the block where you release the mouse button. (Note that the source and destination block may be the very same block.) The arc will, by default, display the red heart. Once the arc is completed the button is deactivated, and dragging again moves blocks. To add more arcs, you'll need to select the likes arc button again.

Alternatively, without using the New Likes button, you can hold the Option or Alt key down while clicking down on the first block then drag to the second.

If you want to add the fact that one block doesn't like another, follow the exact same procedure. But when you have finished dragging the arc, go back to the situation toolbar and click on the button showing the upside-down heart. This will replace the heart with a upside-down heart. Alternatively, if you hold the Shift key down as you drag a likes arc from one block to another, the arc will immediately be labeled with an upside-down heart.

To change an existing arc, first display the arc by selecting the block of origin if necessary. Then click on the arc's heart label (or upside-down heart). Once this selected you can click on the opposite shape heart button (on the toolbar) to switch the heart's direction (make a likes arc a dislikes arc or vice versa) or click on the button of the same shape the heart already has to make the arc disappear completely. (If the heart buttons on the toolbar are greyed out, it's because you haven't selected the label you want to change or because you aren't in Author Mode.)

You cannot edit more than one arc label at a time.

When there are a lot of likes arcs in the situation, it is sometimes hard to see what is going on. This can be solved by viewing the likes arcs originating at individual blocks, one at a time. To do this, turn off Show Likes and Happy, using the button on the situation toolbar which shows blocks with arcs between them. This toggles between the Show Likes and Happy settings. Then you can select a single block to display any likes arcs that originate at that block.

Other situation manipulations

To toggle between 2-D and 3-D views of the situation, use the button on the far right of the toolbar, choose Situation ▸ 2-D View or Situation ▸ 3-D View, or type (⌘Y/Ctrl-Y). When you are viewing the situation in 2-D, you may want to expand the situation panel, particularly if the situation contains happy information. All of the editing functions work in either view.

The body of the proof

To the right of the situation display is the proof panel, which has the sentence toolbar at the top, followed by the steps of the proof. The sentence toolbar is shown below.

In this section, we explain how to modify and navigate around a proof. Before doing this, we present a list of some of the graphical elements you will encounter in the proof panel:

  • Focus Slider. The focus slider appears just to the left of the proof and points to the currently focused step.
  • Proof line and Fitch bar. Proofs and subproofs are demarcated by a vertical line. Attached to the line is a horizontal bar called the Fitch bar. The Fitch bar separates the assumptions of the proof from the steps that follow from those assumptions.
  • Unkown Content Icon. This icon appears as the content of a newly created step. It indicates that either a situation or a sentence may be placed into this step. If you make a change to the situation then this icon with change to a situation icon, and inserting a sentence by typing or using the toolbar with result in this icon being replaced by the sentence.
  • Empty Situation Icon. This icon appears at the top of the proof panel if there are no blocks in the given situation. If it appears at the top of a problem file that you open up, it indicates that there is no situation information, so a purely sentential proof is required.
  • Normal Situation Icon. This icon appears at every step containing new situation information. You should think of it as a placeholder for a situation.
  • Current Situation Icon. This is the highlighted version of the normal situation icon. It indicates which situation is currently in force at the focused step (see below). It is also the situation that is currently being displayed in the situation panel.
  • Constant Box. The constant box appears at the top of subproofs in which a new constant or constants have been introduced. The constant box depicted here indicates that a is a newly introduced constant.
  • Collapsed Subproof Icon. This icon appears when you collapse a subproof to save space in the proof panel.

The current focus

As you work on a proof, there is always one step that is in focus. This step is indicated by a small triangle on the far left of the proof, called the Focus Slider. The focused step is the step affected when you perform any of the editing functions.

Moving the focus

There are several ways to change the focus from one step to another. First, you can drag the focus slider up and down, or simply click in the focus slider area next to the step you want to focus on. Alternatively, you can use the arrow keys on the keyboard to move the focus up and down.

Clicking on a step other than the currently focused step won't move the focus, unless you click in the focus slider area to the left. This is because clicking on steps is the way we enter supports for the currently focused step.

The current situation

As you move the focus around a proof, the situation display will change. What is shown in the display is the current situation at the step in focus. The current situation is the one in force at that point in the proof. It is, for example, the situation in which a sentence would be evaluated if you were to use the Observe rule at that step.

When you change the situation in the course of a proof, the new situation becomes the current situation. It remains current until you either change the situation again, resulting in a new current situation, or else end the subproof in which that situation occurs. When you end a subproof, the current situation reverts back to the one in force outside of the subproof. (Subproofs are explained below.)

In the body of the proof, the situation icon corresponding to the current situation is always highlighted.

Adding new steps

To add a new step to a proof, choose Proof ▸ Add Step After or Proof ▸ Add Step Before.

There are two keyboard equivalents for the Add Step After command. You can either type ⌘A/Ctrl-A or Shift-Return (that is, type a return while holding down the shift key). You can type ⌘B/Ctrl-B as a shortcut for Add Step Before.

Add Step Before and Add Step After will give you a new proof step immediately before or after the step you were focused on, unless you were focused on a Premise step, in which case the new step will be the first step following the premises. (To find out how to add new Premise steps, see later.)

To add a step at the end of the proof, focus on the last step of the proof and choose Add Step After. To insert a step in the middle of a proof, focus on the step you want the new step to follow and choose Add Step After.

New steps added within a subproof will appear in the same subproof. Starting and ending subproofs require slightly different commands. These are described later.

Entering sentences into steps

When you add a new step, an empty new step appears. At this point you can either modify the situation or enter a sentence. To enter a sentence, either use the sentence toolbar or type directly from the keyboard. To type the logical symbols from the keyboard, refer to the list of keyboard equivalents found below.

Symbol¬
Keyboard Equivalent~#&|$%@/

Deleting steps

To delete a step, focus on the step and choose Proof ▸ Delete Step (or type ⌘D/Ctrl-D). If you delete the assumption step of a subproof, the entire subproof beginning with that step will be deleted.

If you accidentally delete a step or subproof, you should immediately choose Edit ▸ Undo Delete Step. This will undo the deletion, but will not work if you have done anything else in the meantime.

You can quickly delete a range of steps by using the selection rectangle. This is explained below.

Specifying a step's rule

When you add a new step, the word Rule? appears to the right of the step. To specify a rule for the step, click down on the word Rule? A popup menu will appear to the right. You can then select the rule you want by dragging the cursor over the appropriate rule name and letting go of the mouse button.

There are three special items on this popup menu, labeled Con, Elim, and Intro. Dragging the cursor over these menu items will cause a second menu to appear with a list of further options. To specify the rule of, say, Negation Elimination, first move the cursor over the item Elim. Then, when the second menu appears, drag the cursor to the item ¬ and release the mouse button. This operation is illustrated below. Similarly, to specify the rule of Taut Con, first move the cursor over the item Con and then choose Taut from the second menu.

The rule determines the type of information (sentence, situation change, or declaration) that you can introduce at the step. When you specify a rule that requires a situation change, you will not be able to enter a sentence. Similarly, when you specify a rule requiring a sentence, you will not be able to modify the situation. When you choose an enabling rule, boldface text will appear stating the rule's declaration.

You can also specify a rule from the keyboard, by typing the appropriate keystroke equivalent. A list of these appears below. Note that in using these keyboard equivalents, you should not hold down the shift key unless it is explicitly mentioned in the table. For example, to specify the rule ∀ Elim, you will actually type Option-2; holding down the shift key will change the rule to ∀ Intro instead. We have listed the shifted (uppercase) characters because they are easier to remember. For example, it is easier to remember that ∧ Elim is Option-& than to think of it as Option-7.

RuleKeyboard EquivRuleKeyboard Equiv
ApplyControl-Option-PNameControl-Option-L
CloseControl-Option-CObserveControl-Option-O
CTAControl-Option-KTrust MeControl-Option-Z
ExhaustControl-Option-XAna ConControl-Option-A
InspectControl-Option-SFO ConControl-Option-F
MergeControl-Option-MTaut ConControl-Option-T
∧ ElimOption-&∧ IntroShift-Option-&
∨ ElimOption-|∨ IntroShift-Option-|
¬ ElimOption-~¬ IntroShift-Option-~
⊥ ElimOption-^⊥ IntroShift-Option-^
⟶ ElimOption-$⟶ IntroShift-Option\$
⟷ ElimOption-%⟷ IntroShift-Option-%
= ElimOption-== IntroShift-Option-=
∀ ElimOption-@∀ IntroShift-Option-@
∃ ElimOption-?∃ IntroShift-Option-?
≥ n ElimOption-Q≥ n IntroShift-Option-Q

To change the rule of an existing step, you must first move the focus to that step. Then, specify the new rule using either the popup menu or the keystroke equivalents.

If there are situation changes at the step, you will not be able to specify a rule that does not permit situation changes (for example Observe or Inspect). To change to such a rule, you must first choose Situation ▸ Revert Situation. This will remove all the modifications that were made to the situation at that step and allow you to change to any of the rules. Similarly, if there is a sentence at the step, you must first delete the entire sentence before you can change to a rule that does not permit sentences (for example Apply or Merge).

Specifying a step's supports

Most rules require that you cite other steps as justification or support. To specify the supports for a step, focus on that step and click on the steps to be cited. The steps you click on will highlight. If your support is a subproof, clicking anywhere in the subproof will highlight the whole subproof. If you click on a step or subproof already cited, it will be uncited.

The rule of Cases Exhaustive (not needed for purely sentential proofs) is a bit more complex. This rule has both support sentences and, in addition, one or more cases (i.e., subproofs) that are claimed to be exhaustive. So you need to specify both the cases that the declaration is about and the sentence or sentences that support the declaration. When you click on the cases, a bracket will appear to mark the cases. When you click on the sentence(s) supporting your claim, these will be highlighted.

To see a step's supports, you must focus on that step. The supporting steps will then become highlighted. To change a step's supports, focus on the step and click on the steps you wish to add or delete from the step's supports.

Some sentence rules can work out the required supports on your behalf. For example, if you create a step containing the formula P ∧ Q and choose the ∧ Intro rule, then you will need to cite two steps containing the sentences P and Q respectively. Using the command Proof ▸ Add Support Steps will do just this. When focussed on the step just described, this command will result in two new steps being created, containing the appropriate sentences. You must have entered a sentence and chosen the rule for this command to be enabled.

Not all sentence rules have the ability to work out the required support steps from the conclusion. For example, if you create a step containing P and select the ⟶ Elim rule then the Add Support Steps command will be disabled. The supports that you need are of the form Q ⟶ P and Q for some sentence Q, but Hyperproof can't work out the sentence that should be used.

All of the introduction rules, except for Intro and the existential quantifier rules, permit you to add supports automatically. The rule of ∨ Intro guesses that the support sentence is the fist disjunct of the conclusion. Of the elimination rules, only ∧ Elim, ¬ Elim, Elim and ∀ Elim have automatic supports.

Checking steps

To check whether a step is correct, focus on the step and either press the Check This Step button on the main toolbar or click on the status line at the bottom of the window. You can also check a step by hitting the Enter key on the numeric keypad or the Function (marked fn, usually lower left and only on keyboards with no numeric keypad) Return key combo.) You can check all of the steps in your proof by choosing Proof ▸ Verify Proof, or by using the Verify Proof button from the proof toolbar.

After you check a step, one of four symbols will appear to the left of the rule name. A check mark means that the step is logically correct. An X means that the step is logically incorrect. An asterisk means that the sentence at that step is not syntactically well-formed. Finally, a question mark, which appears on a Cases Exhaustive or Apply step, meaning a possible (rather than a definite) counterexample was found, or on an application of FO Con or Ana Con which means that the proof took too long, or involved the use of the predicates Between or Adjoins.

If you do not get a check mark for one of your steps, focus on the step and look at the message in the status line. It may provide you with some helpful information about why your step is incorrect.

Rule defaults

Many rules have defaults that can save you considerable time when constructing a proof. For example, when you apply the Merge rule, you generally want to extract all of the situation information that is common to an exhaustive range of cases. Rather than re-enter this information at the Merge step, Hyperproof allows you to choose the Merge rule from the popup menu, specify the required support step (an Exhaustive step), and Check This Step. When you do this, Hyperproof will automatically make all situation changes allowed by the rule.

To give a sentential example, if you choose the rule ⟶ Elim, cite two sentences of the form P ⟶ Q and P, and then Check This Step, Hyperproof will automatically fill in the step with the sentence Q.

Some rules do not have defaults. When you invoke the Observe rule, for example, there is no way for Hyperproof to know which sentence you have in mind and so your sentence must be typed in by hand. The rules that do not have defaults are Ana Con, Apply, Inspect, FO Con, Observe, Taut Con, and Trust Me. Defaults for the other rules are described in the body of the book.

To get Hyperproof to provide a default for a step, the step must be empty. In other words, there must be no situation or sentential information that you have put in yourself. If the step is empty, then when it is checked---whether by hitting Enter, clicking in the status bar, or choosing Verify Proof---Hyperproof will try to provide a default for that step.

Starting and ending subproofs

A subproof is started by using the Proof ▸ New Subproof command. If the focus step is empty, then this step will become the assumption of the new subproof, otherwise the new subproof will be added immediately after the focus step. Once you are within a subproof, any new steps you add will also be in that subproof. So to add a step after a subproof, you need to know how to end the subproof.

To end the subproof, focus on the last step and choose Proof ▸ End Subproof. This will end the subproof and give you a new step following that subproof.

If, when you do this, the last step of the subproof is a new (empty) step, then that step will just be moved out of the subproof. This means you can end two embedded subproofs by choosing End Subproof twice. The first time, you will end the innermost subproof and get a new step in the outer subproof. The second time, the new step will be shifted out of that subproof as well.

There are two keyboard equivalents for End Subproof: you can either type (⌘E/Ctrl-E) or type Alt-Return (that is, type return while holding down the Alt key---the option key on the Macintosh).

When you are in a subproof that is enclosed by a Cases Exhaustive bracket, you cannot end the subproof. You can, however, add a new case (a new subproof) to the bracketed range of cases. In this circumstance, the End Subproof command is replaced on the Proof menu by the command Add Case. The keyboard equivalent for Add Case is also (⌘E/Ctrl-E).

Boxed constants in subproofs

A downward-pointing triangle appears to the left of the assume step of each subproof. This triangle indicates the existence of a popup menu. If you click down on it, while focussed on the step, the menu will appear. In this case, the menu presents you with a list of all the names available in Hyperproof. Choosing one of these names causes it to be added as a boxed constant---unless it is already boxed, in which case it is removed from the box. Boxed constants are used in the rules Name, ∀ Intro, and ∃ Elim.

Exhaustive cases

A exhaustive range of cases (not needed in purely sentential proofs) can be constructed quickly by means of the Proof ▸ Exhaustive Cases and Proof ▸ Add Case commands. Exhaustive Cases gives you a single subproof, already enclosed in a bracket and followed by an Exhaustive step. It leaves the focus on the Assume step of the subproof so that, once you finish this subproof, Add Case will create another subproof, also enclosed in the Cases Exhaustive bracket.

If you enter support steps before choosing Exhaustive Cases, then these supports will be taken as the supports for the Exhaustive step following the cases. Thus the fastest way to break into cases is to add a step, specify the supports you will be using for the Exhaustive step, choose Exhaustive Cases, and then specify your cases one by one.

If you forget to cite support sentences before choosing Exhaustive Cases, then after you finish specifying your cases you will have to move down to the Exhaustive step to cite its supports. To do this, move the focus to the Exhaustive step and then click on the sentences that support this claim.

Collapsing subproofs

Long subproofs can be collapsed so that they take up less room on your screen. To collapse a subproof, choose Proof ▸ Collapse Subproof (⌘-/Ctrl- -) while focused on any step in the subproof. The subproof will be replaced by a single subproof icon. If you are focused on a step of a subproof within a subproof, Collapse Subproof will first collapse the innermost subproof. Then if you choose the command again, it will collapse the outer subproof as well. To expand a subproof, focus on it and choose Proof ▸ Expand Subproof (⌘=/Ctrl-=) .

When a subproof is collapsed, it does not display a rule name, but rather the words Open or Closed. This indicates whether the Close rule has been invoked within that subproof.

A checkmark to the right of a collapsed subproof means that every step in the subproof checks out; an X means that at least one step does not.

Deleting subproofs

To delete a subproof, focus on the assumption step that begins the subproof and choose Proof ▸ Delete Step (or type ⌘D/Ctrl-D). When you delete a subproof, you can get it back if you immediately choose Edit ▸ Undo Delete Step. Once you move the focus or add a step, you can no longer undo the deletion.

Goals

The goals for a problem are represented by icons that appear in the goal strip at the bottom of the proof window. If the goal strip is not visible and you would like it to be, choose Goal ▸ Show Goal Strip (or type ⌘T/Ctrl-T). If the goal strip is visible but you would like more room for the proof, choose Goal ▸ Hide Goal Strip (or type ⌘T/Ctrl-T).

Different icons represent different types of goals. To get a detailed explanation of a goal, open it by double clicking on its icon. Then, if you want an explanation or reminder of how to satisfy the goal, click on the Help tab.

A quick way to find out about your goals is by goal peeking. To peek at your goals, select (click once on) each of them in turn. Key information will appear in one of two places, depending on the type of goal you have selected. If the goal asks you to prove a sentence, then when you select its icon, the sentence is displayed in the status bar. If a goal asks you to prove something about a block, then when you select the icon, the block in question is highlighted in the situation. (Name goals and consistency goals don't do anything when you select them, since their icons carry all the information you need.)

When you are working on a problem and think that you have satisfied one or more of the goals, choose Proof ▸ Verify Proof, or type (⌘F/Ctrl-F) . At that point, one of three things will happen. If your proof contains any incorrect steps, then a message on the status bar will say that goals can only be checked when all proof steps are correct. But if the proof steps all check out, then either a check or an X will appear under each goal icon, depending on whether the goal has in fact been satisfied in the proof.

When an open question goal checks out (for example, a goal that asks whether a sentence follows from the given), the checkmark will also have a small exclamation point or circled exclamation point indicating whether the answer to the goal's question is yes or no.

If you click on the red X associated with a goal, the goal window will appear with a description of what you need to do to solve this kind of goal.

Copying and pasting

Hyperproof allows you to cut, copy, and paste various parts of a proof. Mastering these operations will make the construction of proofs much easier.

When you cut or copy something from a proof, it is placed on the clipboard. The clipboard stores whatever you have cut or copied so you can later paste it somewhere else in the proof. The difference between cut and copy is that the former deletes the item in question from its current place in the proof, while the latter leaves the proof itself untouched, and stores a copy of the item on the clipboard.

Once something is on the clipboard, you can paste copies of it into the proof as many times as you want. It will remain on the clipboard until something else is cut or copied, at which point the new item replaces what used to be on the clipboard.

Copying and pasting sentences

To cut or copy a sentence, or part of a sentence, you must first be focused on the step that contains the sentence. Select the portion you want by clicking down at one end and dragging to the other, holding the mouse button down as you drag. Once it is selected, choose Edit ▸ Copy (⌘C/Ctrl-C) or Edit ▸ Cut (⌘X/Ctrl-X) . Both of these commands place a copy of the selected text on the clipboard; the second simultaneously deletes it from the step.

If you want to copy an entire sentence from a step, simply focus on the step and choose Edit ▸ Copy. There is no need to select the sentence. This places a copy of the whole sentence from that step on the clipboard, ready to paste elsewhere in the proof (or in another proof). This shortcut is particularly useful if you want to copy one of the given sentences when author mode is off, for in that case the given sentence will be locked and you will not be able to select it.

Once the sentence is on the clipboard, you can paste it into another step by moving to that step and choosing Edit ▸ Paste (⌘V/Ctrl-V) . The step must be one that accepts sentences---you cannot, for example, paste a sentence into an Apply step. The text will appear wherever text typed from the keyboard would, so if you want to paste it into the middle of some existing text, make sure the blinking insertion point is located where you want the text to appear.

Copying and pasting goal sentences

If one of the goals of a problem is a sentence goal, you can save some typing by copying the goal sentence from the goal window and pasting it into your proof. To do this, open the goal by double clicking on the icon in the goal strip. When the window opens showing the sentence you are asked to prove, right-click (on the Mac, hold down the control key while clicking) and select Copy Sentence from the popup menu that appears. Then move back to the proof window and paste the sentence into the desired step.

Copying and pasting situations

If you are focused on an empty step that contains a situation icon, say an Assume step, you can copy the current situation by choosing Edit ▸ Copy (⌘C/Ctrl-C) . You can then place this situation at another step in the proof by focusing on that step and choosing Edit ▸ Paste (⌘V/Ctrl-V) . If the focus step is empty, then the situation will be pasted into that step, otherwise a new step will be created immediately after the one in focus, and the situation will be pasted there.

This is useful if you are breaking into several cases that are similar in many respects and differ in just a few. In that circumstance, you can build one case, copy the assumed situation, and then paste it into the remaining cases, making whatever modifications are necessary in the subsequent cases.

When you paste a situation that you copied from another point in the proof, it may turn out that the current situation at the step where you want to paste conflicts in some way with the situation on the clipboard. For example, one and the same block might be a cube in the current situation and a tetrahedron in the clipboard situation. If this happens, a dialog box will appear, warning you of the conflict. If you click Paste, then Hyperproof will paste as much of the clipboard situation as is consistent with the situation current at that point in the proof. It will never change any definite information contained in the current situation.

You can also copy a situation from one proof and paste it into another. But for this to work well, the situation in the second proof must be relatively similar to the situation in the first proof. Otherwise, Hyperproof will not be able to tell which blocks you consider to be the counterparts of the blocks on the clipboard, therefore it will not know where to make the situation changes.

Cut Situation (⌘X/Ctrl-X) works the same way as Copy, except that any situation modifications that are made at the focused step will be deleted (though they will remain on the clipboard). Cut will not delete any situation information that was introduced at an earlier step.

Copying and pasting from the counterexample window

When Hyperproof finds a counterexample in checking a Cases Exhaustive or Apply step, you can copy the counterexample situation and paste it into your proof. With the counterexample window active, right-click (or on the Mac, hold down the control key when clicking) and select Copy Situation from the popup menu that appears. Then move back to the proof window, focus on the step where you would like to paste the situation and choose Edit ▸ Paste Situation.

Copying and pasting ranges of steps

Hyperproof allows you to cut or copy a range of steps and paste them at another location in the same proof or in another proof. This is especially useful if your proof requires several similar subproofs, each containing a similar sequence of steps.

To select a sequence of steps, move the focus on the first of the steps that you want to select, and then shift-click on the last step you want to select. The steps will be highlighted by a gray rectangle. If the rectangle doesn't contain the steps you want, click somewhere else in the proof and the rectangle will disappear. You can then try selecting the steps again. Note, however, that Hyperproof will not allow the selection rectangle to cut a subproof in half: you must either select steps entirely from within a subproof, or else select the subproof as a whole.

When the rectangle contains exactly the steps you want, choose Edit ▸ Cut or Edit ▸ Copy. Both of these commands place a copy of the steps on the clipboard; Cut also deletes the selected steps from the proof.

Once a sequence of steps is on the clipboard, choosing Edit ▸ Paste will insert the steps at the point of focus. If you are currently focused on an empty step, the pasted steps will replace the empty step. If you are currently focused on a step that is not empty, the pasted steps will be inserted after the focused step. If steps are selected when you use the paste command, the pasted steps will replace the selected steps.

If you want to paste steps into your proof immediately following a subproof, but not as part of the subproof, you will have to end the subproof before pasting. This will give you an empty step outside the subproof and Paste Steps will replace this empty step with the steps on the clipboard.

When you paste steps into a proof, Hyperproof will try to keep track of the appropriate supports for those steps. Sometimes, though, the supports for the pasted steps will no longer be legal in the new location, for example if you paste a step into the proof at a point earlier than one of its support steps. In such cases, Hyperproof will remove the illegal support from the step's list of supports.

Note that this also gives you a handy way to delete a large number of steps. Rather than repeatedly choosing Proof ▸ Delete Step, simply select all of the steps you wish to delete and choose Edit ▸ Clear. Simply hitting the Delete key will also delete the selected range of steps.

Printing

To print your proof or situation, choose File ▸ Export HTML, or the print icon on the the main toolbar. This will export the proof and/or situation to a new tab in your default browser. From there you can print. Note that you should print with background colors and images turned on.

Preferences

On a Macintosh, Hyperproof also has preference settings which may be changed from the Preferences window, which is obtained by using the Preferences command from the Application menu (Macintosh), or Edit menu (Windows). If you use this command, a window similar to that shown below will appear. The only choice in the preferences is Use Native File Chooser (and only visible in MacOS) which is shared with the Submit application; in almost all cases you should leave it checked.

Setting up problems

To create a new problem or modify an existing problem, you must be in author mode---that is, there must be a check next to Author Mode on the Edit menu. Hyperproof automatically puts you in author mode when you start a new file by choosing File ▸ New Window. But if you want to change a problem that was saved with author mode off, you must first choose Edit ▸ Author Mode to turn it back on. Author mode allows you to edit the given situation and the given sentences just as you would edit ordinary steps.

Adding and deleting premises

To add a given sentence, choose Proof ▸ Add Premise. If you are currently focused on a given step, the new given step will appear immediately after the focused step. If you are focused on a step in the body of the proof, the new given step will appear at the end of the given steps.

To delete a premise step, focus on the step and choose Proof ▸ Delete Step. You cannot delete the given situation.

Adding and deleting goals

To add a goal to a problem, chooseGoal ▸ New Goal... You will be presented with a dialog box showing the various types of goal icons. If you select one of the icons, the text associated with the goal will appear in the field at the bottom of the dialog box. When you have selected the desired goal type, click OK.

Many of the goals require additional information, for example the specification of a block, a name, or a sentence. If you are setting up one of these goals, a second dialog box will appear, asking for the additional information.

To delete a goal from a problem, select the goal in the goal strip and choose Goal ▸ Delete Goals. To delete several goals, select them all by dragging a rectangle around them (or by shift clicking) before choosing Delete Goals.

Saving new problems

When you have finished setting up a problem, turn off author mode before saving it. This will prevent users from accidentally changing the given information for a problem while trying to solve it. (Of course, author mode can always be turned on if the user intends to change the given.)

To save the problem, choose File ▸ Save As Problem.... A dialog will appear, asking whether you want to save the steps in the body of the proof. Then a subsequent dialog box allows you to name the file and choose the folder it should be saved in. Problem files behave differently from ordinary files: when a problem file called Filename is opened, it appears in a window titled Filename Solution. This makes it less likely that users will accidentally save their changes over the original problem file.

When saving a problem you will be asked whether to include the body of the proof. If you choose not to save the body of the proof,then only the givens and goals will be saved using the specified name, and author mode for the saved problem will be turned off. This allows you to set up a problem, solve it to make sure it can be solved, and then save it in two forms: as a problem (without the solution) and as a finished proof.

Projecting Hyperproof in class

If you are using Hyperproof with projection equipment, you may find that your students have trouble seeing parts of the proof, depending on the quality of your equipment and the size of the room. These problems can be solved by using a larger or bolder font and by darkening the proof lines. To make these changes, choose Window ▸ Font Size..., Window ▸ Font Style... or Window ▸ Darken Proof Lines.