Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946): Difference between revisions

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