In this tutorial, we will assume that you have the X Window System running on your workstation. If your workstation can run X but it is not installed, enlist the aid of a system guru to get him or her to set things up for you. Although it is possible to run IMPS from a dumb terminal (for example, to work from home, where mere mortals only have terminal emulators), you will miss the functionality that X provides, such as fancy TEX previewing of formulas and proofs, and interaction with IMPS using the mouse and the menu facility. We will also assume that you have the shell variable IMPS correctly set.
To start IMPS enter this command at the shell prompt:
$IMPS/../bin/start_imps
Executing this command will do the following:
$HOME/imps and $HOME/imps/theoriesneeded for the IMPS exercises.
If you are trying to learn to use IMPS, it would be a good idea to work through the exercises described in Chapters and 5, after reading this tutorial.
Most of your interaction with IMPS can be initiated by selecting of one of a number of menu options. The menu format depends on the version of Emacs you are using.
You select an option within a menu or pane by pointing with the mouse (notice the selected option is enclosed in a box) and clicking the right mouse button. If you do not want to select anything after the menu appears, click right on the option CANCEL MENU REQUEST (or just click right when the mouse points to somewhere off the menu.) This will cause the menu to disappear.
Notice that some of the options are followed by a sequence of keystrokes enclosed in parentheses. This means that these options can also be invoked directly using these keystrokes. As you become more familiar with IMPS, you will probably want to use these more direct invocations. Note that you can use the menus to change buffers or modify the number of windows on the screen.
You should also be aware that the panes which appear on the menu, and the options within each pane, usually depend on the window you clicked on to bring up the menu.
The following documentation is available online:
For now, you can think of a theory as a mathematical object consisting of a language and a set of closed formulas in that language called axioms. For example, one of the last things that was printed out in the startup procedure was the line
Current theory: #{impstheory 3: HOREALARITHMETIC}horealarithmetic is a basic IMPS theory which contains an axiomatic theory of the real numbers, characterized as a complete ordered field with the integers and rationals as imbedded structures. This is a fairly extensive theory, so we only describe it informally here. The atomic sorts of the language are N, Z, Q, R denoting the natural numbers, integers, rationals, and reals. The language constants of this theory are of three kinds:

The axioms of this theory are the usual field and order axioms as well as the completeness axiom which states that any predicate which is nonvacuous and bounded above has a least upper bound. This theory also contains the full secondorder induction principle for the integers as an axiom.
At any given time there is a theory that IMPS regards as the current theory. For example, as we mentioned above, the current theory is horealarithmetic when IMPS finishes loading. The current theory affects the behavior of IMPS in two very significant ways:
We now describe the string syntax for IMPS. First, some preliminary considerations. A language in IMPS has two kinds of objects: sorts and expressions. Sorts are intended to denote classes of elements; they are used to help specify the value of an expression and to restrict quantification. They are especially useful for reasoning with respect to overlapping domains. For example, suppose zz and rr are sorts denoting the integers and the real numbers, respectively. Then the Archimedean principle for the real numbers can be expressed quite naturally as
forall(a:rr,forsome(n:zz,a<n)).
Sorts are of two kinds: atomic sorts and compound sorts. An atomic sort is just a name. A compound sort is a list [s0,...,sn] where each si is itself a compound sort or an atomic sort. Compound sorts are intended to denote the set of all nary partial functions from the ``domain'' sorts into the ``range'' sort sn (an exception to this rule about intended meanings of sorts is discussed in the Chapter 7). A language distinguishes certain sorts as types and assigns a type to every sort. Distinct types are intended to denote sets of elements which need not be related. prop is a ``base'' type which belongs to every language and which is intended to denote the set of truth values. The sorts for horealarithmetic are given in Table 3.2.
The expressions of a language are built from language constants and
variables as specified by Table 3.3 below. A constant
is a character string specified as such by the deflanguage
form. A variable is also character string. Variables however, must
begin with a text character (that is, an alphabetic character or one
of the symbols _ % $ &
) and contain only text characters or digits.
Moreover, the sorting of a variable within an expression must be
specified either by an enclosing binder or by an enclosing ``with''
declaration.

In the theory horealarithmetic there is additional syntax
for arithmetic operators, described in Table 3.4. For
example,  is used for both sign negation and the binary
subtraction operator. The binary operators are all infix with
different binding powers to reduce parentheses on input and output: In
order of increasing binding power, the arithmetic operators are
+ * / ^ 
.

To check the syntax of an expression (enclosed in double quotes), select the entry Check expression syntax in the pane IMPS help. IMPS will request an expression, which you can supply by clicking the right mouse button on the formula. You can also type the formula directly in the minibuffer. As an exercise, build the formula which asserts that for every nonnegative integer n the sum of squares of the first n integers is n (n+1) (2 n+1)/6.
A formula in a theory is valid if it is true in every ``legitimate'' model of the theory; if the formula has free variables, we have to add: ``with every legitimate assignment of values to its free variables.'' To prove a formula means to offer conclusive mathematical evidence of its validity. The rules for admissible evidence are given by something called a proof system. In this section we will describe the IMPS proof system.
To begin an interactive proof in IMPS, select the start dg option in the Deduction Graphs pane of the menu. For version 19, click on the menubar on DG and then select Start dg. IMPS will then prompt you in the minibuffer with the text
Formula or reference number:This is an IMPS request for some formula to prove. You can supply this formula by typing its reference number in the minibuffer. Alternatively, you can click the right mouse button on the formula (provided that it is enclosed between double quotes), and then press <RET>. You are then ready to begin proving the formula.
After telling Emacs to start the deduction, two new buffers will be created. One buffer, labelled starDeductiongraph1* displays a graphical representation of a data structure called a deduction graph. The other Emacs buffer labeled starSequentnodes1* displays a textual representation of a data structure called a sequent node. Notice that the modeline for the sequent node buffer also contains the text
horealarithmetic: Sqn 1 of 1.This gives you the following information:
To understand the significance of the new buffer, note that a deduction graph provides a snapshot of the current status of the proof. A deduction graph is a directed graph with nodes of two kinds, called sequent nodes and inference nodes. An interactive proof in IMPS is carried out by adding inference nodes and sequent nodes to the deduction graph.
A sequent node consists of the following:
Inference nodes are to be understood in part by their relationship to
sequent nodes: Every inference node i has a unique conclusion node
c and a (possibly empty) set of hypothesis nodes
An inference node represents the following mathematical
relationship between c and
:
if every one of the
sequent nodes
is valid, then the sequent node c is
valid. Alternatively, we can view this as asserting that the validity
of the sequent node c can be reduced to the validity of
Note that if the inference node i has no hypotheses, then c is obviously valid. When this is the case, c is said to be immediately grounded. More generally, c is valid if all the hypotheses of i are valid. Thus validity propagates from hypotheses to conclusion. A sequent node which is recognized as valid in this way is said to be grounded. The system indicates that it has recognized validity of a sequent node when it marks it as grounded. A proof is complete when the original sequent node of the deduction graph (i.e., the deduction graph's goal node) is marked as grounded.
Sequent nodes and inference nodes are added to a deduction graph using deduction graph commands. Some commands correspond to the use of one inference rule; for example extensionality or forcesubstitution fall into this category. Applying such a command either does nothing or adds exactly one inference node to the deduction graph. Moreover, this one inference node corresponds quite closely to the application of one mathematical fact. Other commands such as simplify have similar behavior in that they either do nothing or add exactly one inference node. Yet they are fundamentally different because behind the scene they are often carrying out thousands of very lowlevel inferences, such as logical and algebraic simplification and rewriterule application. Finally a third class of commands are essentially strategies developed to systematically apply primitive commands in search of a proof.
IMPS can be extended in the following ways:
(defconstant CONVERGENT%TO%INFINITY "lambda(s:[zz,rr], forall(m:rr, forsome(x:zz, forall(j:zz, x<=j implies m<=s(j)))))" (theory horealarithmetic))As an exercise, try defining the concept of limit of realvalued sequences. Next, we illustrate how new theories are built by building a theory of monoids. Building a theory is a twostep process. First, we build a language with the required sorts and constants:
(deflanguage MONOIDLANGUAGE (embeddedlanguages horealarithmetic) (basetypes uu) (constants (e "uu") (** "[uu,uu,uu]")))The next step builds the theory itself by listing the axioms:
(deftheory MONOIDTHEORY (componenttheories horealarithmetic) (language monoidlanguage) (axioms (associativelawformultiplicationformonoids "forall(z,y,x:uu, x**(y**z)=(x**y)**z)" rewrite) (rightmultiplicativeidentityformonoids "forall(x:uu,x**e=x)" rewrite) (leftmultiplicativeidentityformonoids "forall(x:uu,e**x=x)" rewrite) ("total_q(**,[uu,uu,uu])" drconvergence)))
There are numerous other ways IMPS can be extended. These are discussed in detail in Chapter 17. In addition, there are a number of annotated files which show you how theories are built and theorems proved in them. These are described in the chapters of this manual ( and 5) on the micro exercises and the exercises.
The IMPS methodology for formalizing mathematics is based on a particular version of the axiomatic method. The axiomatic method is commonly used both for encoding existing mathematics and for creating new mathematics. A chunk of mathematics is represented as an axiomatic theory consisting of a formal language plus a set of sentences in the language called axioms. The axioms specify the mathematical objects to be studied, and facts about the objects are obtained by reasoning logically from the axioms, that is, by proving theorems.
The axiomatic method comes in two styles, both well established in modern mathematical practice. We refer to them as the ``big theory'' version and the ``little theories'' version. In the ``big theory'' version all reasoning is performed within a single powerful and highly expressive axiomatic theory, such as ZermeloFraenkel set theory. The basic idea is that the theory we work in is expressive enough so that any model of it contains all the objects that will be of interest to us, and powerful enough so that theorems about these objects can be proved entirely within this single theory.
In the little theories version, a number of theories are used in the course of developing a portion of mathematics. Different theorems are proved in different theories, depending on the amount and kind of mathematics that is required. Theories are logically linked together by translations called theory interpretations which serve as conduits to pass results from one theory to another. We argue in [10] that this way of organizing mathematics across a network of linked theories is advantageous for managing complex mathematics by means of abstraction and reuse.
IMPS supports both the big theory and little theories versions of the axiomatic method. However, the IMPS little theories machinery of multiple theories and theory interpretations offers the user a rich collection of formalization techniques (described in Chapter 9) that are not easy to imitate in a strict big theory approach.