Proof verification technology and elementary physics

DOI10.1007/978-1-4939-9051-1_4MaRDI QIDQ3296311zbMATH OpenOpenAlexFDO

Authors Ernest Davis

Publication date 7 July 2020

Published in Algorithms and Complexity in Mathematics, Epistemology, and Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-1-4939-9051-1_4

Mathematics Subject Classification ID

Physics (00A79) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 2152637
• Theory Is Forever
• Developments in formal proofs
• Computer-assisted discovery and proof
• Computer theorem proving in mathematics

Cites work

• scientific article; zbMATH DE number 5560312 (Why is no real title available?)
• scientific article; zbMATH DE number 3931797 (Why is no real title available?)
• scientific article; zbMATH DE number 4036509 (Why is no real title available?)
• scientific article; zbMATH DE number 1468963 (Why is no real title available?)
• scientific article; zbMATH DE number 7002608 (Why is no real title available?)
• scientific article; zbMATH DE number 5223003 (Why is no real title available?)
• scientific article; zbMATH DE number 3241252 (Why is no real title available?)
• scientific article; zbMATH DE number 3079157 (Why is no real title available?)
• A formally verified proof of the prime number theorem
• A machine-checked proof of the odd order theorem
• Commonsense reasoning about containers using radically incomplete information
• David Hilbert and the axiomatization of physics (1898--1918). From Grundlagen der Geometrie to Grundlagen der Physik.
• Formalization \textit{of} quantum protocols using Coq
• Formalizing an analytic proof of the prime number theorem
• From Boltzmann to Euler: Hilbert's 6th problem revisited
• Geometry Revealed
• Handbook of knowledge representation.
• How does a box work? A study in the qualitative dynamics of solid objects
• How to grow a mind: statistics, structure, and abstraction
• Isabelle/HOL. A proof assistant for higher-order logic
• Logical formalizations of commonsense reasoning: a survey
• Lost in math. How beauty leads physics astray
• Mathematics, Substance and Surmise
• Physics and proof theory
• Pouring liquids: a study in commonsense physical reasoning
• Probability Theory
• Solution of the Robbins problem
• The Bayesian Treatment of Auxiliary Hypotheses: Reply to Fitelson and Waterman
• The Feynman lectures on physics 4. The structure of matter. Translated from the English by Henner Wessel and Karen Lippert
• The axiomatic method. With special reference to geometry and physics. Proceedings of an International Symposium held at the University of California, Berkeley, December 26, 1957 -- January 4, 1958
• The honors class. Hilbert's problems and their solvers
• The kinematics of cutting solid objects
• The scope and limits of simulation in automated reasoning

Describes a project that uses

Uses Software

• OpenCourseWare
• MathOverflow
• kepler98
• SPASS
• Isabelle/HOL

This page was built for publication: Proof verification technology and elementary physics

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