Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
From MaRDI portal
Publication:2102946
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
Related Items
Uses Software
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
