IMPS is an Interactive Mathematical Proof System developed at The MITRE Corporation by W. Farmer, J. Guttman, and J. Thayer. For a technical overview of the system, see [11].

The manual consists of three parts:

- (1)
*Introductory Material.*This part should definitely be read first. Chapter 3, ``A Brief Tutorial,'' provides a quick way to start using IMPS.- (2)
*User's Guide.*This part describes how to use IMPS, particularly, how to build theories.- (3)
*Reference Manual.*

IMPS aims at computational support for traditional techniques of mathematics. It is based on three observations about rigorous mathematics:

- Mathematics emphasizes the axiomatic method. Characteristics of mathematical structures are summarized in axioms. Theorems are derived for all structures satisfying the axioms. Frequently, a clever change of perspective shows that a structure is an instance of another theory, thus also bringing its theorems to bear.
- Many branches of mathematics emphasize functions, including partial functions. Moreover, the classes of objects studied may be nested, as are the integers and the reals; or overlapping, as are the bounded functions and the continuous functions.
- Proof proceeds by a blend of computation and formal inference.

Moreover, LUTINS allows subtypes to be included within types. Thus, for instance, the natural numbers form a subtype of the reals, and the continuous (real) functions a subtype of the functions from reals to reals. The subtyping mechanism facilitates machine deduction, because the subtype of an expression gives some immediate information about the expression's value, if it is defined at all. Moreover, many theorems have restrictions that can be stated in terms of the subtype of a value, and the theorem prover can be programmed to handle these assertions using special algorithms.

This subtyping mechanism interacts well with the type theory only because functions may be partial. If is a subtype of , while is a subtype of , then is a subtype of . In particular, it contains just those partial functions that are never defined for arguments outside , and which never yield values outside .

The mathematician devotes considerable effort to proving lemmas that justify computational procedures. Although these are frequently equations or conditional equations, they are sometimes more complicated quantified expressions, and sometimes they involve other relations, such as ordering relations. Once the lemmas are available, they are used repeatedly to transform expressions of interest. Algorithms justified by the lemmas may also be used; the algorithm for differentiating polynomials, for example. The mathematician has no interest in those parts of a formal derivation that ``implement'' these processes within predicate logic.

On the other hand, to understand the structure of a proof (or especially, a partial proof attempt), the mathematician wants to see the premises and conclusions of the informative formal inferences.

Thus, the right sort of proof is broader than the logician's notion of a formal derivation in, say, a Gentzen-style formal system. In addition to purely formal inferences, IMPS also allows inferences based on sound computations. They are treated as atomic inferences, even though a pure formalization might require hundreds of Gentzen-style formal inference steps. We believe that this more inclusive conception makes IMPS proofs more informative to its users.

The IMPS system consists of four components.

All the basic logical and deductive machinery of IMPS on which the
soundness of the system depends is included in the *core* of
IMPS. The core is the specification and inference engine of IMPS.
The other components of the system provide the means for harnessing
the power of the engine.

The organizing unit of the core is the IMPS *theory*.
Mathematically, a theory consists of a LUTINS language plus a set of
axioms. A theory is implemented, however, as a data structure to
which a variety of information is associated. Some of this
information procedurally encodes logical consequences of the theory
that are especially relevant to low-level reasoning within the theory.
For example, the great majority of questions about the definedness of
expressions are answered automatically by IMPS using tabulated
information about the domain and range of the functions in a theory.
Theories may be enriched by the definition of new sorts and constants
and by the installation of theorems.

Proofs in a theory are constructed interactively using a natural style
of inference based on sequent calculus. IMPS builds a data
structure which records all the actions and results of a proof
attempt. This object, called a *deduction graph*, allows the
user to survey the proof, and to choose the order in which he works on
different subgoals. Alternative approaches may be tried on the same
subgoal. Deduction graphs also are suitable for analysis by software.

The user is only allowed to modify a deduction through the application
of *primitive inferences*, which are akin to rules of inference.
Most primitive inferences formalize basic laws of predicate logic and
higher-order functions. Others implement computational steps in
proofs. For example, one class of primitive inferences performs
expression simplification, which uses the logical structure of the
expression [20], together with algebraic simplification,
deciding linear inequalities, and applying rewrite rules.

Another special class of primitive inferences ``compute with theorems''
by applying extremely simple procedures called macetes.
^{1.3}
An *elementary macete*, which is built by IMPS whenever a
theorem is installed in a theory, applies the theorem in a manner
determined by its syntax (e.g., as a conditional rewrite rule).
Compound macetes are constructed from elementary and other kinds of
atomic macetes (including macetes that beta-reduce and simplify
expressions). They apply a collection of theorems in an organized
way.

In addition to the machinery for building theories and reasoning
within them, the core contains machinery for relating one theory to
another via theory interpretations. A theory interpretation can be
used to ``transport'' a theorem from the theory it is proved in to any
number of other theories. Theory interpretations are also used in
IMPS to show relative consistency of theorems, to formalize symmetry
and duality arguments, and to prove universal facts about polymorphic
operators. The great majority of the theory interpretations needed by
the IMPS user are built by software without user assistance. For
example, when a theorem is applied outside of its home theory via a
*transportable macete*, IMPS automatically builds the required
theory interpretation if needed.

We have built an extension of the core machinery with the following goals in mind:

- To facilitate building and printing of expressions by providing various parsing and printing procedures.
- To make the inference mechanism more flexible and more autonomous.
In particular, the set of commands available to users includes an
extensible set of inference procedures called
*strategies*. Strategies affect the deduction graph only by using the primitive inference procedures of the core machinery, but are otherwise unrestricted. - To facilitate construction of theories and interpretations between them.

The user interface, which is a completely detachable component of IMPS, is mainly designed to provide users with facilities to easily direct and monitor proofs. Specifically, it controls three critical elements of an interactive system:

- The display of the state of the proof. This includes graphical displays of the deduction graph as a tree, TEX typesetting of the proof history, and proof scripts composed of the commands used to build the proof. The graphical display of the deduction graph permits the user to visually determine the set of unproven subgoals and to select a suitable continuation point for the proof. The TEX typesetting facilities allow the user to examine the proof in a mathematically more appealing notation than is possible by raw textual presentation alone. And, with proof scripts, the user can replay the proof, in whole or in part.
- The presentation of options for new proof steps. For any particular subgoal, the interface presents the user with a well-pruned list of commands and macetes to apply. This list is obtained by using syntactic and semantic information which is made available to the interface by the IMPS supporting machinery. For example, in situations where over 400 theorems are available to the user, there are rarely more than ten macetes presented to the user as options.
- The processing of user commands. The commands are then submitted to the inference software, while any additional arguments required to execute the command are requested from the user.

IMPS is equipped with a library of basic theories, which can be augmented as desired by the user. The theory of the reals, the central theory in the library specifies the real numbers as a complete ordered field. (The completeness principle is formalized as a second-order axiom, and the rationals and integers are specified as the usual substructures of the reals.) The library also contains various ``generic'' theories that contain no nonlogical axioms (except possibly the axioms of the theory of the reals). These theories are used for reasoning about objects such as sets, unary functions, and sequences.

IMPS was designed and implemented at The MITRE Corporation under the MITRE-Sponsored Research program. Ronald D. Haggarty, Vice President of Research and Technology, deserves special thanks for his strong, unwavering support of the IMPS project.

Several of the key ideas behind IMPS were originally developed by Dr. Leonard Monk on the Heuristics Research Project, also funded by MITRE-Sponsored Research, during 1984-1987. Some of these ideas are described in [20].

The IMPS core and support machinery are written in the T programming language [18,23], developed at Yale by N. Adams, R. Kelsey, D. Kranz, J. Philbin, and J. Rees. The IMPS user interface is written in the GNU Emacs programming language [25], developed by R. Stallman.

We are grateful to the Harvard Mathematics Department for providing an ftp site for IMPS.