IMPS Version 1.1 Copyright (c) 1990-1994 The MITRE Corporation Authors: W. M. Farmer, J. D. Guttman, F. J. Thayer Contents: A. Introduction B. IMPS Mailing List C. How to Get IMPS D. How to Install IMPS E. Instructions for IMPS Users F. How to Start IMPS G. The IMPS Manual H. IMPS Papers I. Bug Reports and Questions J. Acknowledgments A. Introduction IMPS is an Interactive Mathematical Proof System developed at The MITRE Corporation. The IMPS system is available via ftp under the terms of a public license (see section C below). IMPS runs under the X Window System or OpenWindows on Sun 4 SPARCstations that have at least 24 MB physical memory (preferably more) and at least a 60 MB swap partition. 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 Mailing List To subscribe to the IMPS mailing list, send your name and e-mail address to imps-request@linus.mitre.org We strongly urge that all users of IMPS subscribe to the IMPS mailing list. C. How to Get IMPS Ftp to math.harvard.edu, login as "anonymous", and give your e-mail address as the password. Then type cd imps The directory you will be in contains a directory named doc and four files: 1. this file (README), 2. the IMPS system (imps.tar.gz), 3. the IMPS manual (imps-manual.dvi.gz), and 4. the IMPS public license (public-license). The IMPS manual and public license are also included in the IMPS system. To get a copy of the IMPS system, type binary get README get imps.tar.gz The transfer will take a few minutes. D. How to Install IMPS 1. Create a directory called imps (or whatever you prefer) somewhere in your file system where you have 35-40 MB free. (About 20 MB of this space is for IMPS; the rest is needed only during installation.) Let us refer to this directory as /.../imps. Execute (the shell command) cd /.../imps 2. Copy the file imps.tar.gz to the /.../imps directory. Then execute the following commands gunzip imps.tar.gz tar -xvf imps.tar Each of these operations will take several minutes. After they are done, you may delete the file imps.tar or recompress it and put it somewhere else. 3. Choose the version of Emacs you want to use with IMPS. The preferred version is Free Software Foundation GNU Emacs 19, but we also support GNU Emacs 18 and Lucid GNU Emacs 19. If you will be using Free Software Foundation GNU Emacs 19 or Lucid GNU Emacs 19, put the line (setq tea-use-comint t) in your .emacs file. Let us refer to the location of the Emacs executable as /.../emacs. Warning: Depending on the version of Emacs you choose, you may have to recompile the .el files in the directory /.../imps/el 4. Execute cd /.../imps/src and edit the file start_imps.sh to change the two lines IMPS=/tea IMPS_EMACS= to IMPS=/.../imps/tea IMPS_EMACS=/.../emacs Finally, execute make (You may ignore the error messages that are printed.) E. Instructions for IMPS Users In your .cshrc (or wherever you define your shell search path) add /.../imps/bin to your path. You may find it convenient to set the shell variable IMPS in your .cshrc using the command setenv IMPS /.../imps/tea If you want a form of Emacs different than /.../emacs, the official IMPS Emacs, set the shell variable EMACS_COMMAND in your .cshrc to the form of Emacs you want; for example, setenv EMACS_COMMAND 'emacs18 -w 94x56+250+20' If you will be using Free Software Foundation GNU Emacs 19 or Lucid GNU Emacs 19, put the line (setq tea-use-comint t) in your .emacs file. If IMPS is being run with Free Software Foundation GNU Emacs 19, the frame parameters (position, background and foreground colors, etc.) of the various IMPS windows are specified in the file /.../imps/el/frame-specs.el You will probably want to modify these specifications to suit your own taste. To do this, first copy the file frame-specs.el to /.../home/imps/imps-emacs.el (where /.../home is your home directory and imps is a subdirectory of your home directory that is created when you first run IMPS). Then change the frame specifications in this file as you like. To subscribe to the IMPS mailing list, send your name and e-mail address to imps-request@linus.mitre.org F. How to Start IMPS To run IMPS, start X or OpenWindows, and then execute start_imps & G. The IMPS User's Manual The IMPS user's manual is written in LaTeX and is available on-line. The .dvi file of the manual is located in the directory /.../imps/doc/manual (Also, both .dvi and .ps files of the manual are located in the imps directory at math.harvard.edu.) The manual is approximately 300 pages long. H. IMPS Papers In the imps/doc directory at math.harvard.edu, there are several papers on IMPS in compressed LaTeX dvi and ps formats. I. Bug Reports and Questions Please mail information about bugs or problems with using IMPS to imps-bugs@linus.mitre.org Other questions can be mailed to imps-request@linus.mitre.org J. Acknowledgments IMPS was designed and developed at The MITRE Corporation under the MITRE-Sponsored Research program. Ronald D. Haggarty, 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 are grateful to the Harvard Mathematics Department for providing an ftp site for IMPS. The IMPS core and support machinery are written in the T programming language, developed at Yale by N. Adams, R. Kelsey, D. Kranz, J. Philbin, and J. Rees. The IMPS user interface is written in the GNU Emacs programming language, developed by R. Stallman.