Jump To: Parent Description
Copyright (c) 1990-2005 The MITRE Corporation
Authors: W. M. Farmer, J. D. Guttman, F. J. Thayer
B. IMPS Web Site
C. How to Install IMPS
D. How to Start IMPS
E. How to Convert from IMPS 1.2 to IMPS 2.0
F. Questions, Comments, and Bug Reports
IMPS is an Interactive Mathematical Proof system developed at The
The IMPS system is available without fee on the
Web under the terms of a Public license (see section B below).
2.0, which is written in Common Lisp, runs on Unix platforms with at
least 16 or more MB physical memory.
IMPS 2.0 should work with most
versions of Common Lisp; we support Allegro CL, CLISP, and CMU Common
We prefer CLISP: it produces small executables, is
well-supported, and is available at
(Use CLISP 2.29 instead of CLISP 2.33.)
successfully run IMPS 2.0 with these versions of Common Lisp on SunOS,
Sun Solaris, and Linux.
IMPS 2.0 runs under the X Window system and
has an emacs-based interface; we support primarily the XEmacs version
The older IMPS 1.2, which is written in the T programming language,
runs only on Sun 4 SPARCstations.
IMPS 1.2 is no longer being
developed or supported and should be considered as obsolete.
IMPS 1.2 who want to convert to IMPS 2.0, should read Section E below.
IMPS is intended to provide organizational and computational support
for the traditional techniques of mathematical reasoning.
particular, the logic of IMPS allows functions to be partial and terms
to be undefined.
The system consists of a database of mathematics
(represented as a network of axiomatic theories linked by theory
interpretations) and a collection of tools for exploring, applying,
extending, and communicating the mathematics in the database.
the chief tools is a facility for developing formal proofs.
contrast to the formal proofs described in logic textbooks, IMPS
proofs are a blend of computation and high-level inference.
Consequently, they resemble intelligible informal proofs, but unlike
informal proofs, all details of an IMPS proof are machine checked.
B. IMPS Web Site
The welcome page for IMPS Web site is at
It includes links to:
1. The IMPS system (README, Public license, and tar files).
2. The IMPS User's Manual in HTML, PostScript, and PDF formats.
is approximately 300 pages long.
Some parts of it refer to IMPS
1.2 and are thus out of date for IMPS 2.0.
3. Technical papers on IMPS in PostScript and PDF formats.
4. The IMPS Mailing List.
5. A hypertext presentation of the IMPS Theory Library.
presentation allows one to explore this body of mathematics by
going, for example, from the name of a constant used in a proof
to the constant's definition or from the proof of a theorem to
the specification of the theory in which the theorem was proved.
C. How to Install IMPS
1. Choose a directory somewhere in your file system where you would
like to put the IMPS system.
You will need about 30 MB of space.
(More space may be needed for certain versions of Common Lisp.)
us refer to this directory as /.../dir.
Execute (the shell command)
2. Move the file "imps-2.0.tar.gz" to the /.../dir directory.
execute the following commands:
tar -xvf imps-2.0.tar
Each of these operations will take about a minute.
After they are
done, you may delete the file imps-2.0.tar or recompress it and put it
wherever you want.
3. Choose what version of emacs and Common Lisp you would like to use.
We recommend XEmacs and Allegro CL, CLISP, or CMU Common Lisp.
versions of emacs and Common Lisp will work, but you may have to make
a few modifications to the IMPS system.
4. Edit the file "install" which is found in /.../dir/imps.
the top of the file are the four lines:
If you leave the file as is, IMPS will be installed with your system
emacs, CLISP, and gawk.
(Make sure these three programs are available
on your system.)
If you would like to use another version of emacs (e.g., if XEmacs is
not your system emacs), change the first line to
emacs-pathname>Warning: XEmacs is the only version of emacs that we are fully supporting. If you would like to use Allegro CL 4, Allegro CL 5, or CMU Common Lisp instead of CLISP, change the second and third lines, respectively, to CL= or CL= or CL= LISP=cmuThe install script assumes that you have gawk installed on your system. If you would like to use nawk instead of gawk, change the fourth line to GAWK= 5. Finally, execute (the shell command) /.../dir/imps/install This will cause the compilation of all the IMPS source files and will produce an executable. (You may ignore the many warning messages that are printed.) Depending on the version of Common Lisp you use, this may take from a few minutes for CLISP to about 30 minutes for CMU Common Lisp. D. How to Start IMPS To run IMPS, start X Windows and then execute /.../dir/imps/bin/start_imps & This will start up IMPS running in an XEmacs window. The default XEmacs settings for color, fonts, etc. may be changed by editing the file /.../dir/imps/el/imps-emacs.el E. How to Convert from IMPS 1.2 to IMPS 2.0 The IMPS Main Theory Library is exactly the same for both IMPS 1.2 and IMPS 2.0, so converting from IMPS 1.2 to IMPS 2.0 should not be very difficult. Since different versions of Common Lisp use different hash functions, some proof scripts produced with IMPS 1.2 will break when they are executed with certain versions of Common Lisp. However, these broken proof scripts are usually very easy to repair. All the proof scripts in the IMPS Main Theory Library work correctly when IMPS is run with CLISP. F. Questions, Comments, and Bug Reports Questions and comments about IMPS can be mailed to email@example.com Please mail information about bugs or problems with using IMPS to firstname.lastname@example.org G. Acknowledgments IMPS was designed and developed at The MITRE Corporation under the MITRE-Sponsored Research program. Ronald D. Haggarty, former MITRE 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. We would like to thank the Harvard Mathematics Department, and professor David Mumford (now at Brown) in particular, for providing the original FTP site for IMPS. The core and support machinery of IMPS 1.2 was written in the T programming language, developed at Yale by N. Adams, R. Kelsey, D. Kranz, J. Philbin, and J. Rees. IMPS 2.0 was created by J. Thayer by producing a macro-emulation of the T programming language in Common Lisp which can execute a suitably translated version of the original IMPS source code. The IMPS user interface is written in the GNU emacs programming language, developed by R. Stallman.