An exercise in Mathematical Engineering - proving weak and strong Goodstein theorems.

Event: ESS Seminar Speaker: Jean-Raymond Abrial Location: 58 / 1065 (Murray Building) Date: Tuesday, 27/06/2017 Time: 14:00–15:00 Material:

Abstract

For many years I have been working on some technologies to be used in the development of large computerised systems using a “correct-by-construction” approach. I was also involved in teaching this to many students around the world. One of the most important aspects of this approach is the mastering of formal proofs by means of some tools. For this reason, I found that it was very important to give students a serious refreshment about proving. After introducing to some background, I found that the best way to continue was to introduce students to some important proofs done in pure mathematics. But I was a bit disappointed with what I found in math textbooks. There are clearly many proofs but I found that mathematicians do not take enough time to explain the way they discover and present such proofs. So, I decided to do it by myself. This is what I call “Mathematical Engineering”: trying to explain in depth what is the approach used in a proof. I also found that this what not too far from what should be done in the formal development of systems. Among the proofs I studied, one is that of a very counterintuitive theorem presented by Reuben Goodstein in 1944. In this seminar, I will present and explain this proof (proved with the Rodin tool set).

Bio

Jean-Raymond Abrial is the co-inventor of various formal method approaches: Z, B and Event-B. He is the author of the “B-book” (CUP 1996), which presents the B-Method. He published another book “Modelling in Event-B: System and Software Engineering” (CUP 2010). He was a guest Professor at ETH Zurich from 2004 to 2007 where he led the team developing the Rodin Platform tool for Event-B (funded by the European Project “Rodin”). After that, he was a researcher also at ETH Zurich, working on a new European Project called “Deploy” till May 2009. More recently, he was a consultant for another European Project: “Advance”. He is also frequently invited in China giving some formal method courses in various Chinese Universities (Peking University in Beijing, East China Normal University in Shanghai). Before being in Zurich, he was a consultant for more than 20 years working in close contact with industrial companies but also with various universities around the world.