Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
type: Item
instance of: scholarly article
title: Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
author: Richard Schmoetten
author: Jake E. Palmer
author: Jacques D. Fleuriot
published in: Journal of Automated Reasoning
publication date: 2022-12-12T00:00:00Z
full work available at URL: https://arxiv.org/abs/2108.10868
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7632096
zbMATH Keywords: Isabelle
zbMATH Keywords: relativity
zbMATH Keywords: Minkowski
zbMATH Keywords: synthetic geometry
describes a project that uses: Isabelle
describes a project that uses: Archive Formal Proofs
describes a project that uses: Isabelle/Isar
describes a project that uses: Automath
describes a project that uses: Isabelle/HOL
describes a project that uses: Isar
describes a project that uses: kepler98
describes a project that uses: Sledgehammer
MaRDI profile type: Publication
Wikidata QID: Q114689845
OpenAlex ID: W3195133477
cites work: Q3367316
cites work: A note on `Einstein's special relativity beyond the speed of light by James M. Hill and Barry J. Cox'
cites work: The significance of ptolemy's Almagest for its early readers
cites work: From Tarski to Hilbert
cites work: A system of axioms for Minkowski spacetime
cites work: Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
cites work: Q5719494
cites work: Formalizing Ordinal Partition Relations Using Isabelle/HOL
cites work: Q4735709
cites work: Orthogonality and spacetime geometry
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Special Relativity in General Frames
cites work: A formulation of the Kepler conjecture
cites work: Without Loss of Generality
cites work: Q3234138
cites work: A potential foundation for emergent space-time
cites work: Comprehending Isabelle/HOL’s Consistency
cites work: The Kepler Conjecture
cites work: Formalizing Projective Plane Geometry in Coq
cites work: Formalizing Hilbert’s Grundlagen in Isabelle/Isar
cites work: Verisimilitude Redefined
cites work: Mechanical Theorem Proving in Tarski’s Geometry
cites work: Q4556039
cites work: Term rewriting and beyond -- theorem proving in Isabelle
cites work: From LCF to Isabelle/HOL
cites work: Foundations of special relativity: Kinematic axioms for Minkowski space- time
cites work: An axiomatic system for Minkowski space–time
cites work: Q4373932
cites work: A type-theoretical alternative to ISWIM, CUCH, OWHY
cites work: An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
cites work: Using Isabelle/HOL to verify first-order relativity theory
cites work: PCT, spin and statistics, and all that.
cites work: Kinematic geometry; an axiomatic system for Minkowski space-time
cites work: Q4781180
cites work: Q3268764
cites work: Q3263441
cites work: Q5219926
cites work: The Isabelle Framework
DOI: 10.1007/S10817-022-09643-1
description: scientific article; zbMATH DE number 7632096