Proof verification and proof discovery for relativity

DOI10.1007/S11229-014-0424-3MaRDI QIDQ514557zbMATH OpenOpenAlexFDO

Authors Naveen Sundar Govindarajalulu, Selmer Bringsjord, Joshua A. Taylor

Publication date 9 March 2017

Published in Synthese (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11229-014-0424-3

zbMATH Keywords

automated physicsaxiomatizations in physicslogic and relativityproof verificationtheorem proving in physics

Mathematics Subject Classification ID

Computational methods for problems pertaining to relativity and gravitational theory (83-08)

Recommendations

• Using Isabelle/HOL to verify first-order relativity theory
• Computer theorem proving in mathematics
• Mathematics by machine
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• scientific article; zbMATH DE number 3880145

Cites work

• A Brief Overview of Mizar
• A logic road from special relativity to general relativity
• Computability and Logic
• scientific article; zbMATH DE number 991288 (Why is no real title available?)
• scientific article; zbMATH DE number 3146798 (Why is no real title available?)
• scientific article; zbMATH DE number 1292563 (Why is no real title available?)
• scientific article; zbMATH DE number 612169 (Why is no real title available?)
• scientific article; zbMATH DE number 1863375 (Why is no real title available?)
• scientific article; zbMATH DE number 824731 (Why is no real title available?)
• Logical analysis of relativity theories
• Using Isabelle/HOL to verify first-order relativity theory
• Vivid: a framework for heterogeneous problem solving

Cited in

(6)

• Investigations of isotropy and homogeneity of spacetime in first-order logic
• Using Isabelle/HOL to verify first-order relativity theory
• Formalizing physics: automation, presentation and foundation issues
• Is universal computation a myth?
• GROUPS OF WORLDVIEW TRANSFORMATIONS IMPLIED BY EINSTEIN’S SPECIAL PRINCIPLE OF RELATIVITY OVER ARBITRARY ORDERED FIELDS
• Axiomatizing relativistic dynamics using formal thought experiments

Describes a project that uses

Uses Software

• Mathematica
• Vivid
• SNARK
• Mizar

This page was built for publication: Proof verification and proof discovery for relativity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q514557)