本网讯（通讯员陈一源）2023年5月17日晚，加拿大卡尔加里大学教授，逻辑学家、哲学家Richard Zach教授通过学术志平台做了关于“自动推理的史前史”（The Pre-History of Automated Reasoning）的线上讲座，是公司逻辑与哲学系列讲座第46讲。讲座由公司程勇教授主持，公司谢凯博副研究员作与谈人，讲座2小时有余，学术氛围活跃，来自国内外390余名听众参加了Zach教授的讲座。

此讲座是关于自动推理学术史的通识讲座。Zach教授为我们提供了关于自动推理发展史的概述，讨论了诸多证明方法的历史背景和发展，介绍了几种解决方法的起源并做比较；Zach教授不仅向逻辑学家，也向哲学家清晰地描述了在自动推理中的许多著名算法的发展。

在讲座的第一阶段，Zach教授介绍了早期自动定理证明的简史。由20世纪20年代的早期决策方法（希尔伯特(Hilbert),Bernays, Behmann, Schönfinkel, Ackermann,Ramsey）开始，就决策问题的性质而言，证明的唯一工具完全是根据给定值进行的机械计算，没有任何思维活动感觉。如果愿意的话，人们可以谈论机械或机器式思维（也许有一天由机器执行）。然后Zach教授又介绍了1931年Herbrand的理论，1939年希尔伯特和Bernays的方法，1950年奎因(Quine)的《逻辑方法》，1952年Dreben和1955年奎因的基于Herbrand的证明系统，以及1958年Beth、1956年Schütte和1957年Kanger的关于Gentzen系统的变种。

在讲座的第二阶段，Zach教授开始讲解相应技术工作的基本思想。Zach教授介绍了Herbrand关于证明方法的理论，其基本思想是：先将一阶公式转化为前束范式，再借助斯科伦化(Skolemize)方法将前束范式转化为只含前置全称量词和斯科伦项的公式，然后消去全称量词，进行有限组实例代入，就可以得到一种原公式不可满足的判据。以原始公式          为例，化为前束范式为        ，再对其进行斯科伦化，得到          (其中          是斯科伦项)，消除全称量词后得到         ，可以找到它的两组实例              (用          代替        )  和          ，用合取词连接这两个实列，得到          ，显然这是一个矛盾式，是不可满足的，故原公式          也是不可满足的。然后，Zach教授由此就两个问题——如何找到这样的实例以及如何表明它们是命题上不可满足的，进一步讲解后续的发展。在讲座的第三阶段，Zach教授介绍了一些解决方法的起源问题，以及自动定理证明的哲学影响。

在评论与提问环节，与谈人谢凯博副研究员概括了报告人的主体内容，然后提出问题：逻辑学历史中，证明论发展一定程度上由希尔伯特纲领推动，那么希尔伯特纲领对自动定理证明的研究产生了什么样的影响？Zach教授回应称这是一个有趣而又复杂的问题。他认为自动定理研究的重要性并非为何希尔伯特纲领如此重要的主要原因，希尔伯特纲领的重要性在于其产生了导致重大数学发现的数学问题，这些数学发现在哲学意义上也是重要的；但为所有的数学提供一劳永逸的基础，并确保其免于受到悖论和直觉主义变革者布劳威尔(Brouwer)的威胁，并不是希尔伯特纲领的哲学目的。然后，讲座参与者Alexander Steen提问自动推理面临的最大挑战是什么。Zach教授认为不仅在哲学上而且在数学上最吸引人的，与其说是自动推理，不如说是计算机辅助理论改进(computer aided theore improving)和定理验证(theorem verification)，这是挑战所在。

最后，主持人程勇教授和Zach教授探讨奎因和他的员工的自动推理思想的哲学动机，以及关于希尔伯特纲领的常见误解等问题，整场讲座在热烈的学术讨论中落下帷幕。

（编辑：邓莉萍  审稿：刘慧）