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 27 articles )
Showing results 1 to 20 of 27.
Sorted by year (- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (extended version) (2016)
- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (2015)
- 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)
- 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)
- 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)
- Bove, Ana; Capretta, Venanzio: Nested general recursion and partiality in type theory (2001)
- Dennis, Louise A.; Smaill, Alan: Ordinal arithmetic: A case study for rippling in a higher order domain (2001)
- Kohlhase, Michael; Franke, Andreas: MBase: Representing knowledge and context for the integration of mathematical software systems (2001)
- Kammüller, Florian: Modular structures as dependent types in Isabelle (1999)
- Bauer, Andrej; Clarke, Edmund; Zhao, Xudong: Analytica --- an experiment in combining theorem proving and symbolic computation (1998)
- Calmet, Jacques: Computer algebra and artificial intelligence (1998)