An Interactive Mathematical Proof System
Copyright (c) 1990-2006 The MITRE Corporation
Contents
IMPS is an Interactive Mathematical Proof System 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. To get
a feel for the kinds of mathematics that it is possible to do in
IMPS, see the description of the IMPS Theory Library.
One of the chief tools of IMPS 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.
The IMPS system is available under the terms of a public license. IMPS 2.0,
which is written in Common Lisp, runs on Linux and Solaris platforms
with at least 16 MB of physical memory. IMPS 2.0 should work
with most versions of Common Lisp.
Currently we support Allegro CL, CLISP, CMU Common Lisp, GCL (Gnu Common Lisp). We
prefer CLISP, because it produces the smallest images, seems well
supported, and has good performance. IMPS runs much faster under
Allegro CL (versions 4.3, 5.0, and 6.0) and CMU Common Lisp 18a
for x86-linux, since both of these lisps have native code compilers.
However, the images created for these lisps are much larger.
IMPS 2.0 runs under the X Window System and has an
Emacs-based interface; we support only XEmacs versions 19 and 20,
although it may run under other versions of Emacs.
It is conceivable, though highly unlikely, that IMPS 2.0
might run under Windows implementations of Emacs and Common Lisp.
The IMPS system consists of three files:
- A README file. This file
explains how to set up an IMPS system.
- The IMPS
public license.
- The IMPS 2.0 tar
file. This file (about 1500K) contains the Common Lisp sources and
GNU Emacs sources of the IMPS system.
To subscribe to the IMPS Mailing List, send e-mail to
imps-request@imps.mcmaster.ca
with the following command in the body of your e-mail message:
subscribe
We strongly urge that all users of IMPS subscribe to the
IMPS Mailing List.
IMPS was designed and developed at The MITRE Corporation
under the MITRE-Sponsored Research program. Ronald D. Haggarty,
former Senior 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 F. J. Thayer by producing a
macro/emulation of the T programming language in Common Lisp. The
IMPS user interface is written in the GNU Emacs programming
language, developed by R. Stallman.
Originally designed by F. Javier Thayer (jt@mitre.org).
Maintained by William M. Farmer (wmfarmer@mcmaster.ca).