@article(andreka2013,
 author       = {Hajnal Andr{\'e}ka and Judit X. Madar{\'a}sz and Istv{\'a}n N{\'e}meti and Gergely Sz{\'e}kely},
 year         = {2013},
 title        = {An {{Axiom System}} for {{General Relativity Complete}} with Respect to {{Lorentzian Manifolds}}},
 journal      = {arXiv:1310.1475 [gr-qc]},
 eprint       = {1310.1475},
)
@article(andreka2011,
 author       = {Hajnal Andr{\'e}ka and Istv{\'a}n N{\'e}meti and Judit X. Madar{\'a}sz and Gergely Sz{\'e}kely},
 year         = {2011},
 title        = {On {{Logical Analysis}} of {{Relativity Theories}}},
 eprint       = {1105.0885},
)
@inproceedings(cocco2020,
 author       = {Lorenzo Cocco and Joshua Babic},
 year         = {2020},
 title        = {A System of Axioms for {{Minkowski}} Spacetime},
 booktitle    = {Journal of {{Philosophical Logic}}},
)
@incollection(debruijn1994a,
 author       = {{de Bruijn}, N. G.},
 year         = {1994},
 title        = {A {{Survey}} of the {{Project Automath}}},
 editor       = {R. P. Nederpelt and J. H. Geuvers and {de Vrijer}, R. C.},
 booktitle    = {Studies in {{Logic}} and the {{Foundations}} of {{Mathematics}}},
 series       = {Selected {{Papers}} on {{Automath}}},
 volume       = {133},
 publisher    = {{Elsevier}},
 pages        = {141--161},
 doi          = {10.1016/S0049-237X(08)70203-9},
 note         = {Reprinted from: Seldin, J. P. and Hindley, J. R., eds., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 579-606.},
)
@article(dzamonja2020,
 author       = {D{\v z}amonja, Mirna and {Koutsoukou-Argyraki}, Angeliki and Lawrence C. Paulson},
 year         = {2020},
 title        = {Formalising {{Ordinal Partition Relations Using Isabelle}}/{{HOL}}},
 eprint       = {2011.13218},
)
@article(einstein1905,
 author       = {A. Einstein},
 year         = {1905},
 title        = {Zur {{Elektrodynamik}} Bewegter {{K\"orper}}},
 journal      = {Annalen der Physik},
 volume       = {322},
 number       = {10},
 pages        = {891--921},
 doi          = {10.1002/andp.19053221004},
)
@incollection(goldblatt1989,
 author       = {Robert Goldblatt},
 year         = {1989},
 title        = {First-{{Order Spacetime Geometry}}},
 editor       = {Jens Erik Fenstad and Ivan T. Frolov and Risto Hilpinen},
 booktitle    = {Studies in {{Logic}} and the {{Foundations}} of {{Mathematics}}},
 series       = {Logic, {{Methodology}} and {{Philosophy}} of {{Science VIII}}},
 volume       = {126},
 publisher    = {{Elsevier}},
 pages        = {303--316},
 doi          = {10.1016/S0049-237X(08)70051-X},
)
@book(goldblatt2012,
 author       = {Robert Goldblatt},
 year         = {2012},
 title        = {Orthogonality and {{Spacetime Geometry}}},
 publisher    = {{Springer Science \& Business Media}},
)
@incollection(harrison2009,
 author       = {John Harrison},
 year         = {2009},
 title        = {Without {{Loss}} of {{Generality}}},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Theorem {{Proving}} in {{Higher Order Logics}}},
 volume       = {5674},
 publisher    = {{Springer, Berlin, Heidelberg}},
 pages        = {43--59},
 doi          = {10.1007/978-3-642-03359-9\_3},
)
@book(hilbert1950,
 author       = {David Hilbert},
 year         = {1950},
 title        = {The {{Foundations}} of {{Geometry}}},
 publisher    = {{The Open Court Publishing Company}},
)
@inproceedings(meikle2010,
 author       = {Laura Meikle and Jacques Fleuriot},
 year         = {2010},
 title        = {Automation for {{Geometry}} in {{Isabelle}}/{{HOL}}.},
 booktitle    = {{{PAAR}}@ {{IJCAR}}},
 pages        = {84--94},
)
@inproceedings(meikle2003,
 author       = {Laura I. Meikle and Jacques D. Fleuriot},
 year         = {2003},
 title        = {Formalizing {{Hilbert}}'s {{Grundlagen}} in {{Isabelle}}/{{Isar}}},
 editor       = {David Basin and Burkhart Wolff},
 booktitle    = {Theorem {{Proving}} in {{Higher Order Logics}}},
 series       = {Lecture {{Notes}} in {{Computer Science}}},
 publisher    = {{Springer}},
 address      = {{Berlin, Heidelberg}},
 pages        = {319--334},
 doi          = {10.1007/10930755\_21},
)
@article(minkowski1908,
 author       = {Herrman Minkowski},
 year         = {1908},
 title        = {Die {{Grundgleichungen}} F\"ur Die Elektromagnetischen {{Vorg\"ange}} in Bewegten {{K\"orpern}}},
 journal      = {Nachrichten von der Gesellschaft der Wissenschaften zu G\"ottingen, Mathematisch-Physikalische Klasse},
 pages        = {53--111},
)
@article(mundy1986,
 author       = {Brent Mundy},
 year         = {1986},
 title        = {Optical {{Axiomatization}} of {{Minkowski Space}}-{{Time Geometry}}},
 journal      = {Philosophy of Science},
 volume       = {53},
 number       = {1},
 pages        = {1--30},
 doi          = {10.1086/289289},
)
@article(mundy1986a,
 author       = {Brent Mundy},
 year         = {1986},
 title        = {The {{Physical Content}} of {{Minkowski Geometry}}},
 journal      = {The British Journal for the Philosophy of Science},
 volume       = {37},
 number       = {1},
 pages        = {25--54},
 doi          = {10.1093/oxfordjournals.bjps/37.1.25},
)
@inbook(narboux2018,
 author       = {Julien Narboux and Predrag Janicic and Jacques Fleuriot},
 year         = {2018},
 title        = {Computer-Assisted Theorem Proving in Synthetic Geometry},
 edition      = {1st},
 pages        = {21--60},
 publisher    = {Chapman and Hall/CRC},
)
@inproceedings(palmer2018,
 author       = {Jake Palmer and Jacques D Fleuriot},
 year         = {2018},
 title        = {Mechanising an {{Independent Axiom System}} for {{Minkowski Space}}-Time},
 booktitle    = {Proceedings of the 12th {{International Conference}} on {{Automated Deduction}} in {{Geometry}}},
 pages        = {64--79},
)
@book(robb1936,
 author       = {Alfred A. Robb},
 year         = {1936},
 title        = {Geometry of {{Time}} and {{Space}}},
 publisher    = {{Cambridge University Press}},
)
@article(schmoetten2021,
 author       = {Richard Schmoetten and Jake E. Palmer and Jacques D. Fleuriot},
 year         = {2021},
 title        = {Towards {{Formalising Schutz}}' {{Axioms}} for {{Minkowski Spacetime}} in {{Isabelle}}/{{HOL}}},
 journal      = {arXiv:2108.10868 [gr-qc]},
 eprint       = {2108.10868},
)
@book(schutz1973,
 author       = {John W. Schutz},
 year         = {1973},
 title        = {Foundations of {{Special Relativity}}: {{Kinematic Axioms}} for {{Minkowski Space}}-{{Time}}},
 series       = {Lecture {{Notes}} in {{Mathematics}}},
 volume       = {361},
 publisher    = {{Springer Berlin Heidelberg}},
 address      = {{Berlin, Heidelberg}},
 doi          = {10.1007/BFb0066798},
)
@article(schutz1981,
 author       = {John W. Schutz},
 year         = {1981},
 title        = {An Axiomatic System for {{Minkowski}} Space\textendash Time},
 journal      = {Journal of Mathematical Physics},
 volume       = {22},
 number       = {2},
 pages        = {293--302},
 doi          = {10.1063/1.524877},
)
@book(schutz1997,
 author       = {John W. Schutz},
 year         = {1997},
 title        = {Independent {{Axioms}} for {{Minkowski Space}}-{{Time}}},
 publisher    = {{CRC Press}},
)
@phdthesis(scott2008,
 author       = {Phil Scott},
 year         = {2008},
 title        = {Mechanising {{Hilbert}}'s {{Foundations}} of {{Geometry}} in {{Isabelle}}},
 type         = {Master's thesis},
 school       = {School of Informatics},
 address      = {{The University of Edinburgh}},
)
@phdthesis(scott2015,
 author       = {Phil Scott},
 year         = {2015},
 title        = {Ordered Geometry in {{Hilbert}}'s {{Grundlagen}} Der {{Geometrie}}},
 type         = {{{PhD Thesis}}},
 school       = {The University of Edinburgh},
 address      = {{School of Informatics}},
)
@inproceedings(scott2011,
 author       = {Phil Scott and Jacques Fleuriot},
 year         = {2011},
 title        = {An {{Investigation}} of {{Hilbert}}'s {{Implicit Reasoning}} through {{Proof Discovery}} in {{Idle}}-{{Time}}},
 editor       = {Pascal Schreck and Julien Narboux and {Richter-Gebert}, J{\"u}rgen},
 booktitle    = {Automated {{Deduction}} in {{Geometry}}},
 series       = {Lecture {{Notes}} in {{Computer Science}}},
 publisher    = {{Springer}},
 address      = {{Berlin, Heidelberg}},
 pages        = {182--200},
 doi          = {10.1007/978-3-642-25070-5\_11},
)
@article(stannett2014,
 author       = {Mike Stannett and Istv{\'a}n N{\'e}meti},
 year         = {2014},
 title        = {Using {{Isabelle}}/{{HOL}} to {{Verify First}}-{{Order Relativity Theory}}},
 journal      = {Journal of Automated Reasoning},
 volume       = {52},
 number       = {4},
 pages        = {361--378},
 doi          = {10.1007/s10817-013-9292-7},
)
@article(szekeres1968,
 author       = {G. Szekeres},
 year         = {1968},
 title        = {Kinematic Geometry; an Axiomatic System for {{Minkowski}} Space-Time: {{M}}. {{L}}. {{Urquhart}} in {{Memoriam}}},
 journal      = {Journal of the Australian Mathematical Society},
 volume       = {8},
 number       = {2},
 pages        = {134--160},
 doi          = {10.1017/S1446788700005188},
)
@incollection(walker1959,
 author       = {A. G. Walker},
 year         = {1959},
 title        = {Axioms for {{Cosmology}}},
 editor       = {Leon Henkin and Patrick Suppes and Alfred Tarski},
 booktitle    = {Studies in {{Logic}} and the {{Foundations}} of {{Mathematics}}},
 series       = {The {{Axiomatic Method}}},
 volume       = {27},
 publisher    = {{Elsevier}},
 pages        = {308--321},
 doi          = {10.1016/S0049-237X(09)70036-9},
)
@techreport(wiedijk2000,
 author       = {Freek Wiedijk},
 year         = {2000},
 title        = {The {{De Bruijn}} Factor},
 type         = {Technical Report},
 institution  = {{Department of Computer Science}},
 address      = {{Nijmegen University}},
)