Using Isabelle to verify special relativity, with application to hypercomputation theory

Mike Stannett, István Németi

Logicians at the Rényi Mathematical Institute in Budapest have spent several years developing versions of relativity theory (special, general, and other variants) based wholly on f…