imps-2.0
-
IMPS 2.0
Copyright (c) 1990-2005 The MITRE Corporation
Authors: W. M. Farmer, J. D. Guttman, F. J. Thayer
Contents:
A. Introduction
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
G. Acknowledgments
A. Introduction
IMPS is an Interactive Mathematical Proof system developed at The
MITRE Corporation.
The IMPS system is available without fee on the
Web under the terms of a Public license (see section B below).
IMPS
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
Lisp.
We prefer CLISP: it produces small executables, is
well-supported, and is available at
http://clisp.sourceforge.net/
without fee.
(Use CLISP 2.29 instead of CLISP 2.33.)
We have
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
of emacs.
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.
Users of
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.
In
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.
One of
the chief tools is a facility for developing formal proofs.
In
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
http://imps.mcmaster.ca
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.
It
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.
The
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.)
Let
us refer to this directory as /.../dir.
Execute (the shell command)
cd /.../dir
2. Move the file "imps-2.0.tar.gz" to the /.../dir directory.
Then
execute the following commands:
gunzip imps-2.0.tar.gz
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.
Other
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.
Towards
the top of the file are the four lines:
EMACS=`which emacs`
CL=`which clisp`
LISP=clisp
GAWK=`which gawk`
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=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=cmu
The 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
imps-questions@imps.mcmaster.ca
Please mail information about bugs or problems with using IMPS to
imps-bugs@imps.mcmaster.ca
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.