So far we can write down terms, but neither we nor the prover knows anything about what they mean. We begin to remedy this.
We describe the fundamental structure of a prover session. The user enters a term using the ``start'' command. We call this the initial term. The user performs a series of manipulations of this term (sometimes of the initial term as well), guaranteed to preserve the truth of the equation between the initial term and the current term. The user finally issues a command, usually
which records the theorem <initial-term> = <current-term> under the name <name-of-theorem>. The manipulations allowed in the intermediate steps are most often applications of equational theorems, and the new theorem just proved will be added to the current ``theory'' (library of theorems) and will be usable in subsequent proofs.
Of course, not all theorems in the library can have been proven; some are introduced initially as axioms or as definitions. Definitions will be discussed below; we now show how to enter an axiom. Issue the following command.
axiom "COMM" "?x+?y" "?y+?x";
A display produced by the prover will follow. The prover now knows that the operator ``+'' is commutative.
The format for an axiom declaration should be clear from the above example; the ``axiom'' command has three parameters, the first being the name of the axiom, the second being the left side of the equation being asserted as an axiom, and the third being the right side of the equation.
Our assertion that the prover ``knows'' that addition is commutative requires some support. Try out the following sequence of commands.
start "?x+?y+?z"; ruleintro "COMM";
The current term now looks like this:
COMM => ?x + ?y + ?z
The infix => is a predeclared operator. The value of ?x=>?y is the same as that of ?y, with the annotation that one intends to apply the theorem ?x to the term ?y. Such terms are called ``embedded theorem applications''.
Now issue the command
which carries out all embedded theorem applications in the current subterm. You should now see the term
(?y + ?z) + ?x
which is the result of applying the commutative law of addition to the original term.
There is another opportunity to apply the commutative law here; this can be realized by the sequence of commands
left(); ruleintro "COMM"; execute();
which should leave you with the term
(?z + ?y) + ?x
You should now be able to see why the movement commands are provided. Next, use ``ruleintro'' to propose application of the commutative law to both the complete term and the subterm at the same time, then use the ``top'' command to return to the complete term, and only then issue the ``execute'' command. Both applications of the commutative law will be carried out at once, returning the term to its original shape. The form of the term before you issue the ``execute'' should be
COMM => (COMM => ?z + ?y) + ?x
As the last exercise illustrates, the commutative law of addition is completely symmetrical in its effect. We introduce another axiom, by the command
axiom "ASSOC" "(?x+?y)+?z" "?x+?y+?z";
with which we will explore further features of theorem application.
Issue the following sequence of commands:
start "?a+?b+?c"; ruleintro "ASSOC"; execute(); (* you can write more than one command on a line! *)
Did you expect something to happen? (It is useful to note that an embedded theorem which does not apply to its target is simply removed by the ``execute'' command).
The difficulty is that the theorem application represented by the infix => always represents the result of attempting to match the target term with the left side of the theorem; the command which works in this situation is
upon which we see
ASSOC <= ?a + ?b + ?c
An infix expression ?x<=?y has the value of ?y and signals the intention of applying the theorem ?x in reverse; that is, attempting to match the term ?y with the right side of the equation. Now, the ``execute'' command gives the desired result
(?a + ?b) + ?c
A useful exercise is to take the term (?a+?b)+?c+?d, or a similar complex term, and try applying the associative law to it in each direction. A useful command to know about is
which restores the initial term.
We now prove a theorem, the theorem ?x+?y+?z = ?z+?y+?x, which we will call ``REVERSE''. Enter this sequence of commands:
start "?x+?y+?z"; revruleintro "ASSOC"; execute(); ruleintro "COMM"; execute(); right(); ruleintro "COMM"; execute(); prove "REVERSE"; (* the new theorem should now be displayed *) startover(); ruleintro "REVERSE"; execute(); (* the new theorem can be applied like the old ones *)
to get another look at your theorem (this is a useful command to know anyway). Note especially the list of strings at the bottom of the display; this indicates the axioms on which ``REVERSE'' depends.
Another command of the same genre is
showalltheorems(); (* after typing this, hit enter repeatedly *)
Each time you hit enter, a theorem will be displayed; it will go through the entire list. Depending on the context you are working in, you may see some extra theorems you don't know anything about. You can use any key other than Enter to break out.
An exercise which one might attempt now is to introduce the axioms of commutativity and associativity for multiplication (represented by *) as well as the distributive law of multiplication over addition, and prove the usual FOIL rule (?x+?y)*(?z+?w) = (?x*?z)+(?x*?w)+(?y*?z)+(?y*?w). You might decide that you wanted to prove some additional theorems to make this easier (for example, if you stated the distributive law as ?x*(?y+?z) = (?x*?y)+(?x*?z), you might want to prove the other form, (?x+?y)*?z = (?x*?z)+(?y*?z), for use in the proof of the FOIL theorem.
A subtlety of theorem use can be illustrated if we introduce the axiom ``INV'': ?a+ -?a=0. Issue the commands
start "0"; revruleintro "INV"; (* after declaring the axiom! *) execute();
If you declared the axiom exactly as described above, you will get
?a_1 + -?a_1
The numerical suffixes (which may take a different value than 1) are added to make collisions with variables that you are already using unlikely. We can assign a specific value to the new variable ?a_1 by using the ``assign'' command:
assign "?a_1" "3";
whereupon we have
3 + -3
In this most common use of the ``assign'' command, it is expected that the variable to which the assignment is made is new; it is important to note that if an assignment is made to a variable which appears in the initial term (the term you introduced with ``start'' at the beginning of your session) that the variable will be replaced in the initial term as well as in the current term; this is obviously necessary if assignments to variables are to preserve an equation between the initial term and the current term.
We use the command ``lookback'' which allows us to look at the initial term without returning to it in the following example:
start "?x+?y"; ruleintro "COMM"; execute(); assign "?x" "?a+?b"; lookback(); (* the initial term will have changed! *) look(); (* the current term is unchanged by the lookback command *) startover(); (* note that this does not undo the assignment *)
With the ``ruleintro'', ``execute'', ``assign'', and ``prove'' commands, you have the basic tools needed to do laborious step by step proofs by hand in MARK2. If you prove interesting theorems, be sure to save your work (using the ``storeall'' command if you started from scratch, or the ``safesave'' command if you are working in an existing theory which you got with the ``load'' command, as described above).