@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%