@inproceedings{b3df9a8244584736a86d633447ddead2,
title = "Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems",
abstract = "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{"}.",
author = "Richard Schmoetten and Jake Palmer and Jacques Fleuriot",
year = "2021",
month = dec,
day = "30",
doi = "10.4204/EPTCS.352.13",
language = "English",
volume = "352",
series = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
publisher = "Open Publishing Association",
pages = "116--128",
editor = "Predrag Jani{\v c}i{\'c} and Zolt{\'a}n Kov{\'a}cs",
booktitle = "Proceedings of the 13th International Conference on Automated Deduction in Geometry 2021",
address = "Australia",
note = "13th International Conference on Automated Deduction in Geometry, ADG 2021 ; Conference date: 15-09-2021 Through 17-09-2021",
}