学　术

　　本次“学术沙龙”活动人力资源部教师发展中心邀请北京邮电大学郁文生教授与我校师生共同探讨基于Coq的数学定理机器证明问题。具体安排如下，欢迎感兴趣的师生参加。

　　一、主　题：基于Coq的数学定理机器证明

　　二、主讲人：北京邮电大学 郁文生 教授

　　三、时　间：2018年5月23日（周三）8:30-10:30

　　四、地　点：清水河校区主楼A1-407

　　五、主持人：数学科学学院 邵晋梁 副教授

　　六、内容简介：

　　数学定理的机器证明是人工智能基础理论的深刻体现。国际著名的法国布尔巴基学派引进数学结构的概念，基于序、代数和拓扑三大结构统一构建数学。利用交互式定理证明工具Coq，可以构建实现布尔巴某数学的机器证明系统，完成一批基本命题的机器证明，尝试一些公开难题的解答，并将成果应用于程序验证及系统安全性检验等领域。

　　七、主讲人简介：

　　郁文生，教授，1998年毕业于北京大学，获博士学位。1998年至2008年在中科院自动化所，任研究员、博士生导师。2009年至2014年任华东师范大学教授、博士生导师。2014年9月引进至北京邮电大学，任三级教授、博士生导师。任中国系统仿真学会智能物联系统建模与仿真专业委员会副主任委员、中国自动化学会控制理论专业委员会委员、中国人工智能学会智能空天系统专业委员会委员、中国人工智能学会自然计算与数字智能城市专业委员会委员等。在系统鲁棒控制理论、时滞系统稳定性分析及线性系统同时镇定等方面做出一系列创新性成果，在《中国科学》《科学通报》《IEEE Trans.》系列等国内外重要学术刊物发表论文七十余篇，多篇被SCI、EI、ISTP三大权威检索机构收录。曾应邀赴澳大利亚墨尔本大学作高级访问学者。曾多次赴美国、英国、澳大利亚、西班牙、日本及中国香港等国家和地区参加国际性学术会议。2013年获杨嘉墀科技奖。2015年组织北邮学生参加了国际水中机器人竞赛组委会组织的水中机器人比赛，获两项一等奖和一项二等奖，获优秀指导教师奖。2015年获中国仿真学会优秀科技工作者称号。2017年获吴文俊人工智能自然科学奖。目前研究方向为数学定理机器证明、智能信息处理等。

　　八、主办单位：人力资源部教师发展中心

　　　　承办单位：数学科学学院

　　　　　　　　　　　　　　　　　　　人力资源部教师发展中心

　　　　　　　　　　　　　　　　　　　　　2018年5月16日