Formalizing Scientifically Applicable Mathematics in a Definitional Framework

DOI10.6092/ISSN.1972-5787/4573MaRDI QIDQ5195269zbMATH OpenOpenAlexFDO

Authors Arnon Avron, Liron Cohen

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) Formalization of mathematics in connection with theorem provers (68V20) Axiomatics of classical set theory and its fragments (03E30) Mathematical knowledge management (68V30)

Recommendations

• Formalising foundations of mathematics
• Mathematical Knowledge Management
• scientific article; zbMATH DE number 4197450
• On the role of formalization in computational mathematics
• Formalizability and knowledge ascriptions in mathematical practice
• Formal semantics and applied mathematics: an inferential account
• Formal methods in the philosophy of science
• A formal framework for managing mathematics
• Formal systems of constructive mathematics

Cites work

• scientific article; zbMATH DE number 3907807 (Why is no real title available?)
• scientific article; zbMATH DE number 3933369 (Why is no real title available?)
• scientific article; zbMATH DE number 3985690 (Why is no real title available?)
• scientific article; zbMATH DE number 4070882 (Why is no real title available?)
• scientific article; zbMATH DE number 3504972 (Why is no real title available?)
• scientific article; zbMATH DE number 3627183 (Why is no real title available?)
• scientific article; zbMATH DE number 1257634 (Why is no real title available?)
• scientific article; zbMATH DE number 1314876 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• A Framework for Formalizing Set Theories Based on the Use of Static Set Terms
• A new approach to predicative set theory
• An introduction to programming and proving with dependent types in Coq
• Constructibility and decidability versus domain independence and absoluteness
• Foundations of set theory. With the collaboration of Dirk van Dalen. 2nd revised ed
• Isabelle/HOL. A proof assistant for higher-order logic
• Mathematical Knowledge Management
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Set theory. An introduction to independence proofs. 2nd print
• Systems of predicative analysis
• Systems of predicative analysis, II: Representations of ordinals
• The fine structure of the constructible hierarchy

Cited in

(13)

• scientific article; zbMATH DE number 4197450 (Why is no real title available?)
• Why Predicative Sets?
• A logical framework for developing and mechanizing set theories
• Foundations of applied mathematics. I
• Weyl reexamined: ``Das Kontinuum 100 years later
• Analysis in a formal predicative set theory
• Introduction: Non-classical Logics—Between Semantics and Proof Theory (In Relation to Arnon Avron’s Work)
• scientific article; zbMATH DE number 7533333 (Why is no real title available?)
• POINCARÉ–WEYL’S PREDICATIVITY: GOING BEYOND
• Two decades of non-classical mathematics: introduction to the special issue
• Applicable mathematics in a minimal computational theory of sets
• A minimal computational theory of a minimal computational universe
• scientific article; zbMATH DE number 2086323 (Why is no real title available?)

Describes a project that uses

Uses Software

• Automath
• Mizar
• Isabelle/HOL

This page was built for publication: Formalizing Scientifically Applicable Mathematics in a Definitional Framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5195269)