Accession Number:

ADA243162

Title:

IMPS: An Interactive Mathematical Proof System

Descriptive Note:

Corporate Author:

MITRE CORP BEDFORD MA

Personal Author(s):

• Farmer, W. M.
• Guttman, J. D.
• Thayer, F. J.

Report Date:

1991-07-01

Pagination or Media Count:

53.0

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. The system supports a natural style of inference based on deduction graphs, which are akin to derivations in a sequent calculus.

Descriptors:

• *FUNCTIONS
• TOOLS
• CALCULUS
• THEORY
• MATHEMATICS
• SPECIFICATIONS
• GRAPHS

Subject Categories:

• Numerical Mathematics
• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE