A行业级
Logic Theorist 完成定理证明
早期 AI 用启发式搜索处理符号推理
已核验1可追溯来源
Newell、Simon 与 Shaw 开发 Logic Theorist，让程序通过启发式搜索证明《数学原理》中的命题。
发生了什么
Logic Theorist 把证明过程视为状态空间搜索，用启发式规则减少需要尝试的路径。它证明了书中 52 个命题中的 38 个，其中一个证明比原书更短。
当时的行业背景
早期计算机主要被看作高速算术设备。要让机器处理推理，研究者必须把符号、规则和求解过程表示成可执行步骤。
为什么重要
它给出了“通用问题求解器”的早期样板，也确立了符号表示、搜索和启发式规则这条持续数十年的 AI 路线。
在它之前
计算机程序的代表用途是数值计算。
在它之后
符号推理和启发式搜索成为正式研究对象。
影响
它改变了什么
对行业
证明程序可以处理此前被认为需要人类推理的任务，推动符号 AI 成为早期主流。
来源