◈ Perslis

解读 · 技术总览

符号 AI 技术大全：1956 年至今的每一种主要方法

一张表收录 130 多项技术、系统与标志性成果，从归结与 A* 到 Rete 算法、STRIPS、CDCL 与归纳逻辑编程：每一种由谁在何时提出、做什么、今天是否仍在使用。然后是它们所属的十大家族、这些家族如何从 1956 年的奠基思想演化而来，以及遇到什么问题该选哪一种。

Perslis Research · 2026-09-26

符号 AI 技术是让程序用显式符号而非学到的权重进行推理的方法：逻辑与定理证明、搜索、规划、知识表示、基于规则的专家系统、约束与 SAT 求解、非单调推理、认知架构以及符号学习。每一种方法给出的答案，都能一步步追溯到明确陈述的事实与规则。

一段话说清

符号 AI 不是某一个算法，而是七十年间积累起来的一整套工具，其中大部分今天仍在日常使用，只是换了名字：SAT 求解器检查芯片设计，A* 在游戏里规划路径，基于 Rete 算法的规则引擎执行保险条款，证明助手检验数学证明，知识图谱支撑着搜索。本页就是这张地图。总表列出每一种主要技术的年份、提出者与所属家族，并链接到深入讲解它的页面。谱系图展示十大家族如何从 1960 年前已经出现的三种思想生长出来。选用指南把问题与技术对应起来；最后几节如实说明这些技术在哪里失效，以及它们能为失效安全模型提供什么。如果想先弄清符号 AI 本身的定义，请从什么是符号 AI？读起。

1. 什么算是一种符号 AI 技术

支柱页把符号 AI 定义为：把知识表示为显式、人可读的符号，并以逻辑、推理和搜索得出结论的方法。所谓一种技术，就是这种方法内部一项可复用的手段：一种表示法、一种推理过程、一种搜索策略，或一种从数据中学习符号结构的方式。本页采用一个可操作的判据。

定义（符号技术）。一种方法是符号 AI 技术，当且仅当：(i) 它的输入与内部状态是具有明确含义的离散结构，例如公式、规则、图或状态；(ii) 每一步都应用一条人能说出名字的显式规则或算子；(iii) 它的结果可以脱离产生它的程序，依据这些规则独立检验。

按这个判据，一些从数据中学习的方法也算在内，例如决策树与归纳逻辑编程，因为它们学到的东西本身就是可读的符号结构；而结果是一组权重向量的方法不算，即使它们是用符号数据训练的。表中还收录了少数并非过程的结论，例如 Cook–Levin 定理与框架问题，因为它们划定了所有技术工作的边界。有几项技术比 AI 这个领域还古老：Boole 的逻辑（1847）、Frege 的一阶逻辑（1879）与 von Neumann 的极小化极大（1928），在程序开始使用它们时才成为 AI 技术。符号 AI 的历史按时间讲述这段故事；本页按方法组织；其中大多数技术的标准教科书讲解，见 Russell 与 Norvig [1]。

2. 总表：每一种主要技术

下表按时间排序。每项技术都链接到其家族页面中的对应小节，那里有它的工作原理、一个完整示例以及局限。年份是我们能够核实的首次发表或首个可运行系统的时间；若一项技术有两个重要日期（思想与命名，或思想与实用版本），则两者并列。今天仍在使用吗？是一个简短判断：是表示仍在常规生产或研究中使用；已成历史表示其思想延续了下来，但技术本身已很少运行；普通文字表示小众或仅限研究。

按时间排序的符号 AI 技术。来源：§9 的参考文献，以及各行链接到的家族页面。
技术年份提出者家族做什么今天仍在使用吗？
命题逻辑1847George Boole（代数形式）逻辑编程与定理证明真假命题用与、或、非连接；SAT 的语言。是：电路、SAT
一阶逻辑1879Gottlob Frege（《概念文字》）逻辑编程与定理证明加入对象、关系以及“所有”和“存在”两个量词。是：规约、证明器
深度优先搜索19 世纪Charles Pierre Trémaux（走迷宫）搜索算法沿一条路径走到底再回退；内存需求很小。是：随处可见
极小化极大1928John von Neumann；Claude Shannon 于 1950 年用于国际象棋搜索算法在双人博弈树中选择最坏结果最好的一步。是：博弈引擎
Herbrand 定理1930Jacques Herbrand逻辑编程与定理证明把一阶不可满足性归结为有限个基例构成的矛盾集合。是：在证明器内部
产生式系统1943；1972Emil Post（改写规则）；Allen Newell、Herbert Simon（作为认知模型）专家系统针对事实工作记忆触发的“如果–那么”规则。是：规则引擎
广度优先搜索1945；1959Konrad Zuse（1972 年才发表）；Edward F. Moore搜索算法逐层扩展状态；每步代价相同时给出最短路径。是：随处可见
回溯搜索1950 年代由 D. H. Lehmer 命名约束满足、SAT 与 SMT每次做一个选择来扩展部分解，走进死胡同就撤销上一个选择。是：每个求解器内部
状态空间搜索1956Allen Newell、Cliff Shaw、Herbert Simon（逻辑理论家、GPS）搜索算法把问题表示为状态、算子与目标测试；求解就是找一条路径。是：共同框架
α–β 剪枝1956John McCarthy 等人各自独立提出；Donald Knuth、Ronald Moore 于 1975 年分析搜索算法跳过不会改变极小化极大结果的博弈树分支；深蓝（1997）所用的搜索。是：国际象棋引擎
手段–目的分析1957–59Newell、Shaw、Simon（通用问题求解器）搜索算法选用最能缩小当前状态与目标之差的算子。已成历史；思想留在规划器中
程序综合1957Alonzo Church（“Church 问题”）形式化验证与程序综合从逻辑规约自动构造程序或电路的问题。活跃的研究方向
常识推理1958–59John McCarthy（《具有常识的程序》）非单调推理用逻辑写下知识，得出人们习以为常的日常结论的研究纲领。仍是开放的研究目标
一致代价搜索1959Edsger Dijkstra（最短路径）搜索算法优先扩展代价最小的路径；步代价非负时最优。是：路径规划
DPLL1962Martin Davis、George Logemann、Donald Loveland（承自 Davis–Putnam，1960）约束满足、SAT 与 SMT通过选变量、传播单子句与回溯来判定 SAT。是：CDCL 的核心
情境演算1963；1969John McCarthy；1969 年与 Patrick Hayes 合作AI 规划动作的逻辑：每个事实在某个动作序列产生的情境中成立。研究
归结1965J. Alan Robinson逻辑编程与定理证明单一推理规则，对一阶逻辑反驳完备：从被否定的目标推出矛盾。是：Vampire、E、Prolog
合一1965J. Alan Robinson逻辑编程与定理证明求使两个项相同的最一般代换。是：Prolog、类型推断
DENDRAL1965Edward Feigenbaum、Bruce Buchanan、Joshua Lederberg、Carl Djerassi（斯坦福）专家系统根据质谱数据推断分子结构；通常被称为第一个专家系统。已成历史
A* 搜索1968Peter Hart、Nils Nilsson、Bertram Raphael（SRI）搜索算法按 f = g + h 做最佳优先搜索；h 从不高估时返回最优路径。是：游戏、机器人、地图
语义网络1968M. Ross Quillian知识表示概念为节点、关系为带标签的边，并沿“是一种”边继承。是：以知识图谱的形式
Hoare 逻辑1969C. A. R. Hoare形式化验证与程序综合三元组 {P} C {Q}：证明程序把满足 P 的状态变成满足 Q 的状态。是：程序验证器
框架问题1969John McCarthy、Patrick Hayes非单调推理如何说明一个动作不改变什么，而不必逐条列出所有非效果。是问题而非工具，仍在研究
概念依存1969Roger Schank知识表示用少数原语动作表示句子的意义，与措辞无关。已成历史
AQ1969Ryszard Michalski符号机器学习归纳出覆盖正例、排除反例的“如果–那么”规则。基本已成历史
Knuth–Bendix 完备化1970Donald Knuth、Peter Bendix形式化验证与程序综合（成功时）把等式组变成合流的重写系统，从而用重写判定相等。是：等式证明器
项重写1970 年代一个领域而非一篇论文；围绕 Knuth–Bendix 发展形式化验证与程序综合用有向等式不断替换子项，直到没有规则可用。是：编译器、计算机代数
前向链接1970 年代产生式系统传统专家系统数据驱动：触发所有条件成立的规则，直到推不出新东西。是：规则引擎、Datalog
后向链接1970 年代MYCIN 与 Prolog 传统专家系统目标驱动：从问题倒推到事实，把规则条件变成子目标。是：Prolog、规则引擎
Hearsay-II1970 年代Lee Erman、Frederick Hayes-Roth、Victor Lesser、Raj Reddy（卡内基梅隆）认知架构语音理解系统，多个知识源通过黑板协作。已成历史
黑板系统1970 年代Hearsay-II 团队（卡内基梅隆）认知架构相互独立的专家模块在共享数据结构上发布并修订部分假设。小众
STRIPS1971Richard Fikes、Nils Nilsson（SRI）AI 规划动作 = 前提条件 + 添加表 + 删除表；PDDL 背后的表示法。是：通过 PDDL
Cook–Levin 定理1971Stephen Cook；Leonid Levin 独立证明约束满足、SAT 与 SMT证明 SAT 是 NP 完全的：没有已知算法能快速解出所有实例。是定理：划定界限
Prolog1972Alain Colmerauer、Philippe Roussel，基于 Robert Kowalski 的工作逻辑编程与定理证明程序就是 Horn 子句；运行程序就是一次归结证明搜索。是：SWI-Prolog 等
MYCIN1970 年代初Edward Shortliffe，与 Bruce Buchanan、Stanley Cohen（斯坦福）专家系统约 600 条后向链接规则，用于识别细菌并推荐抗生素。已成历史；从未用于临床
Sussman 异常1970 年代初Gerald SussmanAI 规划一个积木世界目标，使逐个解决子目标的规划器失败。测试用例，仍在教学
证明助手1972 年起LCF（Robin Milner）；Isabelle（Lawrence Paulson，1986）；Coq，今名 Rocq（1989）；HOL（Michael Gordon）；Lean（Leonardo de Moura，2013）逻辑编程与定理证明由人引导证明；一个小而可信的内核检查每一步。是：Lean、Rocq、Isabelle
SLD 归结1974Robert Kowalski；由 Maarten van Emden 命名逻辑编程与定理证明针对确定子句的目标导向线性归结；Prolog 内部的过程。是：在 Prolog 内部
框架1974Marvin Minsky知识表示刻板情境的记录结构，含槽、默认值与附加过程。是：通过对象与本体
约束满足问题1974Ugo Montanari（约束网络）约束满足、SAT 与 SMT变量、值域与约束；解就是满足全部约束的赋值。是：排程、配置
偏序规划1975；1977Earl Sacerdoti（NOAH）；Austin Tate（Nonlin）AI 规划只在必要处给步骤排序，用添加次序约束来消解冲突。已大体被取代
HTN 规划1975–77Sacerdoti（NOAH）、Tate（Nonlin）；后有 SHOP（Dana Nau 等，1999）AI 规划用已知方法把高层任务分解为子任务，直到原语动作。是：游戏、机器人
确定性因子1975Edward Shortliffe、Bruce Buchanan（MYCIN）专家系统附在规则上的 −1 到 1 之间的数，按固定公式合成。已被概率方法取代
最弱前置条件1975Edsger Dijkstra形式化验证与程序综合计算保证程序到达目标状态的最弱条件。是：在验证器内部
概念图1976John Sowa知识表示一种图形化的逻辑记法，源自 Peirce 的存在图。小众
主观贝叶斯推理1976Richard Duda、Peter Hart、Nils Nilsson（PROSPECTOR）专家系统用专家为每条规则给出的似然比更新假设的几率。已被贝叶斯网络取代
脚本1977Roger Schank、Robert Abelson知识表示刻板的事件序列（如去餐馆），用来补全没有说出的事实。已成历史
抽象解释1977Patrick Cousot、Radhia Cousot形式化验证与程序综合在可靠的抽象值上“运行”程序，以证明对所有输入都成立的性质。是：静态分析器
时序逻辑1977；1981Amir Pnueli（LTL）；Edmund Clarke、E. Allen Emerson（CTL）形式化验证与程序综合关于程序执行中“总是”“最终”“直到”的逻辑。是：规约
弧相容1977Alan Mackworth（AC-3），承自 David Waltz 与 Ugo Montanari约束满足、SAT 与 SMT删去在某条约束上找不到支撑值的取值。是：约束求解器内部
约束传播1970 年代David Waltz、Ugo Montanari、Alan Mackworth约束满足、SAT 与 SMT反复做局部相容检查，直到值域不再缩小。是：约束编程、SAT、ASP
版本空间1977Tom Mitchell符号机器学习保留与样例一致的最一般假设与最特殊假设。已成历史；仍在教学
知识工程1977Edward Feigenbaum专家系统从专家那里获取知识并编码为规则的实践。是：规则、本体
知识获取瓶颈1977Edward Feigenbaum专家系统发现：从专家那里获取知识是专家系统的决定性成本。仍是核心成本
Datalog1977Hervé Gallaire、Jack Minker（逻辑与数据库）；由 David Maier 命名逻辑编程与定理证明无函数符号的规则，在数据库上自底向上求值；求值总会终止。是：程序分析、数据库
失败即否定1978Keith Clark非单调推理把“无法证明”当作“假”；Prolog 与 Datalog 使用的否定。是：Prolog、ASP
PROSPECTOR1970 年代末Richard Duda、Peter Hart 等（SRI）专家系统矿产勘探顾问；1982 年的论文报道它识别出一处隐藏矿床。已成历史
封闭世界假设1978Raymond Reiter非单调推理凡是推不出来的，都视为假。是：每一次数据库查询
EMYCIN1970 年代末William van Melle（斯坦福）专家系统去掉医学知识的 MYCIN：早期的专家系统外壳。已成历史
真值维护系统1979Jon Doyle非单调推理记录每条信念为何成立，支撑消失时即可撤回。小众
缺省逻辑1980Raymond Reiter非单调推理除非遇到反例否则适用的规则：鸟会飞，除非另有所知。研究；在 ASP 中延续
限定1980John McCarthy非单调推理假定异常情形在已知事实允许的范围内尽可能少。研究
XCON1980John McDermott（卡内基梅隆）为 DEC 开发专家系统用 OPS5 规则配置 VAX 计算机订单；高峰时约 2,500 条规则。已成历史
演绎程序综合1980Zohar Manna、Richard Waldinger形式化验证与程序综合从“所需输出存在”的构造性证明中提取程序。研究；思想见于证明助手
非单调逻辑1980Drew McDermott、Jon Doyle非单调推理加入“是一致的”模态算子，使缺省可以写进逻辑内部。研究
SPIN1980；1991 年起免费Gerard Holzmann（贝尔实验室）形式化验证与程序综合面向并发软件的显式状态模型检测器，性质用 LTL 书写。是：协议
OPS51981Charles Forgy（卡内基梅隆）专家系统使用 Rete 匹配的产生式规则语言；XCON 用它写成。已成历史；后继为 CLIPS
模型检测1981–82Edmund Clarke、E. Allen Emerson；Jean-Pierre Queille、Joseph Sifakis形式化验证与程序综合逐一检查有限模型的每个状态是否满足时序公式，失败时给出反例；工具如 SPIN。是：芯片、协议
Rete 算法1982Charles Forgy专家系统把规则条件编译成缓存部分匹配的网络，只重新匹配发生变化的部分。是：Drools、CLIPS
基于案例的推理1980 年代初；1994Roger Schank、Janet Kolodner；四步循环由 Agnar Aamodt、Enric Plaza 提出符号机器学习检索、复用、修正并保存相似的旧案例，以解决新问题。小众
结构映射1983Dedre Gentner符号机器学习把类比建模为已知领域与新领域之间关系结构的对齐。研究：认知科学
局部搜索1983爬山法；模拟退火由 Scott Kirkpatrick、C. Daniel Gelatt、Mario Vecchi 提出搜索算法只保留一个当前状态并移向更优的邻居，有时接受更差的邻居以跳出局部最优。是：布局、排课
Cyc1984Douglas Lenat（MCC）知识表示人工构建的常识知识库，配有推理引擎。小众
IDA*1985Richard Korf搜索算法以 f 值做迭代加深的 A*；最优，且内存与深度成线性。是：内存受限的搜索
自认知逻辑1985Robert C. Moore非单调推理让推理者从“自己知道自己不知道什么”得出结论。研究
KL-ONE1970 年代末；1985Ronald Brachman；与 James Schmolze 的综述（1985）知识表示带定义概念的结构化继承网络；描述逻辑的前身。已成历史
描述逻辑1980 年代KL-ONE 的后继（1980 年代定名）知识表示用于类层级的一阶逻辑可判定片段；OWL 以之为基础。是：OWL 推理机
CLIPS1985NASA 约翰逊航天中心专家系统用 C 语言写成、使用 Rete 匹配的产生式规则外壳。是：仍在维护
信念修正1985Carlos Alchourrón、Peter Gärdenfors、David Makinson（AGM）非单调推理关于在一致的信念集中合理地增加、删除与修正信念的公设。研究
BB11985Barbara Hayes-Roth认知架构为自身的控制计划另设一块黑板的黑板系统。已成历史
WordNet1985George A. Miller 等（普林斯顿）知识表示把英语单词分成同义词集，并以“是一种”“是部分”等关系相连的词汇数据库。是：自然语言处理
迭代加深1985已用于国际象棋程序；由 Richard Korf 分析搜索算法依次以 0、1、2……为深度上限做受限搜索；在穷举树搜索中渐近最优。是：博弈引擎
基于解释的学习1986Tom Mitchell、Richard Keller、Smadar Kedar-Cabelli；Gerald DeJong、Raymond Mooney符号机器学习证明一个样例为何属于目标概念并保留证明所需条件，从单例泛化。小众
ID31986J. Ross Quinlan符号机器学习按信息增益最大的属性分裂，生长决策树。是：以决策树的形式
ATMS1986Johan de Kleer非单调推理基于假设的 TMS：记录每条信念成立所需的最小假设集。小众：诊断
事件演算1986Robert Kowalski、Marek Sergot非单调推理关于事件如何使性质开始或停止成立的时间逻辑。研究
组块化1986John Laird、Paul Rosenbloom、Allen Newell认知架构Soar 的学习方式：解决僵局的结果被编译成新规则。是：在 Soar 中
耶鲁射击问题1986–87Steve Hanks、Drew McDermott非单调推理表明朴素地“最小化变化”会选出错误的时间演变故事。测试用例，仍在教学
Soar1987John Laird、Allen Newell、Paul Rosenbloom认知架构把一切行为建模为问题空间中的搜索，规则存于长期记忆。研究、仿真
约束逻辑编程1987Joxan Jaffar、Jean-Louis Lassez约束满足、SAT 与 SMT在逻辑编程中用某个域上的约束求解取代合一。是：在 Prolog 系统中
TREAT1987Daniel Miranker专家系统按需重新计算连接、而不存储部分匹配的规则匹配算法。思想见于惰性匹配器
回答集编程1988；1999Michael Gelfond、Vladimir Lifschitz（稳定模型）；1999 年定名逻辑编程与定理证明把问题写成规则，其稳定模型恰好就是问题的解。是：配置、排程
自动定理证明器1980 年代末起Otter（William McCune，阿贡国家实验室）；Vampire（Andrei Voronkov，曼彻斯特）；E（Stephan Schulz）逻辑编程与定理证明无需人工引导地搜索一阶逻辑证明。是：Vampire、E
CN21989Peter Clark、Tim Niblett符号机器学习学习能容忍噪声数据的有序“如果–那么”规则列表。小众
FOIL1990J. Ross Quinlan符号机器学习以信息增益为引导，贪心地学习一阶 Horn 子句。小众
认知导师1980 年代–1995John R. Anderson、Albert Corbett、Kenneth Koedinger 等认知架构按技能的产生式规则模型追踪学生每一步的辅导系统。是：数学辅导
符号模型检测1990Jerry Burch、Edmund Clarke、Kenneth McMillan、David Dill、L. J. Hwang，基于 Randal Bryant 的 BDD（1986）形式化验证与程序综合用二元决策图表示状态集合，可检查超过 10²⁰ 个状态的系统。是：硬件
偏好模型1990Sarit Kraus、Daniel Lehmann、Menachem Magidor非单调推理任何合理的非单调推论关系都应满足的公理（System P）。研究
GSAT 与最小冲突1990；1992Steven Minton 等（最小冲突）；Bart Selman、Hector Levesque、David Mitchell（GSAT）约束满足、SAT 与 SMT每次修改一个变量来减少违反的约束；速度快，但无法证明不可满足。是：大规模排程
归纳逻辑编程1991Stephen Muggleton（命名），承自 Gordon Plotkin 与 Ehud Shapiro符号机器学习从样例加背景知识中学习逻辑程序。研究、科学发现
遗传编程1992John Koza；更早有 Nichael Cramer 的树形表示工作符号机器学习通过选择、交叉与变异来进化程序树。小众
SATPlan1992Henry Kautz、Bart SelmanAI 规划把固定步数的规划问题编码为 SAT 公式。研究；思想仍在使用
符号回归1992；2009John Koza；Michael Schmidt、Hod Lipson符号机器学习搜索拟合数据的公式；输出是一个方程。是：科学研究、PySR
ACT-R1993John R. Anderson（源自 1976 年的 ACT 与 1983 年的 ACT*）认知架构产生式规则加陈述性组块，其激活值可预测人的反应时与错误。研究：认知建模
C4.51993J. Ross Quinlan符号机器学习ID3 的后继：支持数值属性、缺失值与剪枝。是：以决策树的形式
本体1993Tom Gruber（标准定义）知识表示共享、形式化的类、关系与约束词汇。是：SNOMED CT、基因本体
Graphplan1995Avrim Blum、Merrick FurstAI 规划构建带互斥关系的分层规划图，再从后向前搜索。思想留在启发式中
Progol1995Stephen Muggleton符号机器学习以逆蕴涵做 ILP，从最特殊子句出发搜索。小众
抽象论辩1995Phan Minh Dung非单调推理论证加攻击关系；被接受的论证集是能为自己辩护的集合。研究
CDCL1996；2001João Marques-Silva、Karem Sakallah（GRASP）；Matthew Moskewicz 等（Chaff）约束满足、SAT 与 SMT在 DPLL 上加入从每次冲突学习新子句与非时序回跳。是：所有现代 SAT 求解器
深蓝1997Murray Campbell、A. Joseph Hoane Jr.、许峰雄（IBM）搜索算法配有定制国际象棋芯片的大规模并行 α–β 搜索；击败了 Garry Kasparov。已成历史
EPIC1997David Kieras、David Meyer（密歇根大学）认知架构规则可并行触发、并配有精细感知与运动时序的认知架构。研究：人因工程
PDDL1998Drew McDermott 等（为国际规划竞赛而设计）AI 规划规划领域与规划问题的标准语言。是：事实标准
国际规划竞赛1998Drew McDermott 与规划学界AI 规划在共享 PDDL 基准上对规划器进行定期的正面比较。是：定期举办
启发式搜索规划1998–2001Blai Bonet、Héctor Geffner（HSP）；Jörg Hoffmann、Bernhard Nebel（FF）AI 规划由忽略删除表的松弛问题计算出启发值，引导前向搜索。是：主流方法
RDF1999W3C知识表示以网络标识符命名的主–谓–宾三元组事实。是：关联数据、Wikidata
有界模型检测1999Armin Biere、Alessandro Cimatti、Edmund Clarke、Yunshan Zhu形式化验证与程序综合把系统展开 k 步，交给 SAT 求解器寻找该长度内的反例。是：CBMC、硬件
SMT2000 年代源于 Nelson–Oppen（1979）；CVC（斯坦福）；Z3（Leonardo de Moura、Nikolaj Bjørner，2008）约束满足、SAT 与 SMTSAT 加上算术、数组与位向量的判定过程。是：验证、测试
基于 SMT 的验证2000 年代众多工具，如 Dafny（K. Rustan M. Leino，微软研究院）形式化验证与程序综合把程序的正确性条件转成 SMT 查询并自动证明。是：工业验证工具
Aleph2001Ashwin Srinivasan符号机器学习Progol 传统中广泛使用的 ILP 系统。研究
分离逻辑1999–2002John C. Reynolds、Peter O’Hearn、Samin Ishtiaq、Hongseok Yang形式化验证与程序综合把 Hoare 逻辑扩展到指针程序：对堆的一部分的证明可以忽略其余部分。是：静态分析器
OWL2004W3C知识表示基于描述逻辑的网络本体语言；2009 年推出 OWL 2。是：本体
Drools2005Bob McWhirter、Mark Proctor（JBoss，后属 Red Hat）专家系统采用改进版 Rete 匹配的 Java 业务规则引擎。是：业务规则
Fast Downward2006Malte HelmertAI 规划在 PDDL 的多值变量翻译上做启发式搜索的规划器。是：研究界的标准
蒙特卡洛树搜索2006Rémi Coulom（命名）；Levente Kocsis、Csaba Szepesvári（UCT）搜索算法以随机模拟引导博弈树生长；AlphaGo（2016）用神经网络来引导它。是：博弈、规划
CompCert2005–06Xavier Leroy（INRIA）形式化验证与程序综合带有 Coq 机器检验证明（编译保持语义）的优化 C 编译器。是：安全关键代码
seL42009Gerwin Klein 等（NICTA）形式化验证与程序综合其 C 代码在 Isabelle/HOL 中被证明实现了规约的微内核。是
归纳程序综合2011Sumit Gulwani（FlashFill）形式化验证与程序综合从输入–输出样例推断程序。是：Excel 快速填充
知识图谱2012Google 知识图谱；Wikidata知识表示程序可以查询与校验的大规模实体与类型化关系图。是：搜索、数据集成
语法引导综合2013Rajeev Alur 等；承自 Armando Solar-Lezama 的 Sketch（2006）形式化验证与程序综合在用户给定的语法中搜索满足逻辑规约的程序。研究
AlphaGo2016DeepMind（David Silver 等）搜索算法由策略网络与价值网络引导的蒙特卡洛树搜索；以 4–1 击败李世石。混合系统的里程碑
认知通用模型2017John Laird、Christian Lebiere、Paul Rosenbloom认知架构ACT-R、Soar 与 Sigma 共同收敛出的结构：工作记忆、程序性记忆与陈述性记忆。研究

3. 各家族如何从 1956 年演化而来

到 1960 年，三种思想已经摆在桌面上。以逻辑作为表示：McCarthy 的“建议接受者”设想（1958）主张，程序应当把所知道的东西存成形式逻辑语句，并依据能推出的结论行动。启发式搜索：逻辑理论家（1956）借助经验法则从目标倒推，证明了定理；GPS 把这一思想推广为手段–目的分析。人类思维的模型：Newell 与 Simon 把 GPS 当作人类如何解决问题的理论来构建，这条路线后来引出了产生式规则、语义记忆，并最终引出认知架构。本页的每个家族都源自其中一种或几种思想。

符号 AI 技术的十大家族如何从奠基思想演化而来 三个层带。顶层：1956 至 1960 年的三种奠基思想，标为 A 以逻辑作为表示、B 启发式搜索、C 人类思维的模型。中层：编号 1 到 10 的十大技术家族，每个家族用彩色圆点标出它源自哪些奠基思想。底层：今天在用的五类系统，各自列出所依赖的家族。 奠基思想，1956–1960 A. 以逻辑作为表示 建议接受者（McCarthy，1958） B. 启发式搜索 逻辑理论家（1956）、GPS C. 人类思维的模型 GPS：一种问题求解理论 十大技术家族，1960 年代–1990 年代 1 逻辑编程 与定理证明 2 形式化验证 与程序综合 3 搜索算法 4 AI 规划 5 约束满足、 SAT 与 SMT 6 知识表示 7 非单调推理 8 专家系统 9 认知架构 10 符号机器学习 今天的应用 求解器与 验证器 SAT、SMT、 CompCert 来自 1、2、5 证明助手 Lean、Rocq、 Isabelle 来自 1、2 规划器与 博弈搜索 PDDL、A*、MCTS 来自 3、4 规则与知识 Drools、OWL、图谱 来自 6、7、8 神经符号系统 AlphaGo、 AlphaGeometry 来自 1、3、5 圆点表示每个家族源自哪种奠基思想：绿色 A，蓝色 B，棕色 C。

图 1. 符号 AI 技术的谱系。家族编号与 §4 一致。演化是共享的：多数家族源自不止一种奠基思想，今天在用的多数系统也依赖不止一个家族。

这种演化并不是一棵整齐的树。规划把逻辑与搜索结合在一起；约束求解与 SAT 把逻辑问题变成搜索问题，然后让搜索变快；符号学习从逻辑借来假设语言，从搜索借来策略。今天真正在运转的系统往往同时依赖好几个家族：CompCert 是在证明助手中被证明正确的编译器；现代规划器是在逻辑模型上做启发式搜索；而 AlphaGeometry 这样的神经符号系统，则让提出方案的神经网络与负责推演的符号引擎配对工作。

4. 十大家族

下面每个家族都有自己的页面，逐一讲解其中每项技术，并附有完整示例、时间线与参考文献。这里的概述说明该家族解决什么问题、点出它的标志性技术，以及它今天的状况。

4.1 逻辑编程与定理证明

这是最古老的家族，也是其他家族借用最多的一个。它的原材料是命题逻辑与一阶逻辑，被当作工作语言而不是哲学来使用。决定性的一步是 J. Alan Robinson 的归结原理与合一算法（1965）：一条对一阶逻辑反驳完备的推理规则，加上一种让它可以机械执行的匹配操作 [2]。Herbrand 定理（1930）早已表明，这样的搜索在原则上能找到每一个证明。

从归结长出了两条路线。逻辑编程把归结限制在 Horn 子句上，使得运行一个程序就是一次证明搜索：Kowalski 的 SLD 归结 [3]、Prolog（1972）[4]、面向数据库的 Datalog，以及在 Gelfond 与 Lifschitz 提出稳定模型（1988）[5] 之后、用于困难组合问题的回答集编程。定理证明则保留完整的逻辑：Otter、Vampire、E 等自动证明器独立搜索证明；而 LCF 传统中的交互式证明助手，如 Isabelle、HOL、Rocq（原名 Coq）与 Lean，由人来引导，由一个小内核检查每一步。深入了解逻辑编程与定理证明 →

4.2 形式化验证与程序综合

验证要回答的是：一个程序或电路是否对所有输入都符合其规约，而不只是对测试过的那些。Hoare 逻辑（1969）逐条语句地证明程序的性质 [6]。模型检测由 Clarke 与 Emerson、Queille 与 Sifakis 在 1981–82 年各自独立提出，它针对时序逻辑公式遍历有限模型的每一个状态，性质不成立时给出反例 [7] [8]。抽象解释（Cousot 夫妇，1977）在程序取值的可靠近似上计算，从而证明整类错误不会发生 [9]。项重写与 Knuth–Bendix 完备化（1970）提供了底层的等式推理 [10]。

综合则方向相反：从规约得到程序。Manna 与 Waldinger 从构造性证明中提取程序 [11]；归纳综合根据样例推断程序，Sumit Gulwani 的 FlashFill（2011）让它走进了主流 [12]。今天最重要的成果是经过验证的系统：在 Coq 中被证明正确的 C 编译器 CompCert [13]，以及在 Isabelle/HOL 中被证明正确的微内核 seL4 [14]。两者都依赖相邻家族的证明器与 SMT 求解器。深入了解形式化验证与程序综合 →

4.3 搜索算法

几乎每一种符号技术，归根结底都要在状态空间里搜索。无信息的策略，即广度优先、深度优先与一致代价搜索，保证覆盖；启发式搜索则加入对剩余代价的估计。A*（Hart、Nilsson 与 Raphael，1968）总是扩展估计总代价最低的节点 [15]：

f(n)=g(n)+h(n),0≤h(n)≤h*(n)

其中 g(n) 是已花费的代价，h(n) 是估计值。只要 h 从不高估真实的剩余代价 h*，A* 扩展到的第一个目标就是最优的。IDA*（Korf，1985）以与深度成线性的内存给出同样的保证 [16]。博弈加入了对手：极小化极大选择最坏情况最好的一步；α–β 剪枝自 1956 年起被多位研究者各自独立发现，并由 Knuth 与 Moore 在 1975 年加以分析 [17]，它跳过不可能改变结果的分支，是 1997 年深蓝内部的搜索方法。蒙特卡洛树搜索（Coulom；Kocsis 与 Szepesvári，2006）用随机模拟取代了手写的评估函数 [18] [19]，AlphaGo（2016）则用神经网络引导它，使其成为混合系统 [20]。深入了解搜索算法 →

4.4 AI 规划

规划是一种搜索：状态是对世界的逻辑描述，走法是带有前提条件与效果的动作。McCarthy 的情境演算（1963，1969 年与 Hayes 进一步发展）给出了逻辑上的刻画 [21]。STRIPS（Fikes 与 Nilsson，1971）给出了实用的刻画：每个动作有前提表、添加表与删除表，未被删除的一切都假定保持为真，从而绕开了框架问题的大部分 [22]。

后来的规划器改变了搜索的组织方式。偏序规划只在必要时才给步骤定序；HTN 规划用已知的“配方”分解任务；Graphplan（Blum 与 Furst，1995）与 SATPlan（Kautz 与 Selman，1992）把规划编译成分层图或 SAT 公式 [23] [24]。PDDL（1998）为国际规划竞赛统一了输入语言 [25]，而 Fast Downward（Helmert，2006）[26] 这类启发式搜索规划器是今天的标准。深入了解 AI 规划 →

4.5 约束满足、SAT 与 SMT

许多问题最好用约束来表述：一组变量，每个变量有一个可能取值的值域，以及所选取值必须共同满足的约束。

P=⟨X,D,C⟩,求 a:X→⋃D，使对每个 c∈C 都有 a⊨c

Montanari（1974）形式化了约束网络 [27]；回溯搜索、弧相容（Mackworth 的 AC-3，1977）[28] 与约束传播负责剪枝；约束逻辑编程（Jaffar 与 Lassez，1987）把约束求解放进了 Prolog [29]。命题可满足性（SAT）是变量只取真假的特例。Cook（1971）证明它是 NP 完全的 [30]；DPLL（1962）给出了基本算法 [31]；冲突驱动子句学习（GRASP，1996；Chaff，2001）让它能处理规模很大的工业公式 [32] [33]。Z3（2008）[34] 与 cvc5 等 SMT 求解器又加入了算术、数组与位向量理论。它们合起来，大概是工业界用得最多的符号 AI：软硬件验证、排程、测试生成与软件包依赖求解。深入了解约束满足、SAT 与 SMT →

4.6 知识表示

知识表示在任何推理发生之前，就决定了系统能说什么。语义网络（Quillian，1968）把概念放进带“是一种”边的图中 [35]；框架（Minsky，1974）加入了槽与默认值 [36]；概念依存与脚本（Schank；Schank 与 Abelson，1977）表示句子的意义与刻板的事件序列 [37]；概念图（Sowa，1976）为网络赋予了逻辑解读 [38]。

一种语言能表达多少、推理能有多快，这两者之间的权衡后来自成一个领域。KL-ONE [39] 引出了描述逻辑，即一阶逻辑的可判定片段，它成为 OWL 的基础，OWL 自 2004 年起是 W3C 标准。RDF（1999）把事实统一为三元组；Gruber 在 1993 年把本体定义为“对概念化的显式规约”，这成了标准定义 [40]；Cyc（1984）则尝试手工编码常识。知识图谱，从 2012 年的 Google 知识图谱到 Wikidata，是今天大规模的语义网络，通常只做较轻的推理。深入了解知识表示 →

4.7 非单调推理

经典逻辑是单调的：增加前提永远不会让结论消失。

Γ⊢φ⟹Γ∪Δ⊢φ

常识却不是这样。“Tweety 是一只鸟”暗示 Tweety 会飞，直到你得知 Tweety 是企鹅。1980 年，Reiter 的缺省逻辑与 McCarthy 的限定给出了两种形式化回答 [41] [42]；Moore 的自认知逻辑（1985）推理一个主体知道自己不知道什么 [43]；Clark 的失败即否定（1978）则是在 Prolog 与 Datalog 中实际运行的版本 [44]。

真值维护系统（Doyle，1979；de Kleer 的 ATMS，1986）负责记账：记录每条信念为何成立，以便其支撑消失时将其撤回 [45] [46]。框架问题（McCarthy 与 Hayes，1969）与事件演算（Kowalski 与 Sergot，1986）处理随时间发生的变化 [47]。这方面的研究如今大多以回答集编程的形式进行。深入了解非单调推理 →

4.8 专家系统

专家系统拿来产生式规则（“如果条件，那么动作”，源自 Post，后经 Newell 与 Simon 发展），在其中填入专家的知识。DENDRAL（始于 1965）推断分子结构；MYCIN（1970 年代初）用后向链接识别引起感染的细菌，并用确定性因子权衡证据 [48]；PROSPECTOR（SRI，1970 年代末）为矿产勘探提供建议，1982 年的论文报道它识别出一处隐藏矿床 [49]；XCON，又名 R1（1980），为 DEC 配置计算机订单 [50]。EMYCIN、OPS5 与 CLIPS 等外壳把推理引擎与知识分离开来。

工程上的突破是 Forgy 的 Rete 算法（1982）：它缓存部分匹配，使工作记忆的每次变化只需重新匹配受影响的部分 [51]。局限则是 Feigenbaum 在 1977 年指出的知识获取瓶颈 [52]：规则必须靠人工从专家那里挖出来，并且要无限期地维护。Drools、CLIPS 等源自 Rete 的引擎至今仍在运行业务规则、资格审查与合规逻辑。深入了解专家系统 →

4.9 认知架构

认知架构是一组固定的机制，目标是为整个心智建模，而不是解决某一项任务。Hearsay-II 是 1970 年代在卡内基梅隆大学构建的语音理解系统，它引入了“黑板”：相互独立的知识源在一个共享结构上发布并修订假设 [53]。Soar（Laird、Newell 与 Rosenbloom，1987）把一切行为建模为问题空间中的搜索 [54]，并通过组块化学习：每当它解决一个僵局，就把结果编译成一条新规则 [55]。

ACT-R（John R. Anderson；1993 年的 ACT-R 源自 1976 年的 ACT 理论）把产生式规则与陈述性记忆组块结合起来，组块的激活值可以预测人的反应时间与错误 [56]。这些系统今天主要用于认知科学、人因建模与仿真，而不是商业 AI 产品。深入了解认知架构 →

4.10 符号机器学习

符号机器学习学到的模型本身就是符号的：规则、树、逻辑程序、公式。Mitchell 的版本空间（1977）把学习看作在假设空间中的搜索 [57]；Quinlan 的 ID3（1986）与 C4.5（1993）生长决策树 [58]；AQ（Michalski，1969）与 CN2（Clark 与 Niblett，1989）归纳规则。基于解释的学习（1986）借助领域知识解释单个样例，从而由此泛化 [59]。

归纳逻辑编程（Muggleton，1991；代表系统有 FOIL、Progol 与 Aleph）从样例加背景知识中学习 Prolog 子句 [60]。基于案例的推理通过 Aamodt 与 Plaza 的“检索–复用–修正–保存”循环复用旧案例 [61]；结构映射（Gentner，1983）为类比建模 [62]。遗传编程（Koza，1992）与符号回归在程序与公式空间中搜索 [63] [64]。这些学习器的产物可以被阅读和检验；代价是它们难以处理原始感知数据以及嘈杂的高维数据。深入了解符号机器学习 →

5. 什么问题用什么技术

这是一个起点，而不是规则手册。真实的系统往往组合使用好几行；而那些哪一行都不太合适的问题，例如识别图像中的物体，通常交给机器学习，再由某种符号技术检查结果。

问题与符号 AI 技术的对应。每项技术都链接到其讲解。
问题选用理由
有良好距离估计的最短路线或路径A*、IDA*启发式可采纳时最优；内存紧张时用 IDA*。
有良好评估函数的双人博弈α–β 剪枝剪枝有证明保证；经典的国际象棋方法。
没有良好评估函数的博弈或决策蒙特卡洛树搜索用模拟估计价值；很适合与学到的引导结合。
达成目标的动作序列PDDL、Fast Downward与领域无关：模型本身就是规约。
有已知“配方”的任务，如操作规程或任务流程HTN 规划编码专家如何拆分工作；更快，也更容易控制。
排课、排班、产品配置约束满足、约束逻辑编程直接陈述约束，传播尽早剪枝。
大规模布尔问题：电路、软件包依赖、谜题CDCL SAT 求解工业级求解器；可满足赋值很容易检验。
关于整数、实数、数组或位向量的约束SMT在 SAT 之上加入理论；程序验证器的常用后端。
这个设计是否满足某个随时间展开的性质？模型检测、时序逻辑对有限模型穷尽检查；失败时给出反例轨迹。
这个程序是否符合规约？Hoare 逻辑、基于 SMT 的验证、抽象解释完整的正确性证明，或可扩展地证明某类错误不会发生。
必须完全可信的证明证明助手由一个小而可信的内核检查每一步。
在数据库上依据规则推导事实Datalog总会终止；其不动点是完备的，所以不在其中就意味着推不出。
带有默认与例外的选择回答集编程、缺省逻辑非单调规则与组合搜索相结合。
成文政策：资格、定价、合规产生式规则、Rete规则与政策条款一一对应；修改只影响局部。
需要一致性检查的共享词汇OWL、描述逻辑推理可判定；能发现矛盾并对概念分类。
来自多个来源、关于大量实体的事实知识图谱、RDF形式简单的三元组，规模可以非常大。
证据变化时必须能撤回的信念真值维护系统、ATMS为每条信念保留其理由。
从少量样例加背景知识学出可读规则归纳逻辑编程学到人能检查的关系规则。
表格数据上可解释的分类器C4.5、ID3模型是一棵可读的树，由数据拟合。
一组测量数据背后的方程符号回归输出是公式，而不是黑箱。
为人如何完成任务建模ACT-R、Soar预测时间与错误，而不只是结果。

6. 这些技术在哪里失效

同样的四个问题在每个家族中反复出现，也正是因为它们，符号 AI 在感知与语言上输给了机器学习。支柱页对它们有深入讨论；这里说明每个问题落在哪里。

7. 符号技术与失效安全模型

失效安全模型是这样一种 AI 模型：当它失败时，失败会把它推向受控的安全状态；证据缺失时它弃权，它的学习可以收窄它的行为，却永远不能扩大它被授权做的事。总表中的若干技术，恰好提供了这种模型所需的部件。

这些技术单独都不能让系统成为失效安全的。这个性质取决于决定权：是由符号层决定什么算作真、什么可以做，还是它只是向一个可以无视它的模型提建议。模型可以提议；只有地板能接纳一条事实。这些技术也带着各自的局限（§6）。符号地板的好坏取决于它的来源和规则，所以用这些部件构建的失效安全模型，说“未知”的次数会比一个靠猜的模型更多。这正是有意为之的取舍。我们的论文《编排层的鸿沟》与《在符号系统中遍历数据》对此有更详细的论证。

Perslis Research 的 Peel 就是按这一原则构建的。据我们所知，它是第一个失效安全模型；确切的主张与最接近的更早工作，见什么是失效安全模型？做决定的回路中没有神经网络；知识是有类型、有来源的卡片；学习是可读的计数。Peel 是研究原型，并非经过认证的安全系统。Perslis 如何使用符号方法，见Perslis 的符号 AI；关于表示与流水线层面，另见符号系统与符号流两篇解读。

8. 常见问题

主要的符号 AI 技术有哪些？
它们可以分为十大家族：逻辑编程与定理证明、形式化验证与程序综合、搜索算法、AI 规划、约束满足与 SAT 和 SMT 求解、知识表示、非单调推理、专家系统、认知架构，以及符号机器学习。广为人知的具体技术包括归结、Prolog、A*、α–β 剪枝、STRIPS、框架、Rete 算法、DPLL 与 CDCL，以及归纳逻辑编程。
第一种符号 AI 技术是什么？
第一个作为人工智能而构建的程序，是 Allen Newell、Cliff Shaw 与 Herbert Simon 在 1956 年完成的逻辑理论家，它用启发式搜索证明定理；他们的通用问题求解器又引入了手段–目的分析。有些工具比这个领域还古老：命题逻辑可追溯到 1847 年的 George Boole，一阶逻辑可追溯到 1879 年的 Gottlob Frege，极小化极大原理可追溯到 1928 年的 John von Neumann。
哪些符号 AI 技术今天仍在使用？
很多，只是通常不再挂着 AI 的名字。SAT 与 SMT 求解器、模型检测与抽象解释用于验证软硬件；A* 及其后继用于规划路径；α–β 搜索与蒙特卡洛树搜索用于下棋和博弈；PDDL 规划器用于安排作业；Datalog 与回答集编程解决数据库与组合问题；Drools 等基于 Rete 的引擎运行业务规则；OWL 本体与知识图谱组织数据；Lean、Rocq、Isabelle 等证明助手检验数学证明与经过验证的软件。
A* 搜索算是符号 AI 吗？
算。A* 在由具名算子连接的显式离散状态空间中搜索，它的保证本身就是一个证明：只要启发式从不高估剩余代价，A* 扩展到的第一个目标就在最优路径上。它由 Peter Hart、Nils Nilsson 与 Bertram Raphael 在 1968 年发表，至今仍是在游戏、机器人与路线规划中用得最广的符号 AI 技术之一。
SAT 求解器与 SMT 求解器有什么区别？
SAT 求解器判定一个只含真假变量的公式能否被满足。SMT 求解器，即可满足性模理论求解器，对还涉及整数、实数、数组、位向量或其他数据类型的公式做同样的判定，方法是把 SAT 求解器与针对每种理论的专门判定过程结合起来。Z3 与 cvc5 是广泛使用的 SMT 求解器。
前向链接与后向链接有什么区别？
前向链接从已知事实出发，触发所有条件成立的规则并加入结论，直到不再产生新东西；产生式规则引擎就是这样工作的。后向链接从问题出发，倒推到能证明它的事实，把每条规则的条件变成子目标；Prolog 与专家系统 MYCIN 就是这样工作的。
决策树算是符号 AI 吗？
模型本身是符号的：决策树是一组可读的“如果–那么”测试。构建它的方式却是统计的：ID3、C4.5 等算法通过在数据上测量信息增益来选择每一次分裂。这就是为什么决策树、规则归纳与归纳逻辑编程被一起归入符号机器学习。
符号 AI 技术与神经符号 AI 是什么关系？
神经符号系统把神经网络与这里的一种或几种技术结合起来。AlphaGo 用神经网络引导蒙特卡洛树搜索，AlphaGeometry 让语言模型与符号推演引擎配对工作，而调用求解器、数据库或证明检查器的语言模型，则以 SAT、SMT、Datalog 或定理证明作为系统中精确的那一半。

9. 参考文献

  1. S. Russell, P. Norvig. Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020.
  2. J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1):23–41, 1965. doi:10.1145/321250.321253
  3. R. Kowalski. Predicate Logic as Programming Language. Proceedings of IFIP Congress 74, 569–574, 1974.
  4. A. Colmerauer, P. Roussel. The Birth of Prolog. In History of Programming Languages II, ACM, 1996. doi:10.1145/234286.1057820
  5. M. Gelfond, V. Lifschitz. The Stable Model Semantics for Logic Programming. Proceedings of the 5th International Conference and Symposium on Logic Programming, MIT Press, 1070–1080, 1988.
  6. C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10):576–580, 1969.
  7. E. M. Clarke, E. A. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. Logics of Programs Workshop 1981, LNCS 131, Springer, 1982.
  8. J.-P. Queille, J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. International Symposium on Programming, LNCS 137, Springer, 1982.
  9. P. Cousot, R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL 1977, 238–252.
  10. D. E. Knuth, P. B. Bendix. Simple Word Problems in Universal Algebras. In J. Leech (ed.), Computational Problems in Abstract Algebra, Pergamon, 263–297, 1970.
  11. Z. Manna, R. Waldinger. A Deductive Approach to Program Synthesis. ACM Transactions on Programming Languages and Systems 2(1):90–121, 1980.
  12. S. Gulwani. Automating String Processing in Spreadsheets Using Input-Output Examples. POPL 2011. doi:10.1145/1926385.1926423
  13. X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM 52(7):107–115, 2009.
  14. G. Klein et al. seL4: Formal Verification of an OS Kernel. SOSP 2009; extended in ACM Transactions on Computer Systems 32(1), 2014. doi:10.1145/2560537
  15. P. E. Hart, N. J. Nilsson, B. Raphael. A Formal Basis for the Heuristic Determination of Minimum Cost Paths. IEEE Transactions on Systems Science and Cybernetics 4(2):100–107, 1968.
  16. R. E. Korf. Depth-First Iterative-Deepening: An Optimal Admissible Tree Search. Artificial Intelligence 27(1):97–109, 1985.
  17. D. E. Knuth, R. W. Moore. An Analysis of Alpha-Beta Pruning. Artificial Intelligence 6(4):293–326, 1975.
  18. R. Coulom. Efficient Selectivity and Backup Operators in Monte-Carlo Tree Search. Computers and Games 2006, LNCS 4630, Springer, 2007.
  19. L. Kocsis, C. Szepesvári. Bandit Based Monte-Carlo Planning. ECML 2006, LNCS 4212, Springer.
  20. D. Silver et al. Mastering the Game of Go with Deep Neural Networks and Tree Search. Nature 529:484–489, 2016.
  21. J. McCarthy, P. J. Hayes. Some Philosophical Problems from the Standpoint of Artificial Intelligence. In Machine Intelligence 4, Edinburgh University Press, 1969.
  22. R. E. Fikes, N. J. Nilsson. STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artificial Intelligence 2(3–4):189–208, 1971.
  23. A. L. Blum, M. L. Furst. Fast Planning Through Planning Graph Analysis. Artificial Intelligence 90(1–2):281–300, 1997 (IJCAI 1995).
  24. H. Kautz, B. Selman. Planning as Satisfiability. ECAI 1992, 359–363.
  25. D. McDermott et al. PDDL: The Planning Domain Definition Language. Technical report, Yale Center for Computational Vision and Control, 1998.
  26. M. Helmert. The Fast Downward Planning System. Journal of Artificial Intelligence Research 26:191–246, 2006. doi:10.1613/jair.1705
  27. U. Montanari. Networks of Constraints: Fundamental Properties and Applications to Picture Processing. Information Sciences 7:95–132, 1974. doi:10.1016/0020-0255(74)90008-5
  28. A. K. Mackworth. Consistency in Networks of Relations. Artificial Intelligence 8(1):99–118, 1977.
  29. J. Jaffar, J.-L. Lassez. Constraint Logic Programming. POPL 1987, 111–119.
  30. S. A. Cook. The Complexity of Theorem-Proving Procedures. STOC 1971, 151–158.
  31. M. Davis, G. Logemann, D. Loveland. A Machine Program for Theorem-Proving. Communications of the ACM 5(7):394–397, 1962. doi:10.1145/368273.368557
  32. J. P. Marques-Silva, K. A. Sakallah. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48(5):506–521, 1999 (ICCAD 1996).
  33. M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver. DAC 2001. doi:10.1145/378239.379017
  34. L. de Moura, N. Bjørner. Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963. doi:10.1007/978-3-540-78800-3_24
  35. M. R. Quillian. Semantic Memory. In M. Minsky (ed.), Semantic Information Processing, MIT Press, 1968.
  36. M. Minsky. A Framework for Representing Knowledge. MIT AI Laboratory Memo 306, 1974.
  37. R. C. Schank, R. P. Abelson. Scripts, Plans, Goals and Understanding. Lawrence Erlbaum, 1977.
  38. J. F. Sowa. Conceptual Graphs for a Data Base Interface. IBM Journal of Research and Development 20(4):336–357, 1976.
  39. R. J. Brachman, J. G. Schmolze. An Overview of the KL-ONE Knowledge Representation System. Cognitive Science 9(2):171–216, 1985.
  40. T. R. Gruber. A Translation Approach to Portable Ontology Specifications. Knowledge Acquisition 5(2):199–220, 1993.
  41. R. Reiter. A Logic for Default Reasoning. Artificial Intelligence 13(1–2):81–132, 1980.
  42. J. McCarthy. Circumscription: A Form of Non-Monotonic Reasoning. Artificial Intelligence 13(1–2):27–39, 1980.
  43. R. C. Moore. Semantical Considerations on Nonmonotonic Logic. Artificial Intelligence 25(1):75–94, 1985.
  44. K. L. Clark. Negation as Failure. In H. Gallaire, J. Minker (eds.), Logic and Data Bases, Plenum, 293–322, 1978.
  45. J. Doyle. A Truth Maintenance System. Artificial Intelligence 12(3), 1979.
  46. J. de Kleer. An Assumption-Based TMS. Artificial Intelligence 28(2):127–162, 1986.
  47. R. Kowalski, M. Sergot. A Logic-Based Calculus of Events. New Generation Computing 4(1):67–95, 1986.
  48. E. H. Shortliffe, B. G. Buchanan. A Model of Inexact Reasoning in Medicine. Mathematical Biosciences 23(3–4):351–379, 1975.
  49. A. N. Campbell, V. F. Hollister, R. O. Duda, P. E. Hart. Recognition of a Hidden Mineral Deposit by an Artificial Intelligence Program. Science 217(4563):927–929, 1982. doi:10.1126/science.217.4563.927
  50. J. McDermott. R1: A Rule-Based Configurer of Computer Systems. Artificial Intelligence 19(1):39–88, 1982.
  51. C. L. Forgy. Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem. Artificial Intelligence 19(1):17–37, 1982.
  52. E. A. Feigenbaum. The Art of Artificial Intelligence: Themes and Case Studies of Knowledge Engineering. IJCAI 1977.
  53. L. D. Erman, F. Hayes-Roth, V. R. Lesser, D. R. Reddy. The Hearsay-II Speech-Understanding System: Integrating Knowledge to Resolve Uncertainty. ACM Computing Surveys 12(2):213–253, 1980. doi:10.1145/356810.356816
  54. J. E. Laird, A. Newell, P. S. Rosenbloom. SOAR: An Architecture for General Intelligence. Artificial Intelligence 33(1):1–64, 1987. doi:10.1016/0004-3702(87)90050-6
  55. J. E. Laird, P. S. Rosenbloom, A. Newell. Chunking in Soar: The Anatomy of a General Learning Mechanism. Machine Learning 1(1):11–46, 1986.
  56. J. R. Anderson. Rules of the Mind. Lawrence Erlbaum, 1993.
  57. T. M. Mitchell. Generalization as Search. Artificial Intelligence 18(2):203–226, 1982.
  58. J. R. Quinlan. Induction of Decision Trees. Machine Learning 1(1):81–106, 1986.
  59. T. M. Mitchell, R. M. Keller, S. T. Kedar-Cabelli. Explanation-Based Generalization: A Unifying View. Machine Learning 1(1):47–80, 1986.
  60. S. Muggleton. Inductive Logic Programming. New Generation Computing 8(4):295–318, 1991.
  61. A. Aamodt, E. Plaza. Case-Based Reasoning: Foundational Issues, Methodological Variations, and System Approaches. AI Communications 7(1):39–59, 1994.
  62. D. Gentner. Structure-Mapping: A Theoretical Framework for Analogy. Cognitive Science 7(2):155–170, 1983.
  63. J. R. Koza. Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, 1992.
  64. M. Schmidt, H. Lipson. Distilling Free-Form Natural Laws from Experimental Data. Science 324(5923):81–85, 2009.