The MARK2 theorem prover is an upgrade of the theorem prover EFTTP, an equational prover implementing first-order logic, to allow the implementation of higher order logic.
The prover is equational: all theorems are equations, and the rules of inference supported directly are exactly the basic rules of equational reasoning that we all learn (implicitly at least) in algebra.
The prover incorporates a programming language. This was originally developed to allow the easy implementation of ``tactics'', procedures for the automatic implementation of many steps of reasoning without user intervention. Tactics or programs look to the system like equational theorems, and are stored in theories along with theorems of the normal sort; we think that the way in which this is achieved has some interest. The fact that the language has its own tactic-writing facility makes it much less dependent on the languages in which it is written (two dialects of ML) than was originally expected. We are currently working on a C++ implementation, which will allow more precise control over details of memory allocation and other aspects of execution.
The prover is interactive. The user enters a term and manipulates it, possibly with the help of automatic tactics, until he or she obtains the desired final form of the term. The user can then prove a theorem equating the initial and final forms of the term, which acquires the same status as the axioms and previously proved theorems of the system. Tactics are developed in the same way. Facilities are also provided for ``debugging'' tactics (programs).
The last couple of paragraphs of this introduction are technical and can safely be skipped.
The semantics of the prover are based on a system of relative typing (``stratification'') analogous to that which underlies Quine's set theory ``New Foundations''. It is closely related to a streamlined version of the type system of the typed -calculus widely used in computer science, and can often be regarded as implementing this streamlined system of types with polymorphism. The type system is completely invisible to an unsophisticated user!
The types in this ``streamlined'' type system are labelled by non-negative integers n, with each type n+1 = (functions from type n to type n) and each type n identified with type (pairs of objects of type n).
The consistency difficulties of ``New Foundations'' do not apply here; this system is related to the version NFU of Quine's system which is known to be consistent. For a technical discussion of the theory of stratified -calculus, see our preprint ``Untyped -calculus with relative typing''.