@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Name: IMPS Keywords: interactive theorem proving, computer proofs in analysis, little theories, computing with theorems, theory interpretations, higher-order logic, partial functions Description: Semantics: The logic of IMPS (called LUTINS) is a nonconstructive version of simple type theory with partial functions and subtypes. Since partial functions are dealt with directly, terms may be nondenoting. However, the logic is bivalent: formulas are either true or false. Deductive machinery: Proofs in IMPS, are represented by a data structure called a deduction graph which is a directed graph with two kinds of nodes: inference nodes and sequent nodes. As an interactive process, a proof consists of a series of reductions of unproven sequent nodes of the graph (which we think of as goals) to new subgoals. These reductions are obtained by applying proof commands to the deduction graph. Dynamics: IMPS objects (e.g., theories, definitions, theorems, interpretations, etc.) are created by evaluating special expressions called def-forms. A body of mathematical knowledge is created in IMPS by progressively evaluating def-forms. Proofs can be developed interactively using the proof support facility of the interface (which is largely menu-driven) or can be developed by building and running proof scripts. Persistence: The def-forms used to create a body of mathematical knowledge are stored in a collection of files which can be loaded in a running IMPS process as needed. Proofs and proof attempts are stored as proof scripts which can be rerun in whole or in part. Contact persons: William M. Farmer, Joshua D. Guttman, F. Javier Thayer E-mail: {farmer,guttman,jt}@mitre.org Address: The MITRE Corporation 202 Burlington Road Bedford, MA 01730-1420 USA Phone: 617-271-2907/2000 User group: To subscribe to the IMPS mailing list, send your name and e-mail address to imps-request@linus.mitre.org. Pragmatics: IMPS is intended to provide mechanical support for traditional mathematical techniques and styles of practice. It is based on three characteristics of mathematics practice: o Emphasis on the axiomatic method. Properties of mathematical structures are summarized in axioms. Theorems are derived for all structures satisfying the axioms. o Emphasis on functions, including partial and higher-order functions. o Use of a blend of computation and formal inference in proof. IMPS emphasizes the "little theories" version of the axiomatic method, as opposed to the "big theory" version. In the big theory approach, all reasoning is carried out within one theory---usually some highly expressive theory, such as the Zermelo-Fraenkel set theory. In the little theories approach, reasoning is distributed over a network of theories. Results are typically proved in compact, abstract theories, and then transported as needed to more concrete theories, or indeed to other equally abstract theories. Theory interpretations provide the mechanism for transporting theorems. The little theories style of the axiomatic method is employed extensively in mathematical practice. The IMPS user has a very substantial database of formalized mathematics to draw on. Documentation: The IMPS user's manual, a full IMPS bibliography, and several other papers on IMPS are available by anonymous ftp at math.harvard.edu (see below). A collection of on-line exercises for learning to use IMPS comes with the system. There is a World Wide Web home page for IMPS at file://math.harvard.edu/imps/imps_html/imps.html It includes a link to a hypertext presentation of the IMPS Main 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. The following are the published papers on IMPS in BiBTeX format: @Article{Farmer90, author = "W. M. Farmer", title = "A Partial Functions Version of {Church's} Simple Theory of Types", journal = "Journal of Symbolic Logic", year = "1990", volume = "55", Optnumber = "3", pages = "1269-91", OPTmonth = "", OPTnote = "Also {\sc mitre} Corporation technical report M88-52, 1988; revised 1990." } @Article{Farmer93b, author = "W. M. Farmer", title = "A Simple Type Theory with Partial Functions and Subtypes", journal = "Annals of Pure and Applied Logic", year = "1993", volume = "64", OPTnumber = "3", pages = "211--240", OPTmonth = "", OPTnote = "" } @InProceedings{Farmer94, author = "W. M. Farmer", title = "Theory Interpretation in Simple Type Theory", booktitle = "Higher-Order Algebra, Logic, and Term Rewriting", year = "1994", series = "Lecture Notes in Computer Science", volume = "816", editor = "J. Heering et al.", pages = "96--123", publisher = "Springer-Verlag", OPTnote = "" } @Article{Farmer95, author = "W. M. Farmer", title = "Reasoning about Partial Functions with the Aid of a Computer", OPTcrossref = "", OPTkey = "", journal = "Erkenntnis", OPTyear = "", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "Forthcoming.", OPTannote = "" } @InProceedings{FarmerEtAl90, author = "W. M. Farmer and J. D. Guttman and F. J. Thayer", title = "{\sc imps}: An {I}nteractive {M}athematical {P}roof {S}ystem (system abstract)", booktitle = "10th International Conference on Automated Deduction", year = "1990", series = "Lecture Notes in Computer Science", volume = "449", editor = "M. E. Stickel", pages = "653--654", OPTorganization = "", publisher = "Springer-Verlag", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{FarmerEtAl92a, author = "W. M. Farmer and J. D. Guttman and F. J. Thayer", title = "{\sc imps}: System Description", booktitle = "Automated Deduction---CADE-11", year = "1992", series = "Lecture Notes in Computer Science", volume = "607", editor = "D. Kapur", pages = "701--705", OPTorganization = "", publisher = "Springer-Verlag", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{FarmerEtAl92b, author = "W. M. Farmer and J. D. Guttman and F. J. Thayer", title = "Little Theories", booktitle = "Automated Deduction---CADE-11", year = "1992", series = "Lecture Notes in Computer Science", volume = "607", editor = "D. Kapur", pages = "567--581", OPTorganization = "", publisher = "Springer-Verlag", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{FarmerEtAl93, author = "W. M. Farmer and J. D. Guttman and F. J. Thayer", title = "{\sc imps}: An {I}nteractive {M}athematical {P}roof {S}ystem", journal = "Journal of Automated Reasoning", year = "1993", volume = "11", OPTnumber = "2", pages = "213--248", OPTmonth = "October" } @InProceedings{FarmerEtAl93a, author = "W. M. Farmer and J. D. Guttman and F. J. Thayer", title = "Reasoning with Contexts", booktitle = "Design and Implementation of Symbolic Computation Systems", year = "1993", series = "Lecture Notes in Computer Science", volume = "722", editor = "A. Miola", pages = "216--228", OPTorganization = "", publisher = "Springer-Verlag", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{FarmerEtAl94, author = "W. M. Farmer and J. D. Guttman and M. E. Nadel and F. J. Thayer", title = "Proof Script Pragmatics in {\sc imps}", booktitle = "Automated Deduction---CADE-12", year = "1994", series = "Lecture Notes in Computer Science", volume = "814", editor = "A. Bundy", pages = "356--370", OPTorganization = "", publisher = "Springer-Verlag", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{FarmerEtAl95, author = "W. M. Farmer and J. D. Guttman and F. J. Thayer", title = "Contexts in Mathematical Reasoning and Computation", OPTcrossref = "", OPTkey = "", journal = "Journal of Symbolic Computation", year = "1995", volume = "19", OPTnumber = "", pages = "201--216", OPTmonth = "", OPTnote = "", OPTannote = "", patron = "Farmer" } @Article{FarmerThayer91, author = "W. M. Farmer and F. J. Thayer", title = "Two Computer-Supported Proofs in Metric Space Topology", journal = "Notices of the American Mathematical Society", year = "1991", volume = "38", OPTnumber = "9", pages = "1133--1138", OPTmonth = "", OPTnote = "" } @InProceedings{Guttman92, author = "J. D. Guttman", title = "Building Verification Environments from Components: A Position Paper", booktitle = "Proceedings, Workshop on Effective Use of Automated Reasoning Technology in System Development", year = "1992", OPTeditor = "", pages = "4--17", OPTorganization = "", OPTpublisher = "", address = "Naval Research Laboratory, Washington, D.C.", month = "April", OPTnote = "" } @InCollection{GuttmanJohnson94, author = "Joshua D. Guttman and Dale M. Johnson", title = "Three Applications of {Formal} {Methods} at {MITRE}", booktitle = "FME '94: Industrial Benefits of Formal Methods", publisher = "Springer Verlag", year = 1994, editor = "M. Naftalin and T. Denvir and Miguel Bertran", volume = 873, series = "Lecture Notes in Computer Science", pages = "55--65", patron = "Guttman" } @Article{Monk88, author = "L. G. Monk", title = "Inference Rules Using Local Contexts", journal = "Journal of Automated Reasoning", year = "1988", volume = "4", OPTnumber = "4", pages = "445--462", OPTmonth = "", OPTnote = "" } Applications: Mathematics: 1. Banach's contractive-mapping fixed-point theorem and applications. The applications include an open mapping theorem for mappings on a Banach space which are near the identity. 2. Development of calculus for normed space valued functions. This includes the mean value theorem for derivatives and integrals, the fundamental theorem of calculus, and other basic properties of the derivative and integral. 3. A theory of finite cardinality. 4. A version of the traditional proof of the Schroeder-Bernstein theorem. 5. A theory of partial orders. Significant results proved here include the Knaster fixed-point theorem and applications. One application is a conceptually simple proof of the Schroeder-Bernstein theorem. 6. Basic facts about divisibility and primes, including the infinitude of primes, the fundamental theorem of arithmetic, and the principle ideal theorem for the integers. 7. The Fundamental Counting Theorem of group theory, of which Lagrange's theorem is an immediate corollary. 8. A development of a portion of elementary geometry based on the betweenness relation, including a proof of Sylvester's theorem. Computer science: 1. Theories formalizing various notions about state machines. 2. Correctness theorems about certain aspects of memory management in the Mach operating system microkernel. 3. A mathematical model of computer processes suited to timed CSP. 4. A software system for formally analyzing PreScheme programs that manipulate machine integers. Resource requirements: IMPS runs under the X Window System or Open Windows on Sun 4 SPARCstations that have at least 24 MB physical memory (preferably more) and at least a 60 MB swap partition. IMPS is implemented in the T-programming language developed at Yale by N. Adams, R. Kelsey, D. Kranz, J. Philbin, and J. Rees. The executable is self-booting, so you do not need to get your own version of T. The IMPS user interface is built on top of GNU Emacs, developed by R. Stallman. It requires Free Software Foundation GNU Emacs version 19. For typesetting formulas, sequents, theories, etc, IMPS also requires LaTeX and a TeX previewer. Where-to-get-it: Getting it by ftp: Ftp to math.harvard.edu as anonymous and cd to the directory named "imps". This directory will contain a directory named "doc" and several other files. "README" is a file explaining how to install IMPS, report bugs, etc. The file "imps.tar.gz" is the compressed tar file of 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. The directory "doc" contains several papers on IMPS in compressed LaTeX dvi format. Getting it by World Wide Web: Go to the IMPS home page at the URL given above. Getting it by tape: We currently have no plans to send out tapes, although we will consider doing so in exceptional cases. Questions: Please send questions by e-mail to imps-request@linus.mitre.org. W. Farmer, J. Thayer, August 4, 1995 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%