Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL

DOI10.1007/s10817-022-09643-1OpenAlexW3195133477WikidataQ114689845 ScholiaQ114689845MaRDI QIDQ2102946

Jacques D. Fleuriot, Jake E. Palmer, Richard Schmoetten

Publication date: 12 December 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2108.10868

zbMATH Keywords

relativityIsabellesynthetic geometryMinkowski

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• Isar
• Sledgehammer
• Automath
• kepler98
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A formulation of the Kepler conjecture
• A system of axioms for Minkowski spacetime
• Term rewriting and beyond -- theorem proving in Isabelle
• Orthogonality and spacetime geometry
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Edinburgh LCF. A mechanized logic of computation
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
• Foundations of special relativity: Kinematic axioms for Minkowski space- time
• From LCF to Isabelle/HOL
• Using Isabelle/HOL to verify first-order relativity theory
• A note on ‘Einstein's special relativity beyond the speed of light by James M. Hill and Barry J. Cox’
• From Tarski to Hilbert
• A potential foundation for emergent space-time
• Comprehending Isabelle/HOL’s Consistency
• The significance of ptolemy's Almagest for its early readers
• Formalizing Projective Plane Geometry in Coq
• The Kepler Conjecture
• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
• Without Loss of Generality
• The Isabelle Framework
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Verisimilitude Redefined
• An axiomatic system for Minkowski space–time
• Special Relativity in General Frames
• Formalizing Ordinal Partition Relations Using Isabelle/HOL
• Mechanical Theorem Proving in Tarski’s Geometry
• Kinematic geometry; an axiomatic system for Minkowski space-time