Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
From MaRDI portal
Publication:2102946
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
- scientific article; zbMATH DE number 3119278 (Why is no real title available?)
- scientific article; zbMATH DE number 3147378 (Why is no real title available?)
- scientific article; zbMATH DE number 3151263 (Why is no real title available?)
- scientific article; zbMATH DE number 1112206 (Why is no real title available?)
- scientific article; zbMATH DE number 6984221 (Why is no real title available?)
- scientific article; zbMATH DE number 4122729 (Why is no real title available?)
- scientific article; zbMATH DE number 1825272 (Why is no real title available?)
- scientific article; zbMATH DE number 3182321 (Why is no real title available?)
- A formulation of the Kepler conjecture
- 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
- A system of axioms for Minkowski spacetime
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
- An axiomatic system for Minkowski space–time
- Comprehending Isabelle/HOL’s Consistency
- Edinburgh LCF. A mechanized logic of computation
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Formalizing ordinal partition relations using Isabelle/HOL
- Formalizing projective plane geometry in Coq
- Foundations of special relativity: Kinematic axioms for Minkowski space- time
- From LCF to Isabelle/HOL
- From Tarski to Hilbert
- Interactive theorem proving from the perspective of Isabelle/Isar
- Kinematic geometry; an axiomatic system for Minkowski space-time
- Logical analysis of relativity theories
- Mechanical Theorem Proving in Tarski’s Geometry
- Orthogonality and spacetime geometry
- PCT, spin and statistics, and all that.
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- Special relativity in general frames. From particles to astrophysics. Translated from the French by the author
- Term rewriting and beyond -- theorem proving in Isabelle
- The Isabelle Framework
- The Kepler Conjecture
- The significance of Ptolemy's Almagest for its early readers
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Using Isabelle/HOL to verify first-order relativity theory
- Verisimilitude Redefined
- Without Loss of Generality
Cited in
(3)
Describes a project that uses
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)
