Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems

Richard Schmoetten
(Artificial Intelligence and its Applications Institute. School of Informatics, University of Edinburgh, United Kingdom)
Jake Palmer
(Artificial Intelligence and its Applications Institute. School of Informatics, University of Edinburgh, United Kingdom)
Jacques Fleuriot
(Artificial Intelligence and its Applications Institute. School of Informatics, University of Edinburgh, United Kingdom)

This contribution reports on the continued formalisation of an axiomatic system for Minkowski spacetime (as used in the study of Special Relativity) 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 brief overview of the axioms as well as of a formalisation of theorems relating to linear order. Proofs and excerpts of Isabelle/Isar scripts are discussed, with a focus on the use of symmetry and reasoning "without loss of generality".

In Predrag Janičić and Zoltán Kovács: Proceedings of the 13th International Conference on Automated Deduction in Geometry (ADG 2021), Hagenberg, Austria/virtual, September 15-17, 2021, Electronic Proceedings in Theoretical Computer Science 352, pp. 116–128.
Published: 30th December 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.352.13 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org