报告主题：人工智能与定理机器证明: 应用软件进行抽象代数定理自动证明的方法
报告人：郁文生教授 (北京邮电大学电子工程学院)
报告时间：2019年9月29日（周日）10:00
报告地点：校本部G507
邀请人：曾振柄教授
报告摘要： 数学定理的机器证明是人工智能基础理论的深刻体现。国际著名的法国Bourbaki学派引进数学结构的概念，基于序、代数、拓扑三大木结构统一构建现代数学。利用交互式定理证明辅助工具COQ，可以构建Bourbaki学派数学的机器证明系统，实现人类和计算机合作学习、理解、构建乃至教育数学的尝试。 Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的（certified）程序。 本报告将以人工智能视角，介绍作者所领导的团队今年在利用COQ辅助证明软件构建和证明抽象代数的工作。相关工作的专著已经由科学出版社近期出版。
欢迎教师、学生参加！