1957 年 Logic Theorist：第一個自動證明的偵探#
案件編號：No.1957 — 委託人：羅素與懷特海。偵探：Newell、Simon、Shaw。事務所：RAND，工具：JOHNNIAC。
案發現場#
1955 年的冬天，匹茲堡的暖氣不太管用。Herbert Simon 本是研究人類決策的政治學家，Allen Newell 是數學出身的博士生，Cliff Shaw 是 RAND 公司的程式高手。三人盯著同一個懸案：人類的推理究竟是神秘靈光，還是可以機械模擬的搜尋？
背景並不樂觀。 《數學原理》 用數百頁證明了 \(1 + 1 = 2\) ， 希爾伯特 的夢想已被 哥德爾 擊碎， Herbrand 定理 雖把一階證明歸約為命題窮舉，但組合爆炸讓人絕望。電腦才剛誕生，連高階語言都沒有。
三人接下的委託堪稱狂妄：讓機器重新證明 《數學原理》第二章 的 52 個命題邏輯定理。不是數值計算，而是符號推理。若成功，等於宣告人工智慧元年；若失敗，「思考即計算」不過是空話。
他們沒有 LISP，沒有 SAT 求解器，只有一台 JOHNNIAC 與一個大膽假設：證明就是在狀態空間中找路，而人類靠的是啟發式，不是窮舉。
偵查過程#
Logic Theorist 把每個邏輯公式看作一個案發現場狀態，把推理規則看作可採取的行動。目標是從公理出發抵達定理，或反向從定理回推到公理。
線索一：三條基本偵查手法#
系統只配備三種操作，對應 《數學原理》 的原始規則：
| 規則 | 名稱 | 內容 | 偵探比喻 |
|---|---|---|---|
| 規則一 | 替換規則 | 以任意公式代入命題變元 \(p\) 、 \(q\) ，由 \(A\) 得 \(A[p := B]\) | 換裝偵查，同一招用在不同嫌犯身上 |
| 規則二 | 分離規則 | 即肯定前件，由 \(A\) 與 \(A \to B\) 得 \(B\) | 掌握動機 \(A\) 與因果 \(A \to B\) 即收網 |
| 規則三 | 鏈式規則 | 由 \(A \to B\) 與 \(B \to C\) 得 \(A \to C\) ，另有等值替換版本 | 併案串連，兩條線索接成一條鏈 |
例如公理 \(P1\) 為 \(p \to (q \to p)\) ，公理 \(P2\) 為 \((p \to (q \to r)) \to ((p \to q) \to (p \to r))\) ，公理 \(P3\) 為 \((\lnot p \to \lnot q) \to (q \to p)\) 。所有證明必須由此出發。
線索二：啟發式搜尋，而非窮舉#
若盲目套用三規則，分支因子爆炸。Logic Theorist 的破案關鍵是三種啟發式：
- 目標匹配：先看目標定理 \(G\) 的主 connective。若 \(G\) 形如 \(A \to B\) ，優先找形如 \(X \to B\) 的公理或已證定理，再把證明 \(A \to X\) 設為子目標。
- 工作記憶與子目標堆疊：把「欲證 \(A \to X\) 」壓入堆疊，遞迴求解，類似今日 Prolog 的深度優先。這是人類「先證引理再證定理」習慣的機械化。
- 相似性排序：比較候選公式與目標的符號相似度，優先試長得像的。這招讓它避開大量無用替換。
用現代眼光看，這就是最佳優先搜尋加剪枝。Simon 稱之為「bounded rationality」——理性受限下的聰明辦案。
線索三：定理 2.45 的重演#
以 *2.13 定理 \(p \to \lnot \lnot p\) 的證明為例，機器先鎖定公理 \(P3\) 的後件 \(q \to p\) 與目標後件 \(\lnot \lnot p\) 相似，令 \(p\) 對應 \(\lnot \lnot p\) ，再反推前件 \(\lnot p \to \lnot q\) 需匹配已知定理，最終經兩次替換加一次分離得證。38 個定理一次過關，其中定理 2.85 的機器證明甚至比羅素原版更短，被 Simon 戲稱為「機器比大師更優雅」。
這呼應了 布林 把邏輯代數化、 弗雷格 把證明形式化的百年鋪墊：邏輯既已符號化，搜尋即有可能。
結案報告#
Logic Theorist 在 1956 年達特茅斯會議前夕完成，1957 年正式發表。它證明了 《數學原理》 第二章 52 定理中的 38 個，開啟三個歷史先例：
- AI 元年：它被公認為第一個 AI 程式，Newell 與 Simon 因此提出「物理符號系統假說」——智慧即符號操作，Simon 更在 1975 年獲圖靈獎。
- 啟發式典範：它證明窮舉之外還有聰明搜尋，直接啟發後來的 GPS 通用問題求解器與 1960 年代的 Davis Putnam 程序 。
- 人機對照：它用機器重演人類大師的證明，預告了從 歸結原理 到今日 Lean 與 AI 證明的整條路線。
當然它的局限也很明顯：只會命題邏輯，不懂量詞與 合一 ，沒有 型別 保護，效率全靠手調啟發式。但正如 Simon 所說：「我們解決的不是數學，而是證明人類可以把思考外包。」
事務所的第一案，就此列入 AI 史冊。
證據與工具#
核心資料結構：以串列表示公式，例如 \(p \to q\) 存為 \((IMPLIES \, P \, Q)\) 。IPL 語言首創串列處理，比 LISP 還早兩年。
三規則的形式化寫法：
替換規則：若 \(T\) 為定理， \(p\) 為變元， \(B\) 為任意公式，則 \(T[p := B]\) 亦為定理。
迷你習題：試以 \(P1\) 與分離規則證明 \(A \to A\) 。提示：先將 \(P1\) 中的 \(p\) 換成 \(A\) ， \(q\) 換成合適公式，再套用 \(P2\) 。機器當年就是這樣「試裝」試出來的。
辦案手記補遺：Logic Theorist 每次只往前看一步，若子目標深度超過預設界限即回溯，這正是今日深度限制搜尋的雛形。若把目標 \(G\) 記為 \(A \to B\) ，系統會為每個候選 \(X\) 計算相似分數 \(score(X, G)\) ，分數最高者先試，失敗再試次高者。
它也留下未破的尾巴：含量的詞公式如 \(\forall x \, P(x)\) 完全不在射程內，需等 Herbrand 定理 的基例生成加 DPLL 的命題引擎，再加 歸結與合一 才算真正收網。自然演繹的引入消去結構要到 Gentzen 被 Howard 重新詮釋才與程式合流。
但歷史地位無可動搖：它首次證明「啟發式加符號表示」足以模擬人類定理證明，為 AI 立下開案第一例。
延伸閱讀：Newell Simon 1956 年報告 The Logic Theory Machine 、Feigenbaum 與 Feldman 編《Computers and Thought》。下一案：當啟發式遇上可滿足性難題，Davis 與 Putnam 如何用三條鐵律掃蕩 CNF？請見 Davis Putnam 程序 。