IMPS: An interactive mathematical proof system
From MaRDI portal
Publication:1319391
DOI10.1007/BF00881906zbMATH Open0802.68129OpenAlexW2137810559MaRDI QIDQ1319391FDOQ1319391
Publication date: 12 April 1994
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00881906
higher-order logicinteractive theorem provingautomated analysispartial functionscomputing with theoremstheory interpretation
Cites Work
- Elementary induction on abstract structures
- A formulation of the simple theory of types
- Completeness in the theory of types
- Systems of predicative analysis
- The calculus of constructions
- Second-order languages and mathematical practice
- Inference rules using local contexts
- A partial functions version of Church's simple theory of types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (38)
- A formalization of metric spaces in HOL Light
- A realizability interpretation of Church's simple theory of types
- Lax Theory Morphisms
- Elements of mathematical analysis in PVS
- Set theory, higher order logic or both?
- A scalable module system
- Towards Knowledge Management for HOL Light
- Adapting functional programs to higher order logic
- Computer algebra and artificial intelligence
- The seven virtues of simple type theory
- Automating Change of Representation for Proofs in Discrete Mathematics
- Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates
- Structure-preserving diagram operators
- Incorporating quotation and evaluation into Church's type theory
- MBase: Representing knowledge and context for the integration of mathematical software systems
- State and progress in strand spaces: proving fair exchange
- Walther recursion
- Automating change of representation for proofs in discrete mathematics (extended version)
- An approach to literate and structured formal developments
- Organizing numerical theories using axiomatic type classes
- Proof script pragmatics in IMPS
- Joshua Guttman: pioneering strand spaces
- Crystal: Integrating structured queries into a tactic language
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- IMPS
- Panoptes
- TPS: A theorem-proving system for classical type theory
- A fixedpoint approach to implementing (Co)inductive definitions
- A two-valued logic for properties of strict functional programs allowing partial functions
- TPS: A hybrid automatic-interactive system for developing proofs
- Formalising foundations of mathematics
- Experiences from exporting major proof assistant libraries
- Structuring theories with implicit morphisms
- A mechanization of strong Kleene logic for partial functions
- Deduction as an Engineering Science
- IMPS: An updated system description
- Morphism equality in theory graphs
- Formalizing mathematical knowledge as a biform theory graph: a case study
Uses Software
This page was built for publication: IMPS: An interactive mathematical proof system
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1319391)
