 |
The EPGY Theorem Proving Environment is a computer program that enables students to write ordinary mathematical proofs. The system is used in a selection of computer-based proof-intensive mathematics courses, allowing students to easily input mathematical expressions, apply proof strategies, verify logical inference, and apply mathematical rules. Each course has its own language, database of theorems, and mathematical inference rules. The system uses a combination of automated reasoning and symbolic computation to verify individual proof steps.
This User Guide describes the individual features that allow students to write proofs in the system. Tutorial movies are also available to explain certain features. Some of the explanations in this user guide require familiarity with symbolic logic. Students who are unfamiliar with symbolic logic are encouraged to read the EPGY Logic Mini-Course Notes.
In order to use the Theorem Proving Environment, you must be running the EPGY Course Series System, version 3.0 or higher. If your EPGY course requires the use of the Theorem Proving Environment, you may access the Proof Environment Support Page through your course web page. Find installation instructions there.
Proof exercises will be served up by the EPGY Course Series System just like a lecture or Derivation System exercise.
A proof is basically a list of statements, each of which is justified by logical reasoning from a combination of other, already-justified statements together. Those may include axioms, theorems, and definitions, as well as given statement or other statements in the proof. In working a proof exercise, you are initially presented with some given statements and a goal, plus (perhaps) a database of axioms, theorems, and definitions. Your job will be to fill in the gap between the given statements and the final goal with a sequence of statements, or proof lines, that ultimately allow you to justify the final goal. New statements are added to the proof by directly inserting a new goal, or they can be generated automatically using proof strategies and inference rules. You will be able to move forward from your given statements, justifying new proof lines along the way, and you will be able to work backwards, reducing a goal to a new, simpler statement which must be proved.
A proof line consists of three parts:
These are shown in Figure 1.
The insertion point is the horizontal bar that appears in Figure 2 above the "final goal". You can insert proof lines directly by first placing the insertion point in the proof box and choosing "Goal" from the Insert menu as displayed in Figure 2.
To change the insertion point, first move your mouse vertically over the region of the proof box where the line numbers appear. When the cursor is in an available location, it will change into a horizontal bar. By clicking the mouse when the cursor appears as a horizontal bar, you will relocate the insertion point to that position.
After selecting "Goal" from the Insert menu, a new proof line will appear at the location of the insertion point, as shown in Figure 3.
The new proof line will be numbered automatically. The line can be renamed at any time during the proof. As in Figure 3, the justification line will have the word "By" and a blank that can be filled in with references to other proof lines, to given statements, or to axioms, definitions, or theorems from a course database (if one is open). More explanation on justifying proof lines is given later in this document. Finally, there will be a box where a statement can be entered, and you will be in MathEdit mode.
ProofEd is equipped with a structural input system that allows you to select special symbols from palettes and use to cutting and pasting, together with keyboard input, to create statements. This is the same tool that is used in the EPGY derivation system for algebra through calculus, but here you will use additional logical symbols. Structural input insists on meaningful, well-formed statements, and, to ensure that statements are well-formed, it imposes certain rules when constructing a statement. For example, if you write a statement involving the symbol "->" for the conditional, you will be required to include statements on either side of the symbol before your statement can be entered as a proof line.
As in other EPGY courses, when you are in math edit mode there will be a movable symbol palette for the creation of special mathematical and logical symbols. As it first appears on the screen, each of the icons on the palette corresponds to a symbol group. For example the symbol "&" identifies the logical symbol group. Clicking on it will expand the palette to look like Figure 4.
When you have finished entering a statement, press <ENTER> or
click the 
button to have your statement accepted. If your statement is not
acceptable, you will remain in math edit mode after typing
<ENTER> and will need to modify your statement in order to
continue. A statement could be unacceptable because of a syntax error
or for some other reason. To help you determine the error, the
portion of the formula that is not correct will be highlighted.
Note that each subject area in which ProofEd is used will have its own set of symbols and rules for the use of those symbols. Initially you will be using ProofEd for propositional logic, where you will use the lower case letters "p", "q", "r", "s", and "t" (and no others!) for propositions. Later when you use ProofEd for predicate logic, you will be able to use letters in the following way:
| Predicates: | A, B, C, …, X, Y, Z |
| Function Symbols: | f, g, h |
| Variables: | u, v, w, x, y, z |
For a goal to become useful in your proof, it needs to be verified. One procedure for verifying a goal is to first enter justifications on the justification line and then use the "Verify" command from the Tools menu. You may use (almost) any proof line, as well as any of the given statements, to justify a new proof line. Additionally, axioms, definitions, and theorems from a database can be used as justifications. There are two ways to use a given statement or an already-verified proof line as a justification:
 |
Once you have entered justifications that you think are sufficient for verifying your proof line, you can select the proof line by clicking on it, then go to the Tools menu and select verify. At that time an automated reasoning system (known as Otter) is run on your statement and list of justifications. You will be notified whether or not the system is capable of verifying your statement based on the listed justifications. If it is verified, the statement will be marked as proved, and it will then be available for use in justifying other proof lines. The system may fail to verify your proof line for various reasons, and they are discussed below.
Think of the proof editor, in this situation, as an intelligent tutor looking over your shoulder and nodding when he sees that your reasoning is correct. When ProofEd indicates "not proved", it is merely saying "I just don’t see that it follows," and it becomes your obligation to explain your reasoning more clearly either by giving more complete justifications or by breaking your logic down into smaller steps.
When you open an exercise, it will include a database containing axioms, definitions, and theorems that can be used as justifications in your proofs. The contents of the database will change as you progress through the course. The program offers some search tools to help you find a particular entry in the database. To use a database item to justify a proof step, simply drag it from the database onto the justification line of the step. You may also drag an axiom or theorem or definition into the proof itself, where it will appear as a new, justified proof step.
In addition to the verify command, ProofEd provides several standard proof strategies and inference rules that can be used to justify proof steps. These rules and strategies impose a natural logical structure on your proofs and are described below. Many rules can be applied in both the forward or backward direction. See the Strategies menu, the Rules menu, and the right-click menu for descriptions of how to use the various rules and strategies.
Below is a brief description of the various components of the theorem proving environment.
Use the File menu to access both proof files and exercises, as well as any databases of theorem, axioms, or definitions.
The "New" and "Open..." options allow you to open
a new or an existing proof (.proof) file.
The "Open Theorems Database" option is useful for a problem
in which theorems, axioms, or definitions are stored across multiple
database (.thdb) files. A database will open
automatically when you open your proof, but you can use this option to
open another..
Selecting "Renumber" will change all the line-numbers of proof steps so that they appear in sequential order. It will not change the order of any proof steps, merely change the numbers so they match the order.
Selecting "Collapse subproof" will cause the contents of the selected subproof to disappear from the display. You may find this useful if your proof is very long. To collapse a subproof, first select the entire subproof by clicking on it (make sure not to click on any step within the subproof or else you will select the step instead), then choose the Collapse subproof command.
Selecting "Expand subproof" will cause the contents of a collapsed subproof to be displayed.
Select "Add comment" (or type <CTRL-M>) to add a comment to a proof step. This will add a line of text on top of the selected proof step. You may edit this line to make whatever comment you would like about the proof line. Simply double-click it to activate it. The contents of the comment have no meaning to ProofEd, but you may use the feature to keep notes on your proof.
The Insert menu provides ways to insert new statements into your proof "from scratch". You may insert a brand new formula that may be a useful intermediate step, insert a free assumption, define a new constant, or create other statements. The various kinds of statements which may be inserted are described below.
From the Strategies menu, you may select one of several techniques that will provide structure for your proof. For instance, to prove a statement of the form "p->q", you could choose the Conditional proof strategy. The various strategies supported by ProofEd are discussed below.
The Rules menu offers several ways to manipulate proof steps. Some of the rules allow you to create a new (hopefully simpler!) proof goal that will automatically justify the original. Others will create a new proof goal that is automatically justified by the original. The rules represent basic useful techniques for logical reasoning and their application should be fairly intuitive. They are explained in more detail below.
In the Tools menu, you will find various ways to justify proof lines. The "Verify" and "Conclude" commands are typically the most useful for purely logical inferences, while the derivation tools help with algebraic inferences. All the tools are explained below.
ProofEd can recognize several different mathematical syntaxes. You can see which language ProofEd is using by looking in the Course menu. You may not change the settings there; they are only for your information.
The choices under the Preferences menu allow you to change the appearance of your proof. The do not affect the content of the proof at all. With the exception of the "Font..." option, all the selections are "on" or "off", as denoted by checkmarks. The various options are explained below.
By right-clicking and holding on an expression in the statement of a proof line, you may highlight (in yellow) a variable or even a whole term. When you release the right mouse button, you will be presented with a short menu of actions. Choosing an action will insert a new proof line at the insertion point, as described below.
Many rules in the ProofEd system require the user to input several statements simultaneously. This may occur during the course of a substitution action if the substitution would cause a conflict of variable names, for instance. It may also happen using the proof by cases strategy, when the user will be asked to specify the various cases. And it will always occur when using the instantiation and generalization rules. Such inputs are handled through a special interface, the "Input Panel", described in this section. A rule requires the use of the input panel will point to this section as part of its description.
On creation of the panel, the first ? is active. To activate any other item, double-click on it.
To finish editing one item, click on the Structural Input Palette or
press the <ENTER> key. The system will make some simple checks
to ensure that your input is valid and then automatically activate the
next ?.
When there are no more ?'s to be filled in, click the Panel's button to submit the input. In some cases, such as instantiation and function definition, it may be natural to leave one or more ? unchanged. The will accept the input in such cases. If some required ?'s are not filled in, clicking the button will have no effect.
Clicking the button at any time will cancel the whole action.
During substitution or definition expansion, the current matches are displayed along the top of the Panel. These are written as
indicating that the "x" of the pattern is matched to the "k" of the target and that the "y" of the pattern is matched to the the "sin k" of the target.
The Structural Input Palette may obscure of of the Panel's buttons. If so, simply move the Palette.
The second line of the Panel displays the current, "relevant" expression. This expression is just a reminder. It cannot be edited, and it does not change as the assignments are entered. While you edit a particular variable assignment, the portion of the expression in which that variable appears is highlighted. For instance, when we are renaming the the l in Figure 6, the second summation is highlighted.
If applicable, a list of forbidden names is displayed under the statement
This list contains all the variables that would cause name-conflicts if assigned for the current variable. As focus changes to other assignments, the list of forbidden variables will change.
Inserting a "Given..." is similar to inserting a goal (below), except that the resulting statement is inserted in the "given" section at the top of the proof and taken as already justified.
This feature is not available when working proof exercises, but is available in "practice" mode.
By selecting "Given..." from the Insert menu, you can add a statement that will be taken as already justified in your proof. When working an exercise, you will typically not need to include any new givens. In fact, if you turn in an exercise with extra given statements added, it will not be counted as correct. If you are writing your own proof from scratch, of course, you will need to insert your own given statements. When you insert a given statement, you will immediately enter the structural input system.
By selecting "Goal..." from the Insert menu, you insert a new line into your proof at the current insertion point. You may not introduce any new independent variables in your new proof line. You will have to justify the new line with one of the Strategies, Rules, or Tools discussed elsewhere. You can add a proof goal to the middle of a proof by clicking to place the insertion point where you would like the goal to be inserted and then selecting "Goal..." from the Insert menu. As with inserting a given statement, inserting a goal will immediately place you in the structural input system.
Use the "New constant..." option from the Insert menu to give a name to a term in the proof. For instance, in a Linear Algebra proof about the matrices A and B, the term "AB-BA" might be important in several statements. In such a case, it might be convenient to declare that the variable C denotes AB-BA. This is the typical reason to use insert a new constant.
Selecting "New constant..." inserts a new proof line of the form
The left side of the equality must be filled in by a new variable (one not already appearing at that point in the proof). The right side of the equality must be filled in by a term. No new variables may be included on the right side of the equality.
When you click to accept the new proof line, the program will check that the
right side of the equality actually denotes a defined term. If it
determines that the term is valid, the statement will be marked
"Proved". Otherwise, the program will add definedness
conditions as proof obligations and
mark the statement "Provable by" them.
Choose "Definition of a Function..." from the Insert menu to define a new function. ProofEd will use the Input Panel to ask for the function definition, as shown in Figure 8.
Along the top line, we see that there is already a function named "f" in the proof (it is defined on line 1). So we may not call our new function "f".
On the next line, we see "Define ? as". Fill in the new function's name there.
On the next line, we see "? (?) = ?". The first ? will be automatically filled in with the function name. In the next, we should enter the variables of the function. In the last, we should enter the term defining the function.
On the last line, we see "whenever ?". We may optionally enter a relation limiting the domain of our new function. In the function definition of line 1, this ? was filled by "x > 1".
When the users clicks the button of the Panel, ProofEd does some automatic checking to verify that the entered expression is a valid function. In particular, it checks that the formula described after "whenever" is sufficient to guarantee that the term defining the function is itself defined. If it determines that the "whenever" formula is sufficient, ProofEd adds the function definition as a proof step marked "Proved" If it cannot determine that the formula is sufficient, it adds a proof obligation stating that the formula is sufficient then adds the function definition marked "Provable" by the obligation. It is then the user's responsibility to justify the obligation.
The "Identity statement..." option of the Insert menu is most useful in some of the more elementary courses using ProofEd. It inserts a statement of the form "x=x" into the proof, where x may denote any term. After selecting the option, the user is asked to provide the term, using the Input Panel, and the resulting statement is marked "Proved".
The "Definition of a number..." option of the Insert menu inserts a justified statement similar to "5 = 4 + 1" (the definition of "5"). After selecting the option, the user is asked to supply any nonzero integer to define.
You may prove conditional statements in either the "forward" or the "backward" direction.
For information about using the forward direction, see the explanation of "Insert an Assumption" under the Insert menu.
To work in the backward direction, first enter the proof line you would like to justify. Then select that proof step and choose "Conditional" from the Strategies menu, as in Figure 9. The result is similar to that shown in Figure 10.
Notice that the assumption (hypothesis) p is automatically filled in, as is the conclusion q. When you justify proof line A.100, proof line 1 will be justified, and its label will change from "By A" to "Proved By A".
Variables introduced by an assumption are treated as constants within the subproof. This means that they cannot be universally generalized within the subproof and they cannot be re-introduced in a deeper subproof. However, if a one of these variables comes out of a subproof (by using the Conclude tool, for instance), it will be considered an independent variable.
In general, statements inside of the subproof are not available as justifications for proof lines outside of the subproof.
The biconditional proof strategy can only be used in the "backward" direction. That is, you must first enter the proof line you would like to justify and then select the strategy: highlight the proof line and select "Biconditional" from the Strategies menu (as in Figure 11).
Since "p<->q" is equivalent to "p -> q & q ->p", you will have two conditional subproofs to complete. The result is shown in Figure 12.
In Figure 12, proof line A.1 is expanded into subproof B and proof line A.2 is expanded into subproof C. When proof line B.100 is justified, proof line A.1 will be justified and its justification line will change to "Proved by B". When proof line C.100 is justified, proof line A.2 will be justified and its justification line will change to "Proved by C". When both lines A.1 and A.2 have been justified, proof line 1 will be justified and its justification line will change to "Proved by A". Then line 1 may be used as justification for subsequent proof lines in the proof.
The statements and variables in all three subproofs (A, B, and C) are subject to the restrictions mentioned in the section on the conditional proof strategy (above). Please note, though, that you may use proof line A.1 or A.2 once it has been justified.
The proof by contradiction, or "indirect proof," strategy allows you to assume the negation of a statement, and by establishing a contradiction (a statement that logically implies "false"), justify the original statement.
You may use proof by contradiction in the backwards direction only. That is, you must first enter the proof line you wish to justify, select it with the mouse, and then select the "By contradiction" from the Strategies menu (as in Figure 13).
You will then be presented with a subproof where the hypothesis is the negation of your proof line and the conclusion is the statement "Contradiction". For example, in Figure 14, we have chosen the proof by contradiction strategy to justify the proof line "q". If, by assuming "¬q", we can justify the contradiction in line B.100, we will have justified proof line 1 and its justification line will read "Proved by B".
The strategy of "proof by cases" is applicable to any statement. Like the biconditional proof strategy, it can only be used in the backward direction (that is, the proof goal must be entered before the strategy is selected). To invoke the strategy, click on the proof step representing the goal and choose "By cases" from the Strategies menu.
The particular behavior of the strategy depends on what kind of statement the goal is:
As with other subproofs, the statements inside subproof B cannot be used as justification for proof lines outside subproof B, and similarly with subproof C. Also, variables in the subproofs are subject to the restrictions mentioned in the section on the conditional proof strategy (above).
Using this rule, you can work backwards from a universally quantified statement. Universal generalization in the forwards direction is explained elsewhere. As in the example, a common way to prove "FORALL x (P(x))" is to prove "P(y)" where y is an independent variable. To do this by the universal generalization rule, first select the proof line as in Figure 18, then choose the "By Universal Generalization" rule from the Rules menu. You will be prompted to choose a variable to replace x (you can usually choose x as the new name, but you might want to choose something else). Figure 19 shows the result after choosing y as the new variable.
The original proof line 1 is labelled as "Derivable from 2", meaning that it is not yet justified but will be justified as soon as line 2 is verified.
Using this rule, you can work backwards from an existentially quantified statement. Existential generalization in the forwards direction is explained elsewhere. To prove an existentially quantified statement, you will often need to supply a particular term to substitute for the quantified variable (there are other situations where the existential generalization rule will be useful, but this is the most common).
Using the existential generalization rule is similar to using the universal generalization rule with one major difference: you many use any term, not just a variable.
The following example is somewhat simplistic, but it illustrates the rule. To justify the claim that "EXISTS x (x > 1)", you will need to supply a term to substitute for x. Select the proof line and choose "By Existential Generalization" from the Rules menu, as in Figure 20. You will be asked to supply a term to substitute for x. In this example, we have chosen "2" to give Figure 21. Line 1 is not yet verified, but as soon as proof line 2 is justified, proof line 1 will become justified and its justification line will change to "Derived from 2".
Use definition expansion in either the forwards or backwards direction to use the definition of a relation from the Theorem Database or a function defined in the proof. To use the rule, select the definition to expand (either a Theorem Database item or a function definition) then right-click and drag to highlight a term in the proof. Then select "By Definition" from the Rules menu.
The behavior of definition is explained below.
Substitution is described below as part of the right-click menu. It may be invoked from the Rules menu as well by first selecting the equation to use, then right-clicking and dragging to highlight the term to be substituted, and finally selecting "Substitute" from the Rules menu.
Using this rule, you can use the proof lines "p" and "p -> q" to immediately justify the proof line "q". First, place the cursor where you would like the new proof line to appear. Then click on the proof line "p" (Figure 22). Then shift-click on the proof line "p -> q", giving something like Figure 23. Finally, select "Modus Ponens" from the Rules menu, as in Figure 24.
In the example shown, there is already a proof line "q" so no new proof lines are generated. Line 1 is simply justified and its justification becomes "Derived from a, b" (Figure 25). If there had been no proof line "q" available at the insertion point, one would have been inserted at the cursor, justified immediately, and its justification line would be "Derived from a, b".
There are two kinds of instantiation, "Universal" and "Existential". Universal instantiation begins with a statement of the form "FORALL y (P(y))" (where "P" represents any formula) and derives the statement "P(t)", where "t" is any term. Existential instantiation begins with a statement of the form "EXISTS y (P(y))" and derives the statement "P(x)", where "x" is a new variable. Either of these rules is carried out by highlighting a step and choosing "Instantiate" from the Rules menu, as in Figure 26.
For either rule, the user must specify the replacement for y. This is done using the Input Panel. In Figure 27, the user may specify terms to replace x and y.
The user may instantiate all or some of the quantified variables in a universal or existential statement. Entering "1" for x and "2" for y results in Figure 28. Entering "1" for x and nothing for y results in Figure 29.
The proof strategies and tools are useful for converting complicated proof goals into simpler proof goals which are arranged in a way that reflects their logical structures. When you would like to actually justify a statement, you may use the "Verify" command. The Verify command passes your statement and any justifications to an automated reasoning program known as Otter (a product of the Mathematics and Computer Science Division of Argonne National Laboratory). You do not need to know how Otter works, except to know that it can often tell whether one logical statement follows from several others.
For example, in Figure 30, the proof line A.100 is a direct
consequence of proof line A.1. To indicate this, the user has entered
"A.1" in the justification line for A.100 and is selecting
"Verify" from the Tools menu. The statements are
passed to Otter and it thinks for a moment. If Otter needs more than
a few seconds to verify your statement, a large "Interrupt the Prover"
button will appear. 
Use this button if you would like to abandon the verification and try
something else (if, for instance, the verification seems to be taking
too long). After Otter has completed its checking, a dialog box
appears reporting success or failure. After you click "OK"
to dismiss that dialog, the proof document looks like Figure 31 (if
the verification was successful): Proof line A.100 has been verified
and marked "Proved By A.1".
In this particular case, proof line 1 is also justified (because we happen to have used the conditional proof strategy to construct subproof A in the first place).
In some cases, the verify tool will fail to justify the proof line you have selected. Please be aware that there are several possible reasons for this:
You will not be given any information as to which case holds, so you will need to decide for yourself. In the first case, you will need to alter your proof goal. In the second case, you may need to add additional justifications. In the third case, you are taking too large a leap of logic and will need to first break your reasoning into smaller steps, then perhaps prove some intermediate results, and finally adjust the justifications and try again. Keep in mind that ProofEd is generally pretty good about verifying logical steps that are clear to the average user. Therefore, when it fails to verify a valid step it is likely that the logic you have used is too complicated for the typical user to easily recognize and understand.
Use the conclude tool in conjunction with the conditional proof strategy in the forward direction. In the example below, subproof A has hypothesis p and the conclusion, r, has been justified. So we can conclude "p -> r". To do this, select the entire subproof A by clicking somewhere inside its box but outside all of its proof lines. This has been done in Figure 32, and you can tell that it is selected because the box around subproof A is colored blue. After the subproof has been selected, you may choose "Conclude" from the Tools menu. The result is shown in Figure 33.
Notice that the conclusion has been put in a new proof line which is justified, and its justification reads "Proved by A".
By selecting a proof line and selecting "Derivation system" from the Tools menu, that line is sent to the EPGY Derivation System, where the user may make algebraic manipulations.
By selecting a term and choosing "Derive equation" from the Tools menu, the user may use the EPGY Derivation System to construct an equation involving that term.
By selecting "Font...", you will bring up a dialog box with which you can change the font for your proof. Any changes will affect the entire proof and become the default font for future proofs.
By checking (or un-checking) "Show subproof border", you cause the borders of the subproof boxes to be shown (or hidden).
When "Instantiate in place" is selected, universal instantiation will behave slightly differently than usual. With this option selected, instantiating a statement such as "FORALL x (x=x)" will not create a new proof step. It will, instead, simply replace the universal statement with the instantiated one. This option may help keep a proof from being cluttered with too many universal statements.
If "Hide Universal Quantifier" is selected, the program will not display any FORALL symbols. Instead, universally quantified formulas will be drawn with the quantified variables in red. For example, "FORALL x (x=x)" will be displayed as "x = x". Quantified variables can still be generalized or instantiated in the usual ways.
If "Toggle Wrap/Scroll of Math" is selected, the system will display long mathematical expressions with line-breaks. If a proof contains very long expressions, this option may make the proof more readable.
Universal generalization in the backwards direction is explained elsewhere. Use the right-click menu for universal generalization in the forwards direction. If "y" is an independent variable, you may use universal generalization to conclude "FORALL y (P(y))". To do this, right-click to highlight the variable "y" in a justified proof line. When you release the mouse button, you will see something like Figure 34. By choosing "Universally Generalize y", you will get something like Figure 35. Please note that the name of the variable you selected, "y", has appeared in the right-click menu.
Existential generalization in the backwards direction is explained elsewhere. Use the right-click menu for existential generalization in the forwards direction. You may existentially generalize from any term. For instance, from the statement "1 + 1 = 2", you may conclude "EXISTS x (x = 2)" by existentially generalizing the term "1 + 1".
To do this, right-click to highlight the term "1 + 1" in a justified proof line. When you release the mouse button, you will see something like Figure 36. After choosing "Existentially Generalize term", you be presented with the Input Panel and asked to choose a new variable. You may choose any variable that does not appear elsewhere in the statement. Figure 37 results from choosing the variable "x".
Please note that the right-click menu (in Figure 36) has no option available for universal generalization. This it because only independent variables can be universally generalized. For terms more complicated than simple variables (and for dependent variables), only existential generalization is possible.
Universal instantiation allows you, given the statement "FORALL y (P(y))", to conclude "P(t)" where t is any term. Existential instantiation allows you, given the statement "EXISTS y (P(y))", to conclude "P(x)" where x is a new variable. Either of these deductions may be carried out by choosing "Instantiate" from the right-click menu.
For an example of universal instantiation, start with the statement "FORALL x (x = x )". As in Figure 38, you may right-click to select x. After you select "Instantiate" from the menu, you will be asked to enter a term to replace the variable you selected. Whatever term you enter will replace all the occurrences of the variable. Figure 39 is the result of choosing "1 + 2" to replace x.
As an example of existential instantiation, start with the statement "EXISTS y (P(y))". As in Figure 40, you may right-click to select y. After you select "Instantiate" from the menu, you will be asked to choose a name for the constant you are instantiating. You must select new variable. Figure 41 is the result of choosing "a".
You may also instantiate quantified variables in more complicated expressions. However, you may only instantiate variables in an outermost quantifier. For example, in the statement
you may instantiate either x or y but not z.
You may rename any quantified variable in an expression. This is useful to avoid name-conflicts. For instance, to rename the quantified variable z, right-click and hold to highlight any instance of z. When you release the right mouse button, select "Rename z" from the pop-up menu, as in Figure 42. The Input Panel will appear and you will be asked for a new variable name. After you supply a new variable, a new proof line will be generated and marked "Proved By" (or "Provable from") your original line (in Figure 43, we see the result of choosing "a" as the new name).
Use the "Expand by Definition" tool from the right-click menu to invoke the definition of a relation (from the Theorem Database) or the definition of a function (from a step in the proof).
Definition expansion may be used in either the forwards or the backwards direction. If the insertion point in above the proof step, expansion will be backwards, so the proof step will be marked "Provable from..." the new step. If the insertion point is below the proof step, expansion will be forwards, so the new step will be marked "Provable from..." the original step.
To expand the definition of a relation from the Theorem Database, select the Definition, then right-click and drag to select the relation in the proof step. In Figure 44, we are working backwards and expanding the definition of the relation "S". ProofEd matches the "x" in the definition with the "a" in the proof step and the "y" in the definition with the "b" in the proof step and creates a new step, as in Figure 45. If there were any ambiguity in the matching, or if bound variables needed to be renamed, the user would be presented with the Input Panel and asked to resolve the conflicts.
Expanding the definition of a function is similar. As in Figure 46, to work backwards from f(y) in line 2, first select the definition of f (line 1), then right-click and drag to select the term "f(y)" in line 2. Since the insertion point is above line 2, we will work backwards. After selecting "Expand by Definition" from the pop-up menu, we get Figure 47. The main result is line 3, "sqrt(y) = sqrt(y)", which is the expansion of line 2. The proof obligation in line 4, "y > 1", is included because it is the domain condition for f.
You may substitute one term for another if they are related by an equality somewhere in your proof. This equality may be the entire statement of a proof line, or it may be the conclusion of a conditional statement. To use the substitution tool,
If you are substituting from a plain equality (as in Figure 48), a new proof line will be generated, marked as "Proved from" (or "Provable from") the equality you selected and the line into which you are substituting (as in Figure 49).
If you are substituting from a conditional equality (as in Figure 50), ProofEd will need to verify that the appropriate hypotheses holds. If ProofEd cannot verify the hypotheses, they will be added as extra proof steps (as in Figure 51) which need to be justified before your proof goal is marked as "Derived".
Select one term in an equation and choose "Derive an equation" from the right-click menu to send that term to the EPGY Derivation System. Once there, the user may make algebraic manipulations to derive a new equation involving that term.
By selecting "Copy" from the right-click menu, you copy the highlighted term to the clipboard. The term may then be pasted at any active editing prompt.
