Title: Formalising Minkowski Spacetime
Speaker: Richard Schmoetten
Abstract: My MSc project proposes to formalise an axiomatic system for Minkowski spacetime in the proof assistant Isabelle. I will outline the axioms as originally published by John Schutz in 1997, contrasting them with our current formalisation in Isar. The procedure of de-sugaring and converting a prosaic definition to a workable Isabelle/Isar object is illustrated with an example central to many of the results we are interested in. Using some of our proofs (finished and otherwise) as examples, I will expand on the difficulties I have encountered so far as a novice to automated reasoning.