Email Gateway (Apr 10 2024 at 09:56): Email Gateway (Apr 10 2024 at 09:56):From: Alex Shkotin <alex.shkotin@gmail.com>
Dear All,
I have done a google search for axiomatic theory of Mechanics, and we have
some reports after Newton and Lagrange.
Do we have any formal theory for Mechanics?
I have created a small framework
<https://www.researchgate.net/publication/374265191_Theory_framework_-_knowledge_hub_message_1>
for the theory of undirected graphs. Just to show framework possibility.
And I hope to populate it from Isabelle storage
<https://www.isa-afp.org/sessions/undirected_graph_theory/#Undirected_Graph_Basics.html>
this summer.
Now my task is to create a formal theory framework for Mechanics. And by
the way do we have a formal theory of Hilbert's Geometry?
For me the simplest way is just to populate a framework from existing
formal theory.
Thank you in advance,
Alex Shkotin
Independent Computer Scientist ashkotin@acm.org
LinkedIn: https://www.linkedin.com/in/ashkotin/
Ontolog Board of Trustees https://ontologforum.com/
Email Gateway (Apr 10 2024 at 10:11):From: Julien Narboux <narboux@unistra.fr>
Dear Alex,
About Mechanics in Isabelle, I don’t know but I would be curious about your progress.
About geometry, there are several way to formalize geometry: analytic geometry (using coordinates), synthetic geometry (starting from axioms like Hilbert’s, Tarski’s, or Euclid’s), and mixed approach like the metric approach.
The GeoCoq library contains a formalization of geometry based on Tarski/Hilbert/Euclid axioms and link with analytic geometry, this library has been ported to Isabelle by Roland Coghetto:
https://github.com/CoghettoR/IsaGeoCoq2_R1/tree/main <https://github.com/CoghettoR/IsaGeoCoq2_R1/tree/main>
(There is an older version in Archive of formal proofs).
About formalization of some mechanics in Coq, you can have a look at Damien Rouhling thesis:
https://theses.fr/2019AZUR4058
Regards,
Julien Narboux
Email Gateway (Apr 10 2024 at 11:23):From: Alex Shkotin <alex.shkotin@gmail.com>
Dear Julien,
Thank you for your quick response! I'll use it. Coq will keep its lines in
the framework together with Isabelle, HOL4 and other formal languages which
we use for formal ontologies.
Regards,
Alex
ср, 10 апр. 2024 г. в 13:08, Julien Narboux <narboux@unistra.fr>:
Last updated: May 04 2024 at 20:16 UTC