Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
From MaRDI portal
Publication:2102946
DOI10.1007/S10817-022-09643-1OpenAlexW3195133477WikidataQ114689845 ScholiaQ114689845MaRDI QIDQ2102946FDOQ2102946
Authors: Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot 
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
Recommendations
- Axiomatization of special relativity in first order logic
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Hermann Minkowski, Relativity and the Axiomatic Approach to Physics
- scientific article; zbMATH DE number 1112206
- Axiomatic foundations of the kinematics common to classical physics and special relativity
Cites Work
- The Isabelle Framework
- Edinburgh LCF. A mechanized logic of computation
- The Kepler Conjecture
- A formulation of the Kepler conjecture
- PCT, spin and statistics, and all that.
- Title not available (Why is that?)
- Title not available (Why is that?)
- From Tarski to Hilbert
- Mechanical Theorem Proving in Tarski’s Geometry
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Title not available (Why is that?)
- Orthogonality and spacetime geometry
- Title not available (Why is that?)
- Formalizing projective plane geometry in Coq
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Title not available (Why is that?)
- A note on `Einstein's special relativity beyond the speed of light by James M. Hill and Barry J. Cox'
- A potential foundation for emergent space-time
- Logical analysis of relativity theories
- Using Isabelle/HOL to verify first-order relativity theory
- Verisimilitude Redefined
- Title not available (Why is that?)
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- Foundations of special relativity: Kinematic axioms for Minkowski space- time
- An axiomatic system for Minkowski space–time
- Title not available (Why is that?)
- Without Loss of Generality
- Special Relativity in General Frames
- A system of axioms for Minkowski spacetime
- Term rewriting and beyond -- theorem proving in Isabelle
- Title not available (Why is that?)
- Kinematic geometry; an axiomatic system for Minkowski space-time
- Title not available (Why is that?)
- Comprehending Isabelle/HOL’s Consistency
- Formalizing Ordinal Partition Relations Using Isabelle/HOL
- An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
- From LCF to Isabelle/HOL
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- The significance of Ptolemy's Almagest for its early readers
Cited In (2)
Uses Software
This page was built for publication: Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102946)
