Email Gateway (Aug 18 2022 at 16:10): Email Gateway (Aug 18 2022 at 16:10):From: Johannes Hölzl <hoelzl@in.tum.de>
At TPHOLS 2009 Osman Hasan, Sanaz Khan Afshar and Sofiene Tahar
presented "Formal Analysis of Optical Waveguides in HOL" which is about
formalizing some physical properties in HOL4. As far as I know, physics
is mostly about calculus, so the Multivariate Analysis found in
HOL-light or Isabelle/HOL and the probability theory available in HOL4
and now also in Isabelle/HOL could be a good starting point.
Multivariate Analysis does also support non-euclidean spaces, which is
surely needed for the theory of relativity, and the probabilty theory
could be helpfully when formalizing quantum problems. So formalizing
some well established physics should be no problem. But how can
formalizing physics help when no theories are available for G.U.T.?
Greetings,
Johannes
Email Gateway (Aug 18 2022 at 16:10):From: Jens Doll <jd@cococo.de>
Hello Johannes,
how about systematically generating axioms and theorems, which satisfy
physical phenomena, and having Isabelle verify them?
Was it possible? Would we need faster machines?
Jens
Email Gateway (Aug 18 2022 at 16:11):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
What you're suggesting sounds quite over the top IMO, but you might be interested in the work of Bundy, Chan, and Lehmann about ontology evolution in physics:
http://dream.inf.ed.ac.uk/projects/ontology_evolution/
Jasmin
Email Gateway (Aug 18 2022 at 16:11):From: Jens Doll <jd@cococo.de>
Thanks, Jasmin. I know that it looks like another Freshman's dream. ;-) Jens
Email Gateway (Aug 18 2022 at 16:11):From: Jens Doll <jd@cococo.de>
Thanks, Jasmin. I know that it looks like another Freshman's dream. ;-) Jens
Last updated: Apr 20 2024 at 12:26 UTC