Title: Mechanising Newtonian Mechanics in Isabelle
Speaker: Lars Werne
Abstract: 

The Isabelle Theorem Prover is an interactive framework for developing formal mathematical theories that checks proofs for validity using the rules of Higher Order Logic. In my talk, I will present the state of my project on the mechanisation of Newtonian mechanics using this framework.

In my work thus far, I have focused on the interplay of forces acting on point particles and their position, velocity, and acceleration, based on Newton’s fundamental laws of motion and previous results on abstract analysis from the Isabelle proof library. In the coming months, some of main aims will be to generalise my current implementation so that “space” is treated as an arbitrary real vector space, and expand on my results on central, conservative forces and their properties