Using Isabelle/HOL to verify first-order relativity theory

DOI10.1007/s10817-013-9292-7zbMath1314.68287arXiv1211.6468OpenAlexW2085972255WikidataQ57691192 ScholiaQ57691192MaRDI QIDQ2351148

Mike Stannett, Istvan Németi

Publication date: 23 June 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1211.6468

zbMATH Keywords

hypercomputation\texttt{Isabelle/HOL}first-order relativity theoryphysics and computation

Mathematics Subject Classification ID

Related Items (5)

Investigations of isotropy and homogeneity of spacetime in first-order logic ⋮ GROUPS OF WORLDVIEW TRANSFORMATIONS IMPLIED BY EINSTEIN’S SPECIAL PRINCIPLE OF RELATIVITY OVER ARBITRARY ORDERED FIELDS ⋮ Specification, testing and verification of unconventional computations using generalizedX-machines ⋮ Proof verification and proof discovery for relativity ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• Isar

Cites Work

• A logic road from special relativity to general relativity
• Proof verification and proof discovery for relativity
• Formal statement of the special principle of relativity
• Axiomatizing relativistic dynamics without conservation postulates
• On the possibility of supertasks in general relativity
• The existence of superluminal particles is consistent with the kinematics of Einstein's special theory of relativity
• The case for hypercomputation
• Relativistic computers and the Turing barrier
• Twin paradox and the logical foundation of relativity theory
• CLOSED TIMELIKE CURVES IN RELATIVISTIC COMPUTATION
• Existence of Faster than Light Signals Implies Hypercomputation already in Special Relativity
• P Systems Controlled by General Topologies
• Deciding Arithmetic Using SAD Computers
• Membrane Systems and Hypercomputation
• On Computable Numbers, with an Application to the Entscheidungsproblem
• Logical Approaches to Computational Barriers
• Non-Turing computations via Malament--Hogarth space-times

This page was built for publication: Using Isabelle/HOL to verify first-order relativity theory