[数学]自动推理（定理机器证明）研究进展讲座

9月9日14:30，数学学院徐杨教授在X2511会议室举行了自动推理（定理机器证明）研究进展的讲座。数学学院副院长杨晗教授，12、13级辅导员徐海晶老师参加了此次讲座。

首先，徐教授介绍了自动推理的定义，以及一直以来许许多多的数学家为了自动推理的发展所做的贡献，然后仔细讲解了有关“谁是罪犯”的一个案例，并用他们自主研发的程序对其进行了验证。验证过程仅用时1秒左右，这非常直观地向大家展示了自动推理的便捷性。接下来，徐教授又简要阐述了为什么要研究基于逻辑的自动推理，并介绍了自动推理的主要方法：归结原理和Herbrand定理。然后，他对于现在因软件数据错误而导致的重大事故进行了分析，分析结果表明了判断软件可信度的重要性，而他的团队所研发的程序Scavel C正可以用来检验软件是否安全。到现在为止，该程序运行状态良好，在不少领域甚至超过了其他国际知名的证明器。徐教授团队在借鉴并拓展归结原理思想的基础上，建立了一套分离矛盾体的理论，同时还加强了其可靠性与完备性，使得程序在许多领域，尤其是证明数学问题领域中取得了重要的突破。

在听讲座的过程中，同学们都对徐教授团队研发的程序表现出了极大的兴趣，大家都听得十分认真。祝愿徐教授团队能够在该程序的研发中取得更大的成就！