Special Relativity is a cornerstone of modern physical theory. While a standard coordinate model is well-known and widely taught today, several alternative systems of axioms exist. This paper reports on the formalisation of one such system which is closer in spirit to Hilbert's axiomatic approach to Euclidean geometry than to the vector space approach employed by Minkowski. We present a mechanisation in Isabelle/HOL of the system of axioms as well as theorems relating to temporal order. Proofs and excerpts of Isabelle/Isar scripts are discussed, particularly where the formal work required additional steps, alternative approaches, or corrections to Schutz' prose.
翻译：特殊相对性是现代物理理论的基石。虽然标准协调模式在当今广为人知和广泛教授,但存在着几种不同的轴心系统。本文报告了一种此类系统正式化的情况,这种系统在精神上更符合Hilbert对欧几何学的不言而喻的方法,而不是Minkowski采用的矢量空间方法。我们在伊莎贝尔/HOL中展示了与时间顺序有关的轴心系统以及与时间顺序有关的理论的机械化。讨论了伊莎贝尔/伊萨尔脚本的证明和节录,特别是在正式工作需要额外步骤、替代方法或对Schutz的插曲进行校正的情况下。
相关内容
微信扫码咨询专知VIP会员