Mark2 is an interactive equational theorem prover. The basic model for a session under this prover is that the user enters a term in the internal language of the prover, further restrained by declarations of constants and operations in the theory in which the user is working. This term can be thought of as the left side of an equation which the user is setting out to prove. The user will then modify this term using equational theorems already proved or given as axioms as rewrite rules until he converts the equation to the desired form. The user views a selected subterm of the current version of the right side of the equation; he may issue ``movement'' commands which change which subterm is selected, or he may apply theorems as rewrite rules to the selected subterm. All uses of equations as rewrite rules apply only to the selected subterm, not to its proper subterms. When the equation has assumed the form the user wants, it is ``proved'' as a theorem and becomes available for use as a rewrite rule.
There are some additional factors which complicate this basic model, but the broad outline has remained fixed through the development of the prover. One thing which should be clear is that this is not a model for an automated prover. It is also clear that this procedure would be very laborious without access to automation of reasoning steps.
The ability to automate reasoning steps is provided by a tactic language. A distinctive feature of the tactic language is that tactics or ``programs'' in this languages are represented as equations in the internal language, i.e., as theorems. The way in which this is achieved will be discussed below. This differs from the situation in provers in the tradition of Edinburgh LCF, in which theorems and tactics are objects at quite different levels written in different languages.
The logic immediately apparent to the user in this prover is simple equational or ``algebraic'' logic. There is a higher-order logic implicit in the definition and variable-binding procedures of the prover, which can be thought of as a polymorphic version of the simple type theory of Russell, in which no explicit type indices are ever needed. It is actually a version of Quine's New Foundations.
For precise syntax of commands mentioned in the text, look in the Command Reference section. Also look at the beginning of the Command Reference section for information on syntax restrictions imposed by ML (arguments must be quoted and unit arguments are needed for operations which don't have real arguments). The Command Reference represents an older layer of documentation than the rest of the test, so may not include descriptions of some commands referenced in the text. Later versions will be updated.
An old document with a tutorial and an even older command reference section of its own is appended; the earlier one is more reliable. Both have been updated to some extent in the course of the preparation of this document; they are organized along somewhat different lines.