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 34 articles )
Showing results 1 to 20 of 34.
Sorted by year (- 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)
- 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)
- Owens, Scott; Slind, Konrad: Adapting functional programs to higher order logic (2008)
- Andrews, Peter B.; Brown, Chad E.: TPS: A hybrid automatic-interactive system for developing proofs (2006)
- Cantone, Domenico; Cincotti, Gianluca; Gallo, Giovanni: Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates (2006)
- Kutsia, Temur; Buchberger, Bruno: Predicate logic with sequence variables and sequence function symbols (2004)
- Paulson, Lawrence C.: Organizing numerical theories using axiomatic type classes (2004)
- Cantone, Domenico; Omodeo, Eugenio G.; Schwartz, Jacob T.; Ursino, Pietro: Notes from the logbook of a proof-checker’s project (2003)
- Farmer, William M.; von Mohrenschildt, Martin: An overview of a formal framework for managing mathematics (2003)