Logic Theorist：首个AI程序
Allen Newell 和 Herbert Simon 创造 Logic Theorist，第一个能证明数学定理的AI程序。
事件概述
1956年，Allen Newell 和 Herbert Simon 在 RAND 公司开发了 Logic Theorist（逻辑理论家），这被认为是第一个人工智能程序。Logic Theorist 能够自动证明 Whitehead 和 Russell《数学原理》中的定理，其证明方法有时比原书更优雅。程序使用启发式搜索来探索可能的证明路径，模拟人类数学家的推理过程。Logic Theorist 在达特茅斯会议上展示，与它同时诞生的是"信息处理语言"（IPL），这是最早的表处理语言之一。
深度学习笔记
背景、原理、影响与要点，一次读懂这个事件
背景与脉络
1955—1956 年，Allen Newell、Herbert Simon 与 J.C. Shaw 在兰德公司（RAND）开发出 Logic Theorist，被广泛称为“第一个人工智能程序”。彼时学界关心“机器能否思考”，三人却另辟蹊径：不造通用心智，而造一个能模仿人类数学家、用启发式搜索证明逻辑定理的程序。他们随手取书架上罗素与怀特海的《数学原理》为靶子——并非想贡献数理逻辑，而是它足够复杂、非数值，能展示机器可在符号领域靠“类人启发式”发现证明。1956 年达特茅斯会议期间，他们首次公开展示，标志 AI 作为实验学科起步。
核心要点
- 1由 Newell、Simon、Shaw 于 1955—1956 年在 RAND 开发，用 IPL 语言编写。
- 2目标是在《数学原理》命题演算中自动证明定理，而非做数值计算。
- 3成功证明第二章 52 条定理中的 38 条，部分证明比原著更新颖。
- 4采用逆向推理的启发式搜索：从目标倒推可达的子目标。
- 51956 年达特茅斯会议展示，被明斯基誉为“首个能工作的人工智能程序”。
- 6论文曾因“重证旧定理无意义”被《符号逻辑杂志》退稿。
原理与技术细节
Logic Theorist 把“证明定理”当作在符号空间里搜索一条从公理到目标的逻辑路径。它不使用穷举，而采用启发式搜索：从待证目标出发，逆向寻找能推出它的子目标与可用规则，逐步把大问题拆成更小的、可立即判定的子问题，直到所有分支都落到已知公理。换句话说，它模拟的是数学家“先想清楚要证什么，再倒推需要什么引理”的策略，而非盲目尝试。程序运行于 IBM 704，核心是对符号列表做逻辑操作与规则推导；它用世界上第一个面向 AI 设计的表处理语言 IPL 编写，而 IPL 也是首个基于列表的编程语言，直接启发了 LISP。
影响与后续
Logic Theorist 确立了“符号 AI”范式：智能 = 对符号结构的搜索与变换。它直接催生了 GPS 通用问题求解器，并影响了 LISP 的表处理设计。在机器定理证明领域其影响有限——王浩 1958 年用 9 分钟证完《数学原理》一阶逻辑全部定理，显示其方法并非最高效。但它的真正遗产是证明“用启发式引导搜索”可行，奠定了专家系统与认知科学的基石，也开创了对“人类如何解题”的计算建模。
学习要点
- 智能不必先有“理解”，能系统地搜索并变换符号即可展现推理。
- 从一个具体任务（证定理）抽象出通用机制，是 AI 工程的常见路径。
- “重证旧定理”被退稿提醒我们：方法的原创性有时比结果新颖更重要。
术语表
用“经验法则”优先探索有希望的路径，避免穷举整个解空间的搜索策略。
首个为 AI 设计的表处理语言，Logic Theorist 即用其编写，是 LISP 的前身。
从待证目标出发，反向寻找能推出它的子目标与规则，直至落到已知公理。