IMPS
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.
Keywords for this software
References in zbMATH (referenced in 52 articles , 1 standard article )
Showing results 1 to 20 of 52.
Sorted by year (- Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
- Kohlhase, Michael; Rabe, Florian: Experiences from exporting major proof assistant libraries (2021)
- Betzendahl, Jonas; Kohlhase, Michael: Translating the IMPS theory library to MMT/OMDoc (2018)
- Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
- Maggesi, Marco: A formalization of metric spaces in HOL Light (2018)
- Müller, Dennis; Kohlhase, Michael; Rabe, Florian: Automatically finding theory morphisms for knowledge management (2018)
- Berger, Ulrich; Hou, Tie: A realizability interpretation of Church’s simple theory of types (2017)
- Carette, Jacques; Farmer, William M.: Formalizing mathematical knowledge as a biform theory graph: a case study (2017)
- Kohlhase, Michael; Rabe, Florian: QED reloaded: towards a pluralistic formal library of mathematical knowledge (2016)
- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (extended version) (2016)
- Rabe, Florian: Lax theory morphisms (2015)
- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (2015)
- Kaliszyk, Cezary; Rabe, Florian: Towards knowledge management for HOL Light (2014)
- Rabe, Florian; Kohlhase, Michael: A scalable module system (2013)
- Sabel, David; Schmidt-Schauß, Manfred: A two-valued logic for properties of strict functional programs allowing partial functions (2013)
- Guttman, Joshua D.: State and progress in strand spaces: proving fair exchange (2012)
- Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
- Farmer, William M.; Grigorov, Orlin G.: Panoptes: an exploration tool for formal proofs (2009)
- Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei: TPS: A theorem proving system for classical type theory (2008)
- Farmer, William M.: The seven virtues of simple type theory (2008)