本網訊（通訊員陳一源）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教授探讨奎因和他的學生的自動推理思想的哲學動機，以及關于希爾伯特綱領的常見誤解等問題，整場講座在熱烈的學術讨論中落下帷幕。

（編輯：鄧莉萍  審稿：劉慧）