在Isabelle/HOL中形式化Schutz闵可夫斯基时空公理
计算机科学中的逻辑
2021-09-07 v2 广义相对论与量子宇宙学
摘要
狭义相对论是现代物理理论的基石。虽然今天一个标准的坐标模型广为人知并被广泛教授，但存在几种替代的公理系统。本文报告了对其中一个系统的形式化，该系统在精神上更接近希尔伯特对欧几里得几何的公理化方法，而非闵可夫斯基采用的向量空间方法。我们展示了在Isabelle/HOL中对公理系统以及与时间顺序相关的定理的机械化。文中讨论了证明和Isabelle/Isar脚本的摘录，特别是在形式化工作需要额外步骤、替代方法或对Schutz原文进行修正的地方。
引用
@article{arxiv.2108.10868,
title = {Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL},
author = {Richard Schmoetten and Jake E. Palmer and Jacques D. Fleuriot},
journal= {arXiv preprint arXiv:2108.10868},
year = {2021}
}
备注
45 pages, 7 figures, submitted to Journal of Automated Reasoning. V2: updated title page