4月19日：Jean-Raymond Abrial: An exercise in mathematical Engineering: Proving weak and strong Goodstein theorems

报告题目:An exercise in mathematical Engineering: Proving weak and strong Goodstein theorems

报告人：Jean-Raymond Abrial 院士/教授

主持人：朱惠彪 教授

报告时间：4月19日（周三）13:30~14：30

报告地点：中北校区数学馆201

报告人简介：

       简-埃蒙德 阿布瑞尔(Jean-Raymond Abrial)，法国计算机科学家，欧洲科学院院士，苏黎世联邦理工学院教授、华东师范大学紫江教授。他是安全攸关软件开发领域的主要奠基人，是将软件形式化方法成功应用于工业界的先驱者。阿布瑞尔教授荣获2015年度上海市国际科技合作奖和2016年度中华人民共和国国际科学技术合作奖。

报告摘要:

       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。