解读 · 定义、机制与实例
什么是符号 AI?
人工智能中把知识写成显式符号与规则、再用逻辑和搜索进行推理的那一支。它如何运作、一个带数学的完整例子、它与机器学习的比较、它今天在哪里运行,以及它在哪里失效。
符号 AI(symbolic AI,符号人工智能)是这样一种人工智能方法:它把知识表示为显式的、人可读的符号(对象、关系与规则),并通过逻辑、推理和搜索来操作这些符号,从而得出结论。每一个结论都可以追溯到产生它的事实与规则。它也被称为经典 AI、基于规则的 AI 或 GOFAI。
一个符号 AI 系统由两部分组成:一个用形式语言写成的、由事实与规则构成的知识库,以及一个推理过程,它从已有事实推出新事实,或者搜索一串能够到达目标的步骤。除非另外加入学习组件,它不会从统计中学到任何东西;系统知道的,就是某个人或某个过程写下来的内容。这让符号 AI 精确、可检查、可修正,也正因如此,它的答案会附带一份证明。同样的原因,它在写下的内容之外显得脆弱,填充知识的代价高昂,并且容易陷入组合爆炸。从 20 世纪 50 年代到 80 年代末,符号 AI 主导了这个领域;它从未停止在编译器、求解器、规划器和规则引擎中运行;如今它又作为神经符号系统中负责推理的那一半回归。
1. 精确的定义
当一个系统的知识和推理都由符号承载时,它就是符号 AI。符号是诸如 Parent、ann 或 Ancestor 这样的记号,它们代表世界中的事物,并按照明确的语法组合成更大的表达式。反复出现的要素有四个:
- 含义事先声明的符号。每个符号命名一个对象、一种性质或一种关系。它的含义由构建系统的人确定,而不是从数据中发现。
- 显式的知识。事实与规则用形式语言写成:逻辑、产生式规则、框架、带类型关系的图。每一条知识都是独立的、可读的、可删除的条目。
- 推理。一个通用过程借助肯定前件(modus ponens)或归结(resolution)等推理规则,从已有表达式推出新表达式。无论哪个领域,这个过程都相同;变化的只是知识库。
- 搜索。当单步推理无法回答问题时,系统在由可能步骤(证明、计划、着法)构成的空间中探索,直到找到可行的一条,或穷尽整个空间。
这一思想的经典表述,是艾伦·纽厄尔(Allen Newell)与赫伯特·西蒙(Herbert Simon)的物理符号系统假说,出自他们 1975 年的图灵奖演讲,于 1976 年发表:“物理符号系统具有实现一般智能行为的充分必要手段”[2]。同一篇演讲还提出了启发式搜索假说:符号系统通过生成并逐步修改符号结构、直到得到一个解,来解决问题。这一假说对人类心智是否成立至今仍有争论;而作为一种工程方法,它造就了 1990 年以前的大部分 AI。
GOFAI 这个绰号,即“好的老式人工智能”(Good Old-Fashioned Artificial Intelligence),由哲学家约翰·豪格兰(John Haugeland)在 Artificial Intelligence: The Very Idea(1985)一书中提出 [3]。这种方法也被称为经典 AI、基于逻辑的 AI、基于知识的系统,或者用它在工业中最常见的形态来称呼:基于规则的 AI。它在历史上的对手是联结主义:认为智能涌现自大量简单单元及其经学习得到的数值连接强度,这正是今天神经网络的前身。
2. 符号 AI 如何运作
每个符号系统都要回答两个设计问题:知识如何写下来(知识表示),以及如何从中产生新结论(推理与搜索)?
2.1 知识表示
- 逻辑。命题逻辑陈述或真或假的事实(正在下雨)。一阶逻辑加入了对象、关系和量词(祖先的父母也是祖先)。约翰·麦卡锡(John McCarthy)1959 年的《具有常识的程序》(Programs with Common Sense)常被视为第一个提出把程序的知识表示为逻辑语句、并让程序据此推理的方案 [4]。
- 产生式规则。IF–THEN 形式的规则(如果该菌为革兰氏阴性且呈杆状,那么……)。它是专家系统的主力,也是今天业务规则引擎的主力。
- 框架。马文·明斯基(Marvin Minsky)1974 年的提议:为一种典型情境准备的结构化记录,带有表示其组成部分的槽,以及可被覆盖的默认值 [8]。这一想法预示了编程中的对象与类。
- 语义网络。把概念作为节点、关系作为带标签的边(金丝雀 —是一种→ 鸟),由 M. 罗斯·奎利恩(M. Ross Quillian)于 1968 年引入 AI [9]。
- 本体与描述逻辑。带有类层级与约束的形式化词汇表,推理机可以检查其一致性。W3C 的 OWL 语言以及 SNOMED CT 等临床术语体系都是这样构建的。
- 知识图谱。由海量“主体–关系–客体”事实构成的集合(玛丽·居里 —获奖→ 诺贝尔物理学奖),例如 Wikidata。它们是网络规模的语义网络,通常推理较轻。
2.2 推理
- 前向链接(forward chaining)由数据驱动:从已知事实出发,触发所有条件已满足的规则,加入其结论,如此反复,直到不再出现新事实。产生式系统和业务规则引擎就是这样工作的。
- 反向链接(backward chaining)由目标驱动:从问题出发,寻找能够得出它的规则,把这些规则的条件变成子问题,递归进行,直到每个子问题都是已知事实。Prolog 和 MYCIN 专家系统就是这样工作的。
- 合一(unification)是两者内部的匹配步骤。它寻找一个变量代换,使两个表达式完全相同:把
Ancestor(ann, z)与Ancestor(x, cal)合一,得到{x/ann, z/cal}。J. 艾伦·鲁滨逊(J. Alan Robinson)在 1965 年给出了标准的合一算法 [5]。 - 归结出自同一篇 1965 年论文,它是一条对一阶逻辑反驳完备的推理规则:如果一组子句相互矛盾,反复归结终将推出空子句。要证明一个命题,就加入它的否定,然后搜索这个矛盾。归结是 Prolog 和许多自动定理证明器的基础。
一些扩展处理纯演绎做不到的事:缺省推理与非单调推理(新事实到来时可以撤回的结论),以及不确定性(20 世纪 70 年代 MYCIN 的确定性因子,后来的概率图模型)。
2.3 搜索与规划
许多问题不是一次推理,而是一串选择。符号 AI 把它们表述为在状态空间中的搜索:一次证明搜索、一条路线、一棵国际象棋博弈树、一份排程。启发式搜索(A* 是标准例子)利用对剩余代价的估计,优先探索有希望的状态。带 alpha–beta 剪枝的博弈树搜索用于双人对弈。约束满足与布尔可满足性(SAT)搜索能让所有约束为真的赋值。自动规划搜索一串动作,每个动作都有明确的前提与效果,使初始状态变为目标状态。STRIPS(Fikes 与 Nilsson,1971)确立了多数规划器至今仍在使用的动作格式,如今以规划领域定义语言(PDDL)书写 [10]。
3. 一个完整的例子:规则、肯定前件与不动点
整套方法可以装进一棵家谱树。从两条事实和两条规则开始。
3.1 唯一的推理规则:肯定前件
肯定前件(modus ponens)说:由 与 ,得出 。含变量时,这条规则需要一个经合一求得的代换 。这就是广义肯定前件:
3.2 前向链接直至不动点
前向链接一次性把每条规则应用到已知事实的每一种匹配组合上。把它写成作用于事实集合的算子 :
并在第一个满足 的 处停止,这就是不动点。在家谱树上:
| 轮次 | 规则 | 代换 θ | 新事实 |
|---|---|---|---|
| 1 | R1 | {x/ann, y/bob} | Ancestor(ann, bob) |
| 1 | R1 | {x/bob, y/cal} | Ancestor(bob, cal) |
| 2 | R2 | {x/ann, y/bob, z/cal} | Ancestor(ann, cal) |
| 3 | R1、R2 | 所有匹配都已知 | 无:不动点, |
第 2 轮中,规则 R2 需要 Ancestor(bob, cal),而它在第 1 轮产生之前并不存在。这就是链接的本质:结论变成前提。到第 3 轮,每条规则仍然能匹配,但产出的都是集合中已有的事实,于是过程停止,共得到五条事实。
对家谱树而言,、、:至多 18 条可能的事实,而过程在 5 条时停止。这个定理还说出了统计模型说不出的话:Ancestor(cal, ann) 不在不动点中,所以它不被这个知识库蕴涵。系统并不是认为它“不太可能”,而是没有任何推导,并如实说出这一点。
3.3 同一个答案,反向求得
反向链接提问 Ancestor(ann, cal)?。R1 需要 Parent(ann, cal),这不是事实,于是该分支失败。R2 以 合一,留下两个子目标 Parent(ann, y) 与 Ancestor(y, cal)。第一个由 y = bob 满足;第二个 Ancestor(bob, cal) 由 R1 与 Parent(bob, cal) 推出。结论相同,证明相同,只是从另一端找到。反向链接只触及与问题相关的事实,这正是 Prolog 和诊断型专家系统采用它的原因。
3.4 为什么推导本身就是解释
图 1. Ancestor(ann, cal) 的推导。每个节点要么是给定事实,要么是某条具名规则在给定代换下的结论。
问一个符号系统为什么相信 Ancestor(ann, cal),诚实的回答就是图 1。这棵树不是事后生成的摘要,它就是计算本身。这带来三个实际后果:
- 它可以由别人检查。每一步都只是一条规则的一次应用,所以一个小而独立的检查器就能验证这份证明,而无需信任找到它的那个系统。证明助手正是建立在这种分离之上。
- 它可以在指定之处被质疑。如果
Parent(bob, cal)被证明是错的,你能准确知道哪些结论依赖于它。真值维护系统把这种记账工作自动化。 - 它是忠实的。神经网络的归因方法(显著图、特征重要性)估计哪些输入对某个分数起了作用;它们是对一个本身并非理由的计算的近似。推导则在“系统做了什么”与“系统报告了什么”之间没有任何落差。
4. 符号 AI 与机器学习、神经网络的比较
| 维度 | 符号 AI | 机器学习 / 神经网络 |
|---|---|---|
| 表示 | 显式的符号、规则、图;每一条都可单独阅读 | 分布在模型中的数值参数(权重);没有哪个单独的权重代表一条事实 |
| 知识从何而来 | 由人编写,或从结构化来源编译 | 通过优化拟合样本 |
| 学习 | 并非内置;存在归纳逻辑程序设计等扩展 | 核心机制 |
| 可解释性 | 推导本身就是解释 | 至多是事后近似 |
| 数据需求 | 很少或不需要;一条规则覆盖无穷多情形 | 大规模的有标注或无标注数据集 |
| 杂乱的感知输入(图像、语音、自由文本) | 弱:符号必须由外部提供 | 强 |
| 脆弱性 | 一旦超出写下的内容便骤然失效 | 超出训练分布时性能下降,而且常常悄无声息 |
| 保证 | 可靠性,以及逻辑允许时的完备性 | 统计性的:在相似数据上的期望误差 |
| 当它不知道时 | 没有推导:它可以说“不被蕴涵” | 除非另加弃权机制,否则仍会输出最可能的答案 |
| 改变行为 | 修改一条规则;效果即时且局部 | 重新训练或微调;影响可能扩散 |
| 擅长之处 | 验证、规划、配置、合规,以及对结构化数据的精确推理 | 感知、语言,以及从复杂到无法写成规则的模式中进行预测 |
两者与其说是对手,不如说是互补。神经网络擅长把原始信号变成类别;符号系统擅长在类别已经存在之后,做精确、可检查的工作。长期以来,这种分野被称为符号主义与联结主义之争。今天构建的大多数有意思的系统同时使用两者,而设计上的关键问题是:哪一部分拥有“什么算作真”的决定权。
5. 今天仍在使用的符号 AI 实例
符号 AI 从未消失。它一旦奏效就不再被称为 AI,并在大多数人每天使用却浑然不觉的软件中运行。
- SAT 与 SMT 求解器。判定一个逻辑公式能否被满足的程序。它们源自 Davis–Putnam–Logemann–Loveland 过程(1962)[13];微软研究院的 Z3 等 SMT 求解器又加入了算术、数组和位向量 [14]。它们被用于硬件与软件验证、测试生成和排程。
- 定理证明器与证明助手。Lean、Rocq(2025 年更名前称 Coq)和 Isabelle 用一个小型可信内核检查形式证明的每一步 [15]。它们曾被用来验证一个优化 C 编译器(CompCert,基于 Coq)和一个操作系统微内核(seL4,基于 Isabelle/HOL),并把大量数学形式化。
- 自动规划器。以 PDDL 书写的 STRIPS 式规划器用于物流、制造和航天器运行的排程;NASA 的 Remote Agent 实验于 1999 年在深空一号(Deep Space 1)上运行了星载规划器。
- 编译器与类型检查器。语法分析是由文法驱动的符号操作;OCaml、Haskell 等语言所用的 Hindley–Milner 类型推断,正是用合一求解的,与 §2.2 中的操作相同。
- 规则引擎与业务规则。CLIPS(由 NASA 开发)和 Drools 等产生式规则引擎延续了专家系统的传统,其中许多使用源自查尔斯·福吉(Charles Forgy)Rete 算法(1982)的匹配算法 [11]。凡是决策必须遵循成文政策的地方都常见它们:保险核保、资格审核、税务与合规。
- 知识图谱与本体。Wikidata、搜索引擎的知识图谱,以及 SNOMED CT 和基因本体(Gene Ontology)等生物医学本体,把事实存为带类型的关系,供程序查询和检查。
- 专家系统(历史)。DENDRAL(斯坦福,始于 1965 年)从质谱数据推断分子结构。MYCIN(斯坦福,20 世纪 70 年代)用大约 600 条反向链接规则识别菌血症、脑膜炎等严重感染背后的细菌并推荐抗生素;在评估中其表现与专科医生相当,但从未投入临床使用 [16]。XCON(又称 R1)自 1980 年起为 DEC 的 VAX 计算机订单进行配置,规则最终增至约 2,500 条 [17]。
- 国际象棋引擎。IBM 的深蓝(Deep Blue)在 1997 年击败世界冠军加里·卡斯帕罗夫,依靠的是每秒可达约 2 亿个局面的 alpha–beta 搜索和一个手写的评估函数。Stockfish 至今仍用 alpha–beta 搜索,但自 2020 年起用一个小型神经网络(NNUE)评估局面:这是一种混合体,搜索是其中符号的一半。
6. 长处与局限
6.1 符号 AI 的长处
- 精确。可靠的推理过程绝不会推出前提不支持的结论。推出的事实不存在“86% 正确”这回事。
- 透明、可审计。每条规则都可阅读,每个结论都可追溯(§3.4)。
- 数据高效,靠规则泛化。上面的 R2 适用于任何规模的任何家族,包括从未见过的家族。
- 可编辑。修正一条规则会立即改变行为,且只在该规则适用之处生效,无需重新训练。
- 知道自己不知道什么。没有推导就没有答案,系统可以如实报告,而不是去猜。
6.2 它在哪里失效
- 脆弱性。符号系统只知道被告知的东西。超出其规则一步的情形,会得到没有答案或错误的答案;而普通常识被证明需要数量极其庞大的规则。框架问题(McCarthy 与 Hayes,1969),即如何简洁地说明一个动作发生时哪些东西不变,就是一个著名的例子。
- 知识获取瓶颈。专家往往说不出自己使用的规则。爱德华·费根鲍姆(Edward Feigenbaum)在 1977 年指出,从专家那里提取知识是专家系统的关键瓶颈 [18];庞大的规则库维护起来代价也很高。
- 符号接地。在系统内部,
Parent只是一个与其他记号相关联的记号。是什么把它与真实的父母联系起来?史蒂文·哈纳德(Stevan Harnad)称之为符号接地问题(1990):只由其他符号定义的含义,就像只用一本汉汉词典去学中文 [6]。实践中,接地来自人、传感器或学习得到的感知。 - 组合爆炸。搜索空间随问题规模呈指数增长。1973 年呈交英国科学研究委员会的莱特希尔报告(Lighthill report)把组合爆炸列为核心障碍,并促成了大幅削减经费 [19]。SAT 本身是 NP 完全问题。启发式、子句学习和良好的问题编码让许多实际实例变得很快,但目前没有已知的通用出路。
- 不确定性与噪声。经典逻辑非真即假。真实输入充满噪声,而确定性因子之类的早期修补方案在概率方法成熟之前一直显得随意。
7. 容易混淆的概念
- 符号回归。一种机器学习方法,它在数学表达式的空间中搜索能拟合数据的公式,通常借助遗传编程(例如 Schmidt 与 Lipson 2009 年从实验数据中还原物理定律的工作 [20],或 PySR 库)。它的输出是一个可读的公式,但这个公式是拟合数据得来的,而不是从知识中演绎出来的。它是回归,而不是符号推理。
- 符号计算(计算机代数)。精确操作数学表达式的软件:因式分解、化简、求导、求闭式积分。Macsyma(MIT,始于 20 世纪 60 年代末)、Mathematica(1988)、Maple 和 Python 库 SymPy 都是例子。它与早期 AI 一同成长,共享重写与模式匹配等技术,但目标是精确的数学,而不是对世界进行推理。
- 符号执行。一种程序分析技术:用符号输入而非具体值运行代码,收集每条路径得以执行的条件,并常常交给 SMT 求解器处理。它使用符号 AI 的工具,但它是一种验证方法,而不是 AI 系统。
8. 今天的符号 AI,以及一段简史
当前这一波 AI 是神经网络的;而在其上构建的最强系统,越来越多地依靠符号机制来完成必须精确的部分。大语言模型会把计算器、代码解释器、数据库和求解器当作工具来调用。DeepMind 的 AlphaGeometry(2024)把一个负责提出辅助构造的语言模型与一个负责证明的符号演绎引擎结合,解出了 30 道近年奥赛几何题中的 25 道 [21]。AlphaProof 用 Lean 书写证明,因此每一份被接受的证明都经过证明助手内核的检查。阿图尔·达维拉·加塞兹(Artur d’Avila Garcez)与路易斯·兰姆(Luís Lamb)把这种结合称为 AI 的“第三次浪潮”[7]。这些部件如何组合、又会在哪里出错,是我们神经符号 AI 一页的主题。
用一段话讲完历史:1956 年的达特茅斯研讨会为这个领域命名;纽厄尔、肖(Shaw)与西蒙在同一时期的“逻辑理论家”(Logic Theorist)通过启发式搜索证明了《数学原理》(Principia Mathematica)中的定理。20 世纪 60、70 年代带来了归结、Prolog、框架和规划器;80 年代迎来专家系统的商业热潮,随后是专用硬件市场的崩溃,以及第二次“AI 寒冬”。从 90 年代起统计机器学习领先,2012 年起则是深度学习。带日期的完整故事见符号 AI 的历史。关于符号系统与知识表示的基础理论,见符号系统;关于如何把符号步骤串成确定性流水线,见符号流。
9. 符号 AI 与失效安全模型
失效安全模型是这样一种 AI 模型:当它失败时,失败会把它推向受控的安全状态;证据缺失时它弃权,它的学习可以收窄它的行为,却永远不能扩大它被授权做的事。符号 AI 是构成这种安全状态的天然材料,理由本页前文都已出现:
- “不被蕴涵”是一等公民的答案。§3 的定理让符号层可以说出“这个断言没有推导”,而不是给它附上一个概率。这正是失效安全模型需要的弃权。
- 每一条被接纳的事实都带着理由。一份推导或一条来源引用,让每一次拒绝和每一次接纳都能向人类审查者负责(§3.4)。
- 可靠性为损害设了上限。如果只有符号层能接纳事实,那么一个出错的神经组件可以让系统变慢、变得不那么有用,却不能让它断言知识库不支持的东西。
关键词是决定权。在语言模型旁边加一个规则检查器,并不能让这个组合成为失效安全的,只要模型的输出仍然可以不经检查地到达用户或执行机构。只有当符号层是决定“什么算作真”的那一方时,这个性质才成立:模型可以提议;只有地板能接纳一条事实。这也是一条诚实的局限。符号地板的好坏取决于它的来源和规则;它并不能让系统正确,而是让系统的失败终结于“未知”,而不是一个自信的错误。我们的论文《编排层的鸿沟》论证了为什么链级不变量需要这样一层,而魔方对比用一幅画面展示了其中的差别:一个不可能的魔方被点名拒绝,这是置信度分数无法表达的。
Perslis Research 的 Peel 就是这样构建的。据我们所知,它是第一个失效安全模型(确切的主张与最接近的更早工作,见什么是失效安全模型?)。做决定的回路中没有神经网络;知识是有类型、有来源的卡片;学习是可读的计数。Peel 是研究原型,并非经过认证的安全系统。关于 Perslis 如何使用符号层,更多内容见Perslis 的符号 AI。
每一种技术,一页讲清。从 A* 与 alpha–beta 到 Rete、STRIPS、描述逻辑与 CDCL:符号 AI 技术大全收录 130 多种技术,按十个家族分别详解。
10. 常见问题
- 用简单的话说,什么是符号 AI?
- 符号 AI 是这样一种人工智能:它依据用形式语言写下的显式事实与规则工作,并通过对它们运用逻辑与搜索得出结论。由于每个结论都是从明确陈述的事实与规则一步步推出的,系统能够准确展示它为什么得出这个结论。
- 什么是 GOFAI?
- GOFAI 是 Good Old-Fashioned Artificial Intelligence(好的老式人工智能)的缩写。哲学家约翰·豪格兰在 1985 年的著作 Artificial Intelligence: The Very Idea 中提出这个词,用来指称经典符号 AI:把知识表示为符号、并通过操作符号进行推理的系统。
- ChatGPT 是符号 AI 吗?
- 不是。ChatGPT 和其他大语言模型是在大量文本上训练的神经网络;它们的知识存储在数值权重中,而不是显式规则中。它们可以调用计算器、代码解释器、数据库或求解器等符号工具,把两者结合起来的系统被称为神经符号系统。
- 符号 AI 如今还在使用吗?
- 是的,而且应用广泛,只是常常不以这个名字出现。SAT 与 SMT 求解器、Lean、Rocq 和 Isabelle 等证明助手、自动规划器、编译器与类型检查器、业务规则引擎和知识图谱,都是每天都在使用的符号 AI。
- 符号 AI 与联结主义 AI 有什么区别?
- 符号 AI 把知识表示为显式的符号与规则,并用逻辑推理。联结主义 AI 是今天神经网络背后的传统,它把知识表示为分布在大量简单单元之间、经学习得到的数值连接强度。符号系统精确、可解释,但脆弱;联结主义系统能从数据中学习、能处理带噪声的输入,但提供的保证较弱。
- 符号 AI 可解释吗?
- 可以,这是由其构造决定的。符号系统通过一串规则应用得出结论,而这串应用本身就是解释:它列出了用到的每一条事实与规则,并且可以由独立的检查器验证。解释的质量取决于规则的质量,但它永远不是对系统所做之事的近似。
- 符号 AI 有哪些例子?
- 历史上的例子包括逻辑理论家、DENDRAL、MYCIN 和 XCON。当下的例子包括 Z3 等 SAT 与 SMT 求解器、Lean 等证明助手、PDDL 规划器、CLIPS 与 Drools 等规则引擎、Wikidata 等知识图谱,以及国际象棋引擎中的搜索部分。
- 符号 AI 有哪些局限?
- 它的主要局限是:超出所给知识时的脆弱性、从专家那里获取并维护这些知识的高昂代价、把符号与世界联系起来的符号接地问题,以及搜索中的组合爆炸。它在感知方面也很弱,例如识别图像或语音。
11. 参考文献
- S. Russell, P. Norvig. Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020.
- A. Newell, H. A. Simon. Computer Science as Empirical Inquiry: Symbols and Search. Communications of the ACM 19(3):113–126, 1976. doi:10.1145/360018.360022
- J. Haugeland. Artificial Intelligence: The Very Idea. MIT Press, 1985.
- J. McCarthy. Programs with Common Sense. In Mechanisation of Thought Processes: Proceedings of the Symposium at the National Physical Laboratory (Teddington, 1958). HMSO, London, 1959.
- 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
- S. Harnad. The Symbol Grounding Problem. Physica D 42:335–346, 1990. doi:10.1016/0167-2789(90)90087-6
- A. d’Avila Garcez, L. C. Lamb. Neurosymbolic AI: The 3rd Wave. Artificial Intelligence Review 56(11):12387–12406, 2023. doi:10.1007/s10462-023-10448-w. arXiv:2012.05876
- M. Minsky. A Framework for Representing Knowledge. MIT AI Laboratory Memo 306, 1974.
- M. R. Quillian. Semantic Memory. In M. Minsky (ed.), Semantic Information Processing. MIT Press, 1968.
- 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.
- C. L. Forgy. Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem. Artificial Intelligence 19(1):17–37, 1982.
- M. H. van Emden, R. A. Kowalski. The Semantics of Predicate Logic as a Programming Language. Journal of the ACM 23(4):733–742, 1976.
- 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
- L. de Moura, N. Bjørner. Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963. doi:10.1007/978-3-540-78800-3_24
- L. de Moura, S. Kong, J. Avigad, F. van Doorn, J. von Raumer. The Lean Theorem Prover (System Description). CADE-25, 2015.
- E. H. Shortliffe. Computer-Based Medical Consultations: MYCIN. Elsevier, 1976.
- J. McDermott. R1: A Rule-Based Configurer of Computer Systems. Artificial Intelligence 19(1):39–88, 1982.
- E. A. Feigenbaum. The Art of Artificial Intelligence: Themes and Case Studies of Knowledge Engineering. Proceedings of IJCAI-77, 1977.
- J. Lighthill. Artificial Intelligence: A General Survey. In Artificial Intelligence: a paper symposium. Science Research Council, 1973.
- M. Schmidt, H. Lipson. Distilling Free-Form Natural Laws from Experimental Data. Science 324(5923):81–85, 2009. doi:10.1126/science.1165893
- T. H. Trinh, Y. Wu, Q. V. Le, H. He, T. Luong. Solving Olympiad Geometry without Human Demonstrations. Nature 625:476–482, 2024.