【大讲堂】北京邮电大学郁文生教授|公理化集合论机器证明系统
北京邮电大学郁文生教授将于7月9日下午14：00做客“智慧物联大讲堂“，将为大家带来报告—公理化集合论机器证明系统，敬请期待！
报告人：郁文生
公理化集合论机器证明系统
报告简介：数学定理的机器证明是人工智能基础理论的深刻体现。报告人基于Coq介绍公理化集合论机器证明系统，并给出选择公理与它的几个著名等价命题间等价性的机器证明。国际著名的法国布尔巴基学派引进数学结构的概念，基于序、代数和拓扑三大结构统一构建数学。利用交互式定理证明工具Coq，可以构建实现布尔巴基数学的机器证明系统。利用交互式定理证明工具Coq，报告人给出了Morse-Kelley公理化集合论形式化系统，包括对该体系中8个公理和1个公理图示以及全部181条定义或定理的Coq描述。
腾讯会议ID：702 884 157
https://meeting.tencent.com/s/9odsGoFsIT2B