Formalizing Scientifically Applicable Mathematics in a Definitional Framework

DOI10.6092/issn.1972-5787/4573zbMath1451.68333OpenAlexW2586863512MaRDI QIDQ5195269

Liron Cohen, Arnon Avron

Publication date: 18 September 2019

Full work available at URL: https://doaj.org/article/8a7840a604df464591b85c0cf0a5c0e0

zbMATH Keywords

MKMsafety relationsscientifically applicable mathematics

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30) Formalization of mathematics in connection with theorem provers (68V20) Mathematical knowledge management (68V30)

Related Items

Why Predicative Sets? ⋮ Analysis in a formal predicative set theory ⋮ POINCARÉ–WEYL’S PREDICATIVITY: GOING BEYOND ⋮ Applicable Mathematics in a Minimal Computational Theory of Sets ⋮ Unnamed Item ⋮ WEYL REEXAMINED: “DAS KONTINUUM” 100 YEARS LATER ⋮ Introduction: Non-classical Logics—Between Semantics and Proof Theory (In Relation to Arnon Avron’s Work)

Uses Software

• Isabelle/HOL
• Mizar
• Automath

Cites Work

• Set theory. An introduction to independence proofs. 2nd print
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Isabelle/HOL. A proof assistant for higher-order logic
• Constructibility and decidability versus domain independence and absoluteness
• Foundations of set theory. With the collaboration of Dirk van Dalen. 2nd revised ed
• Mathematical Knowledge Management
• Systems of predicative analysis
• A Framework for Formalizing Set Theories Based on the Use of Static Set Terms
• Systems of predicative analysis, II: Representations of ordinals
• The fine structure of the constructible hierarchy
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item