Hajnal Andréka, Judit X. Madarász, István Németi & Gergely Székely (2013):
An Axiom System for General Relativity Complete with Respect to Lorentzian Manifolds.
arXiv:1310.1475 [gr-qc].
ArXiv:1310.1475.
Hajnal Andréka, István Németi, Judit X. Madarász & Gergely Székely (2011):
On Logical Analysis of Relativity Theories.
ArXiv:1105.0885.
Lorenzo Cocco & Joshua Babic (2020):
A System of Axioms for Minkowski Spacetime.
In: Journal of Philosophical Logic.
N. G. de Bruijn (1994):
A Survey of the Project Automath.
In: R. P. Nederpelt, J. H. Geuvers & R. C. de Vrijer: Studies in Logic and the Foundations of Mathematics,
Selected Papers on Automath 133.
Elsevier,
pp. 141–161,
doi:10.1016/S0049-237X(08)70203-9.
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..
Mirna Džamonja, Angeliki Koutsoukou-Argyraki & Lawrence C. Paulson (2020):
Formalising Ordinal Partition Relations Using Isabelle/HOL.
ArXiv:2011.13218.
A. Einstein (1905):
Zur Elektrodynamik Bewegter Körper.
Annalen der Physik 322(10),
pp. 891–921,
doi:10.1002/andp.19053221004.
Robert Goldblatt (1989):
First-Order Spacetime Geometry.
In: Jens Erik Fenstad, Ivan T. Frolov & Risto Hilpinen: Studies in Logic and the Foundations of Mathematics,
Logic, Methodology and Philosophy of Science VIII 126.
Elsevier,
pp. 303–316,
doi:10.1016/S0049-237X(08)70051-X.
Robert Goldblatt (2012):
Orthogonality and Spacetime Geometry.
Springer Science & Business Media.
John Harrison (2009):
Without Loss of Generality.
In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics 5674.
Springer, Berlin, Heidelberg,
pp. 43–59,
doi:10.1007/978-3-642-03359-9_3.
David Hilbert (1950):
The Foundations of Geometry.
The Open Court Publishing Company.
Laura Meikle & Jacques Fleuriot (2010):
Automation for Geometry in Isabelle/HOL..
In: PAAR@ IJCAR,
pp. 84–94.
Laura I. Meikle & Jacques D. Fleuriot (2003):
Formalizing Hilbert's Grundlagen in Isabelle/Isar.
In: David Basin & Burkhart Wolff: Theorem Proving in Higher Order Logics,
Lecture Notes in Computer Science.
Springer,
Berlin, Heidelberg,
pp. 319–334,
doi:10.1007/10930755_21.
Herrman Minkowski (1908):
Die Grundgleichungen Für Die Elektromagnetischen Vorgänge in Bewegten Körpern.
Nachrichten von der Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-Physikalische Klasse,
pp. 53–111.
Brent Mundy (1986):
Optical Axiomatization of Minkowski Space-Time Geometry.
Philosophy of Science 53(1),
pp. 1–30,
doi:10.1086/289289.
Brent Mundy (1986):
The Physical Content of Minkowski Geometry.
The British Journal for the Philosophy of Science 37(1),
pp. 25–54,
doi:10.1093/oxfordjournals.bjps/37.1.25.
Julien Narboux, Predrag Janicic & Jacques Fleuriot (2018):
Computer-Assisted Theorem Proving in Synthetic Geometry,
1st edition,
pp. 21–60.
Chapman and Hall/CRC.
Jake Palmer & Jacques D Fleuriot (2018):
Mechanising an Independent Axiom System for Minkowski Space-Time.
In: Proceedings of the 12th International Conference on Automated Deduction in Geometry,
pp. 64–79.
Alfred A. Robb (1936):
Geometry of Time and Space.
Cambridge University Press.
Richard Schmoetten, Jake E. Palmer & Jacques D. Fleuriot (2021):
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL.
arXiv:2108.10868 [gr-qc].
ArXiv:2108.10868.
John W. Schutz (1973):
Foundations of Special Relativity: Kinematic Axioms for Minkowski Space-Time.
Lecture Notes in Mathematics 361.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
doi:10.1007/BFb0066798.
John W. Schutz (1981):
An Axiomatic System for Minkowski SpaceTime.
Journal of Mathematical Physics 22(2),
pp. 293–302,
doi:10.1063/1.524877.
John W. Schutz (1997):
Independent Axioms for Minkowski Space-Time.
CRC Press.
Phil Scott (2008):
Mechanising Hilbert's Foundations of Geometry in Isabelle.
Master's thesis.
School of Informatics,
The University of Edinburgh.
Phil Scott (2015):
Ordered Geometry in Hilbert's Grundlagen Der Geometrie.
PhD Thesis.
The University of Edinburgh,
School of Informatics.
Phil Scott & Jacques Fleuriot (2011):
An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time.
In: Pascal Schreck, Julien Narboux & Jürgen Richter-Gebert: Automated Deduction in Geometry,
Lecture Notes in Computer Science.
Springer,
Berlin, Heidelberg,
pp. 182–200,
doi:10.1007/978-3-642-25070-5_11.
Mike Stannett & István Németi (2014):
Using Isabelle/HOL to Verify First-Order Relativity Theory.
Journal of Automated Reasoning 52(4),
pp. 361–378,
doi:10.1007/s10817-013-9292-7.
G. Szekeres (1968):
Kinematic Geometry; an Axiomatic System for Minkowski Space-Time: M. L. Urquhart in Memoriam.
Journal of the Australian Mathematical Society 8(2),
pp. 134–160,
doi:10.1017/S1446788700005188.
A. G. Walker (1959):
Axioms for Cosmology.
In: Leon Henkin, Patrick Suppes & Alfred Tarski: Studies in Logic and the Foundations of Mathematics,
The Axiomatic Method 27.
Elsevier,
pp. 308–321,
doi:10.1016/S0049-237X(09)70036-9.
Freek Wiedijk (2000):
The De Bruijn Factor.
Technical Report.
Department of Computer Science,
Nijmegen University.
eptcs@eptcs.org