IMPS: An interactive mathematical proof system
From MaRDI portal
Publication:1319391
DOI10.1007/BF00881906zbMath0802.68129OpenAlexW2137810559MaRDI QIDQ1319391
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 logicpartial functionsinteractive theorem provingautomated analysiscomputing with theoremstheory interpretation
Related Items
Lax Theory Morphisms, Formalizing mathematical knowledge as a biform theory graph: a case study, Automating change of representation for proofs in discrete mathematics (extended version), Automating Change of Representation for Proofs in Discrete Mathematics, Joshua Guttman: pioneering strand spaces, An approach to literate and structured formal developments, TPS: A hybrid automatic-interactive system for developing proofs, A two-valued logic for properties of strict functional programs allowing partial functions, Crystal: Integrating structured queries into a tactic language, Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge, TPS: A theorem-proving system for classical type theory, A scalable module system, Structuring theories with implicit morphisms, A realizability interpretation of Church's simple theory of types, Morphism equality in theory graphs, Computer algebra and artificial intelligence, State and progress in strand spaces: proving fair exchange, Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates, Structure-preserving diagram operators, The seven virtues of simple type theory, IMPS: An updated system description, Walther recursion, A formalization of metric spaces in HOL Light, Incorporating quotation and evaluation into Church's type theory, Deduction as an Engineering Science, Organizing numerical theories using axiomatic type classes, MBase: Representing knowledge and context for the integration of mathematical software systems, A fixedpoint approach to implementing (Co)inductive definitions, Proof script pragmatics in IMPS, A mechanization of strong Kleene logic for partial functions, IMPS, Formalising foundations of mathematics, Adapting functional programs to higher order logic, Experiences from exporting major proof assistant libraries, Towards Knowledge Management for HOL Light, Panoptes
Uses Software
Cites Work
- Inference rules using local contexts
- The calculus of constructions
- Elementary induction on abstract structures
- Second-order languages and mathematical practice
- Systems of predicative analysis
- A partial functions version of Church's simple theory of types
- A formulation of the simple theory of types
- Completeness in the theory of types
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
