IMPS 2.0 Copyright (c) 1990-2004 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= 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= 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.