An Interactive Mathematical Proof System


Copyright (c) 1990-2006 The MITRE Corporation

Authors: W. M. Farmer, J. D. Guttman, F. J. Thayer


Contents

Introduction

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.

How to Get IMPS

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:

  1. A README file. This file explains how to set up an IMPS system.
  2. The IMPS public license.
  3. The IMPS 2.0 tar file. This file (about 1500K) contains the Common Lisp sources and GNU Emacs sources of the IMPS system.

Mailing List

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.

Acknowledgments

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).