×

IMPS

swMATH ID: 9143
Software Authors: Farmer, William M.; Guttman, Joshua D.; Thayer, F.Javier
Description: IMPS: An interactive mathematical proof system. 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 contained over a thousand repeatable proofs covers significant portions of logic, algebra, and analysis and provides some support for modeling applications in computer science.
Homepage: http://imps.mcmaster.ca/
Keywords: interactive theorem proving; automated analysis; computing with theorems; theory interpretation; higher-order logic; partial functions
Related Software: Isabelle; Nuprl; Coq; HOL; PVS; ETPS; ML; HOL Light; Isabelle/HOL; TPS; MMT; Mizar; Automath; Analytica; OMDoc; Mathematica; TPTP; QMT; Theorema; OMRS
Cited in: 51 Publications

Citations by Year