IMPS: An Interactive Mathematical Proof System

William M. Farmer, Joshua D. Guttman, F. Javier Thayer

1993

Abstract

IMPS is an Interactive Mathematical Proof System intended as a general
purpose tool for formulating and applying mathematics in a familiar
fashion.  The logic of IMPS is based on a version of simple type
theory with partial functions and subtypes.  Mathematical
specification and inference are performed relative to axiomatic
theories, which can be related to one another via inclusion and theory
interpretation.  IMPS provides relatively large primitive inference
steps to facilitate human control of the deductive process and human
comprehension of the resulting proofs.  An initial theory library
containing almost a thousand repeatable proofs covers significant
portions of logic, algebra and analysis, and provides some support for
modeling applications in computer science.

Keywords: Interactive theorem proving, automated analysis, computing
with theorems, theory interpretation, higher-order logic, partial
functions.