报告题目：浅淡人工智能与自动推理
邀请人：梁治安
报告人：郁文生教授 北京邮电大学
时间：2019年11月22日（周五） 14:00-15:00
地点：红瓦楼723
摘要：数学定理的机器证明是人工智能基础理论的深刻体现。国际著名的法国布尔巴基学派引进数学结构的概念，基于序、代数和拓扑三大结构统一构建数学。利用交互式定理证明工具Coq，可以构建实现布尔巴基数学的机器证明系统，完成一批基本命题的机器证明，尝试一些公开难题的解答，实现研究人员跟随计算机学习、理解、构建乃至教育现代数学的设想，并将成果应用于程序验证及系统安全性检验等领域。