11月13号下午,中国科学院数学与系统科学研究院博士生导师王定康研究员在K7-310作了题为“参数Groebner基与几何定理的自动证明与发现”的学术报告。本次报告会由kok官网登录页面院长刘修生院长主持,该院全体教师参加了本次学术交流活动。
王定康研究员首先介绍了机器证明的背景, 提到最开始由中国的吴文俊先生创立, 使得证明几何定理的效率大幅度提高。之后又提出了利用不同的工具也可以进行几何定理证明。王定康研究员最后提出了自己的想法,利用参数Groebner基进行几何定理证明。紧接着,通过几个简单的例题实际结合思路,给出了如何刻画几何定理问题,把这些问题转换为相应的含参数的代数问题,最后用机器解决,对应已知的结论完全正确。最后比较了多种算法在相同问题下的计算时间,通过比较可得知王定康研究员提出的算法是最后。王定康研究员还介绍了他们的团队最近几年在机器证明方面取得的最新成果, 同时鼓励在座的年轻老师多交流,定期组织讨论班。 王研究员的讲述深入浅出,思路明确,讲解清晰,开阔了老师们的视野,增进了老师们对机器证明的认识和理解,激发了老师们的研究热情。 讲解结束后,王研究员还与kok官网登录页面教师进行了交流,针对提出的问题,给出了详细的回答,赢得了大家的热烈掌声。(通讯员 于龙 )