题目： 浅谈人工智能与自动推理

　　报告人： 郁文生教授 （北京邮电大学）

　　报告时间： 2021年12月17日周五下午 15：00 – 16：00

　　报告地点：数学院南楼 N205

　　摘要： 数学定理的机器证明是人工智能基础理论的深刻体现。国际著名的法国布尔巴基学派引进数学结构的概念，基于序、代数和拓扑三大结构统一构建数学。利用交互式定理证明工具，可以完整构建布尔巴基数学的机器证明系统。本次讲座回顾人工智能的简要发展历程，介绍数学定理机器证明方法，具体包括基于交互式定理证明工具的公理化集合论及分析基础的形式化实现，充分体现基于Coq 的数学定理机器证明具有可读性和交互性的特点，其证明过程规范、严谨、可靠。在一定意义上，实现读者跟随计算机学习、理解、构建、教育乃至发展现代数学的尝试。