IMPS: An Interactive Mathematical Proof System

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 1991
Accession Number
ADA243162

Entities

People

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

Organizations

  • MITRE Corporation

Tags

Communities of Interest

  • Energy and Power Technologies
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Binomials
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Human-Machine Interaction
  • Language
  • Logic
  • Mathematical Analysis
  • Mathematical Logic
  • Mathematics
  • Notation
  • Numbers
  • Real Numbers
  • Recursive Functions

Readers

  • Mathematical Modeling and Probability Theory.
  • Space Exploration and Orbital Mechanics.
  • Theoretical Analysis.

Technology Areas

  • AI & ML