什么是逻辑编程？

逻辑编程是一种编程风格：程序是一组逻辑语句，通常是事实和“如果……那么……”规则，运行程序就是从这些语句出发证明一个查询。Prolog、Datalog 和回答集编程是主要的逻辑编程语言。查询的答案是使查询为真的替换，或事实的集合。

人工智能中的归结是什么？

归结是子句形式逻辑的单一推理规则，由 J. A. Robinson 于 1965 年提出。它从两个含有互补文字的子句出发，在合一这两个文字之后，推出合并其余部分的新子句。一个子句集不可满足，当且仅当归结能推出空子句，因此定理是通过驳倒其否定来证明的。

合一是寻找变元替换、使两个项变得完全相同的过程。例如，p(X, f(Y)) 与 p(a, f(X)) 在 X = a、Y = a 时合一。两个项可以合一时，存在一个最一般合一子。合一是归结、Prolog 和类型推断内部的匹配步骤。

Prolog 现在还有人用吗？

有。SWI-Prolog、SICStus Prolog 和 GNU Prolog 都在持续维护，Prolog 有 ISO 标准，用于基于规则的系统、语法分析、教学和研究。IBM Watson 曾用 Prolog 在句法分析树上做模式匹配。它的思想也延续在用于程序分析的 Datalog 引擎中。

Prolog 和 Datalog 有什么区别？

Datalog 是一种受限的逻辑编程，没有函数符号，从事实出发自底向上求值直到不动点。每个 Datalog 程序都会终止，结果也不依赖规则顺序。Prolog 允许函数符号，是图灵完备的，以深度优先搜索自顶向下运行，所以一个逻辑上正确的 Prolog 程序仍可能死循环。

什么是回答集编程？

回答集编程是一种面向搜索问题的声明式编程，基于 Gelfond 与 Lifschitz（1988）的稳定模型语义。程序用选择规则描述候选解，用约束排除坏的候选；clingo 等求解器返回稳定模型，每个稳定模型就是一个解。

自动定理证明器和证明助手有什么区别？

Vampire 或 E 这样的自动定理证明器独立搜索证明，要么找到，要么放弃。Rocq、Isabelle 或 Lean 这样的证明助手让人交互式地编写证明，由一个小而可信的内核检查每一步。证明助手经常调用自动证明器来处理常规子目标。

计算机能判定任意一阶命题是否为真吗？

不能。Church 和 Turing 在 1936 年证明一阶有效性不可判定。它是半可判定的：证明器终将确认每一个有效命题，但面对无效命题时可能永远运行下去。命题逻辑和 Datalog 等可判定片段以表达力换取了必然终止。

符号 AI 技术 · 逻辑与证明

逻辑编程与定理证明

机器如何证明一件事。归结与合一、SLD 归结与 Prolog、Datalog、回答集编程、Vampire 和 E 等一阶定理证明器，以及 Rocq、Isabelle、HOL、Lean 等证明助手。每一项都讲清是谁、在何时提出，给出算例，说明今天用在哪里、在哪里止步。

Perslis Research · 2026-09-26

逻辑编程是一种编程方式：程序是一组逻辑语句，通常是事实和“如果……那么……”规则，运行程序就是从这些语句出发证明一个查询。自动定理证明是更广的任务：让计算机在形式逻辑中寻找或检查证明。两者都建立在同一条规则之上：带合一的归结。

一段话概述

1965 年，J. A. Robinson 证明：单独一条推理规则，归结，加上他称为合一的匹配过程，就足以驳倒任何不可满足的一阶子句集。逻辑编程把归结限制在 Horn 子句上，把证明搜索当作计算来读：Prolog（马赛，1972 年）、面向数据库的 Datalog、面向搜索问题的回答集编程。自动定理证明器，如 Vampire 和 E，保留完整的一阶逻辑。证明助手，如 Rocq（原名 Coq）、Isabelle 和 Lean，则由人来引导证明，由一个小而可信的内核检查每一步。局限是真实存在的：一阶有效性只是半可判定的，搜索可能爆炸，而一个证明的价值不会超过它所证明的规约。

本页是符号 AI 技术下的一个家族页面，那里汇总了所有主要的符号方法。关于整个领域，见什么是符号 AI？；关于这些思想在更大历史中的位置，见符号 AI 的历史。

1. 作为工具的逻辑：命题逻辑与一阶逻辑

命题逻辑

是什么。命题逻辑用联结词 $\neg$ 、 $\land$ 、 $\lor$ 、 $\to$ 把原子命题（ $p$ 、 $q$ ……）组合成公式。如果某种真假赋值能使公式为真，公式就是可满足的；如果所有赋值都使它为真，它就是有效的。有效性是可判定的：最坏情况下，把真值表的每一行都检查一遍。

怎么用。几乎所有自动推理器都先把公式化成子句形式：若干子句的合取，每个子句是若干文字的析取。蕴涵式 $p \to q$ 变成子句 $\neg p \lor q$ 。命题推理在实践中的后代，即 SAT 与 SMT 求解器，另有专页：约束满足、SAT 与 SMT。

局限。判定可满足性是 NP 完全的（Cook，1971），而且命题逻辑无法谈论个体，也无法说“对所有”。

一阶逻辑

是什么。一阶逻辑加入了指称个体的项（常元如 $ann$ ，变元如 $x$ ，函数符号如 $f (x)$ ）、作用于项的谓词，以及量词 $\forall$ 和 $\exists$ 。它的表达力足以覆盖大部分数学，也足以陈述程序需要的大部分知识。

它保证什么，不保证什么。哥德尔的完全性定理（1930）表明，有效的一阶公式恰好就是可证明的公式，所以一个逐一枚举证明的程序终将确认任何有效公式 [1]。Church 和 Turing 在 1936 年证明，不存在还能总是确认无效公式的程序 [2] [3]。因此一阶有效性是半可判定的：证明器能在每条真定理上成功，但面对非定理时可能永远运行下去。本页的每个系统都要面对这一事实：要么限制逻辑（Datalog、ASP），要么接受搜索可能不终止（Prolog、一阶证明器）。

Herbrand 定理

谁、何时。Jacques Herbrand，1930 年在巴黎大学的博士论文 [4]。这篇论文里已经勾勒出了合一的思想。

定理（Herbrand，子句形式）。一个有限的一阶子句集

S

不可满足，当且仅当

S

中子句的某个有限基例集（把每个变元都替换为不含变元的项所得的实例）作为命题公式集是不可满足的。

为什么重要。这条定理把一阶问题化归为一串命题问题：生成基例，检验，重复。早期证明器正是这样做的。Davis 与 Putnam 1960 年的过程就建立在它之上 [5]，其命题核心经 Davis、Logemann 和 Loveland 在 1962 年改进，至今仍是现代 SAT 求解器的基础。弱点在于盲目实例化：基项有无穷多个，没有好办法猜中正确的那些。归结解决了这个问题。

2. 归结与合一

归结

谁、何时。John Alan Robinson，《A Machine-Oriented Logic Based on the Resolution Principle》，发表于 1965 年的 Journal of the ACM [6]。Robinson 称它“面向机器”，因为它只有一条推理规则，便于计算机反复应用，而不像为人设计的逻辑那样有许多规则。

怎么工作。取两个含有互补文字的子句，合一这两个文字，再把其余部分合并：

\frac{C \lor L D \lor \neg L^{'}}{(C \lor D) σ} 其中 σ = mgu (L, L^{'})

要从前提 $Γ$ 证明目标 $G$ ，就加入 $\neg G$ 的子句，不断归结，直到出现空子句 $□$ 。空子句是矛盾，所以 $Γ \cup {\neg G}$ 不可满足，从而 $Γ ⊨ G$ 。这就是反驳证明。

定理（Robinson 1965：可靠性与反驳完全性）。对子句集

S

，能用归结（配合因子化）从

S

推出空子句，当且仅当

S

不可满足。

算例：一次归结反驳。前提：父母的父母是祖父母；Ann 是 Bill 的父母；Bill 是 Carl 的父母。目标：Ann 是 Carl 的祖父母。化成子句形式，并对目标取否定：

四步完成的反驳。每一步都注明所归结的两个子句及所用的替换，因此整个证明可以机械地检查。
#	子句	依据
1	$\neg P (x, y) \lor \neg P (y, z) \lor G (x, z)$	前提（规则）
2	$P (ann, bill)$	前提
3	$P (bill, carl)$	前提
4	$\neg G (ann, carl)$	目标的否定
5	$\neg P (ann, y) \lor \neg P (y, carl)$	4 与 1 归结， $σ = {x \mapsto ann, z \mapsto carl}$
6	$\neg P (bill, carl)$	5 与 2 归结， $σ = {y \mapsto bill}$
7	$□$	6 与 3 归结：矛盾，故目标成立

今天用在哪里。归结及其能处理等式的后继者叠加演算（superposition calculus），是 Vampire、E 等一阶证明器的核心（§4）。它在 Horn 子句上的限制形式就是 Prolog 的执行模型（§3）。

局限。不加限制的归结产生子句的速度远快于找到空子句的速度，因此实用证明器依赖各种精化（序限制、包含删除）和子句选择启发式。朴素归结处理等式也很糟糕。

合一

是什么。合一就是寻找一个替换，使两个项变得完全相同。Robinson 1965 年的论文给出了第一个通用算法，并证明：只要两个项可以合一，就存在一个最一般合一子（mgu），其他所有合一子都可由它再做替换得到 [6]。

算例。合一 $p (X, f (Y))$ 与 $p (a, f (X))$ 。逐个参数匹配： $X = a$ 给出 ${X \mapsto a}$ ；代入后第二个参数变成 $f (Y)$ 与 $f (a)$ ，于是 $Y \mapsto a$ 。最一般合一子为

σ = {X \mapsto a, Y \mapsto a}, p (X, f (Y)) σ = p (a, f (X)) σ = p (a, f (a))

合一会在函数符号冲突时失败（ $f (X)$ 对 $g (Y)$ ），也会在出现检查（occurs check）时失败： $X$ 不能与 $f (X)$ 合一，因为没有哪个有限项等于包含它自身的项。

效率。Robinson 的算法在对抗性输入上可能耗费指数级的时间和空间。Paterson 与 Wegman（1976，期刊版 1978）给出了线性时间算法 [7]，Martelli 与 Montanari（1982）给出了一个以方程组改写形式表述的高效算法 [8]。

今天用在哪里。每个 Prolog 系统、每个归结证明器、ML 家族语言中的类型推断，以及改写引擎中的模式匹配。一个众所周知的捷径：为了速度，大多数 Prolog 系统默认省略出现检查，这在少数程序中会构造出循环项并得出不可靠的结论。需要时，ISO Prolog 提供 unify_with_occurs_check/2。

3. 逻辑编程：SLD 归结、Prolog、Datalog、ASP

SLD 归结

谁、何时。Robert Kowalski 的《Predicate Logic as Programming Language》（IFIP 大会，斯德哥尔摩，1974）提出了 Horn 子句的过程式读法：规则 A :- B, C. 可以读作“要解 A，先解 B，再解 C” [9]。van Emden 与 Kowalski（1976）给出了与之对应的声明式语义：最小 Herbrand 模型，它是一步推论算子的最小不动点 [10]。这条推理规则的名字 SLD 归结（Selective Linear Definite clause resolution，选择性线性确定子句归结）来自 Maarten van Emden；Apt 与 van Emden（1982）证明了它对确定程序是可靠且完全的 [11]。

怎么工作。目标是一列待证的原子。每一步选出一个原子（Prolog 选最左边的），找一条子句头能与之合一的程序子句，用该子句的体替换这个原子，并把合一子作用于整个目标。空目标即成功；各步替换的复合就是答案。因为每一步都是当前目标与一条输入子句归结，推导是线性的，这正是它运行代价低的原因。

算例：一次 Prolog 推导。程序与查询：

parent(ann, bill).          % 子句 1
parent(bill, carl).         % 子句 2
ancestor(X, Y) :- parent(X, Y).                   % 子句 3
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).   % 子句 4
?- ancestor(ann, carl).

Prolog 执行的 SLD 推导：深度优先、从左到右。子句变元每次使用时都重新改名（X1、Z2……）。
步骤	目标	子句与合一子
0	$\leftarrow ancestor (ann, carl)$	查询
1	$\leftarrow parent (ann, carl)$	子句 3， ${X_{1} \mapsto ann, Y_{1} \mapsto carl}$
–	没有子句头能匹配	失败；回溯到第 0 步
1′	$\leftarrow parent (ann, Z_{2}), ancestor (Z_{2}, carl)$	子句 4， ${X_{2} \mapsto ann, Y_{2} \mapsto carl}$
2	$\leftarrow ancestor (bill, carl)$	子句 1， ${Z_{2} \mapsto bill}$
3	$\leftarrow parent (bill, carl)$	子句 3， ${X_{3} \mapsto bill, Y_{3} \mapsto carl}$
4	$□$	子句 2：空目标，回答 yes

图 1. Prolog 以深度优先方式探索的 SLD 树。失败的分支通过回溯被放弃；成功的分支就是证明。

同一个程序也能回答带变元的问题：?- ancestor(ann, W). 返回 W = bill，回溯后再返回 W = carl。每个答案都是从一条成功分支上读出的替换。

局限。SLD 归结在如下意义上是完全的：每个答案都位于树的某条分支上。但 Prolog 的深度优先搜索可能在到达它之前就掉进一条无穷分支。把递归子句写成 ancestor(X, Y) :- ancestor(X, Z), parent(Z, Y).，上面的查询就永远不会返回：最左边的目标在消耗任何数据之前先调用了自己。逻辑完全相同，搜索却不同。

Prolog

谁、何时。Alain Colmerauer 和 Philippe Roussel，在 Robert Kowalski 的合作下，于艾克斯-马赛大学的人工智能小组完成。初步版本在 1971 年底运行，较定型的版本在 1972 年底完成；名字由 Roussel 取自法语 PROgrammation en LOGique（逻辑编程）[12]。David H. D. Warren 为 DEC-10 Prolog 写的编译器让它变得快速，他在 1983 年提出的抽象指令集，即 Warren 抽象机（WAM），成为实现 Prolog 的标准方式 [13]。ISO 标准是 ISO/IEC 13211-1:1995 [14]。

怎么工作。Prolog 程序是一组 Horn 子句；执行就是 SLD 归结，采用最左目标选择规则，按文本顺序尝试子句，按时间顺序回溯，如上例所示。Prolog 还补上了纯逻辑在编程上缺少的东西：算术、输入输出、用于剪枝搜索的截断（!），以及否定即失败 \+ G：当 G 无法被证明时它成功。Clark（1978）把否定即失败解释为在程序的完备化上推理，即把每个谓词的子句读作“当且仅当” [15]。它在缺省推理中的作用见非单调推理。

今天用在哪里。SWI-Prolog、SICStus 和 GNU Prolog 都在持续维护。Prolog 用于规则密集的应用、语法分析、教学和研究；IBM 的 Watson 问答系统曾用它在句法分析树上做模式匹配。日本的第五代计算机系统计划以逻辑编程为基础，见历史页面。

局限。过程性成分（截断、副作用、子句顺序）意味着 Prolog 程序的行为不能完全由其逻辑描述。否定即失败只有在封闭世界的读法下才是可靠的：无法证明的就当作假，对于不完整的知识，这是一个很强的假设。

Datalog

是什么。Datalog 是为数据库而限制的逻辑编程：没有函数符号，因此可能事实的集合是有限的；规则头中的每个变元都必须出现在规则体中。逻辑与数据库这一领域在 Hervé Gallaire 和 Jack Minker 于 1977 年组织的一次研讨会前后成形；Datalog 这个名字归功于 David Maier。标准综述是 Ceri、Gottlob 与 Tanca（1989）[16]。

怎么工作。Datalog 自底向上求值。从已存储的事实出发，反复应用所有规则推出新事实，直到不再变化。结果是程序的直接推论算子 $T_{P}$ 的最小不动点，也就是 van Emden 与 Kowalski 所说的最小 Herbrand 模型 [10]：

M_{P} = lfp (T_{P}) = ⋃_{n = 0}^{\infty} T_{P}^{n} (\emptyset)

对 ancestor 程序：第 1 轮从 parent 事实推出 ancestor(ann,bill) 和 ancestor(bill,carl)；第 2 轮推出 ancestor(ann,carl)；第 3 轮没有新事实，求值停止。半朴素求值（semi-naive evaluation）只连接上一轮新产生的事实，避免重复推出同样的事实。自底向上的求值在 Prolog 中会死循环的左递归版本上也能终止。

今天用在哪里。程序分析是它在今天最大的用途。Soufflé（Jordan、Scholz 与 Subotić，2016）把 Datalog 编译成并行 C++，运行 Doop 这样的指向分析 [17]；Semmle 的查询语言，即现在 GitHub 的 CodeQL，是一种面向对象的 Datalog 变体。Datomic 以 Datalog 作为查询语言，SQL:1999 也以同样的精神加入了递归查询。

局限。Datalog 有意不是图灵完备的。对固定程序求值，复杂度是数据规模的多项式（P 完全）；若程序也作为输入，问题是 EXPTIME 完全的。否定与聚合需要分层等限制，才能保持唯一的含义。

回答集编程

谁、何时。Michael Gelfond 与 Vladimir Lifschitz 在 1988 年定义了稳定模型 [18]。1999 年，Marek 与 Truszczyński 以及 Niemelä 各自独立地提出，把这种语义下的逻辑程序当作求解搜索问题的一种范式 [19] [20]；回答集编程（ASP）这个名字也始于同一年。

怎么工作。给定候选原子集 $M$ ，构造约简 $P^{M}$ ：删去每条含有否定文字 $not b$ 且 $b \in M$ 的规则，再从其余规则中删去剩下的否定文字。约简不含否定，所以有最小模型 $Cn (P^{M})$ 。

定义（稳定模型，Gelfond 与 Lifschitz 1988）。

M

是

P

的稳定模型（回答集），当且仅当

M = Cn (P^{M})

。

算例。程序 p :- not q. q :- not p. 有两个稳定模型。试 $M = {p}$ ：第二条规则因为 $p$ 在 $M$ 中而被删去，第一条变成事实 p.，其最小模型是 ${p}$ ，等于 $M$ 。由对称性， ${q}$ 也是稳定的； $\emptyset$ 和 ${p, q}$ 则不是。单独一条规则 p :- not p. 根本没有稳定模型。每个稳定模型就是一个解。ASP 正是这样编码搜索问题的：选择规则生成候选，约束排除坏的候选。下面是用 clingo 系统的输入语言写的图的 3 着色：

color(red; green; blue).
{ assign(N, C) : color(C) } = 1 :- node(N).     % 每个节点恰好一种颜色
:- edge(N, M), assign(N, C), assign(M, C).      % 相邻节点颜色不同

今天用在哪里。配置、排程、规划、生物信息学和诊断。主要的求解器是波茨坦大学 Potassco 项目的 clingo，其搜索借鉴了 SAT 求解器的冲突驱动学习 [21]，以及 DLV。

局限。ASP 程序要先接地（grounding），即在所有常元组合上实例化，领域一大，接地就可能爆炸。判定一个正规程序是否有稳定模型是 NP 完全的，所以难的实例依旧难。

4. 自动定理证明器

自动定理证明器：Otter、Vampire、E

是什么。这类程序接收一组一阶公理和一个猜想，在没有人帮助的情况下搜索证明，几乎总是 §2 那种反驳。通常被称为第一个定理证明程序的是 Newell、Shaw 与 Simon 的 Logic Theorist（1956），它证明了《数学原理》第 2 章前 52 条定理中的 38 条。

谁、何时。Otter 及其后继 Prover9 由 William McCune 在阿贡国家实验室编写。McCune 的另一个证明器 EQP 在 1996 年解决了 Robbins 问题，证明每个 Robbins 代数都是布尔代数，这是一个长期悬而未决的问题；搜索用了大约八天 [22]。Vampire 由 Andrei Voronkov 在曼彻斯特大学开始开发，现由一个国际团队开发，多次赢得一年一度的 CADE 自动定理证明系统竞赛（CASC）的主要一阶组别 [23]。E 由 Stephan Schulz 开发，始于慕尼黑工业大学，建立在等式叠加演算之上 [24]。证明器在 TPTP 问题库上相互比较。

怎么工作。现代证明器使用给定子句循环（given-clause loop）：维护一个已处理子句集和一个未处理子句队列；反复选出最有希望的未处理子句，在它与已处理集之间做出所有推理，化简，并丢弃冗余结果。证明器的大部分实力在于子句选择启发式、项索引和冗余消除，而不在演算本身。

今天用在哪里。作为证明助手的后端（Isabelle 的 Sledgehammer 把目标发给 E、Vampire 等证明器，再重放它们找到的证明），以及硬件验证：1994 年奔腾除法错误之后，AMD、Intel 等公司采用定理证明来检查浮点运算。

局限。半可判定性意味着：证明器没有找到证明，就什么也没有证明；超时是家常便饭。成功取决于如何陈述问题以使搜索空间保持很小，以及在大型库中如何选取公理。

5. 交互式证明助手

证明助手：LCF、HOL、Isabelle、Rocq（Coq）、Lean

是什么。在证明助手中，人写下定义、命题和证明，机器检查每一步。自动化填补常规步骤，人提供思路。结果是一个由小程序而不是由审稿人认证的证明。

谁、何时。Robin Milner 的 LCF（斯坦福，1972；Edinburgh LCF，1979）提出了至今大多数系统仍在使用的设计 [25]。定理是一个抽象类型的值，只有推理规则才能创建它，所以任何策略（tactic）无论多复杂，最坏也只是失败，而不能产生假定理。LCF 还为编写这些策略引入了 ML 语言。HOL 家族和 Lawrence Paulson 于 1986 年开始开发的 Isabelle [26] 都源自它。Coq 基于 Thierry Coquand 和 Gérard Huet 的构造演算 [27]，由 INRIA 于 1989 年首次发布；它在 2013 年获得 ACM 软件系统奖，并于 2025 年 3 月随 9.0 版更名为 Rocq Prover。Lean 由 Leonardo de Moura 于 2013 年在微软研究院开始开发 [28]；Lean 4 是一次重新实现，同时也是一门编程语言，于 2021 年发布 [29]。

怎么工作。Rocq 和 Lean 基于依赖类型论，采用 Curry–Howard 对应：命题是类型，证明是该类型的程序，因此检查证明就是类型检查。下面是一行 Lean 4 证明，通过引用一条库引理说明自然数加法满足交换律：

example (a b : Nat) : a + b = b + a := Nat.add_comm a b

Isabelle/HOL 和 HOL Light 使用带 LCF 式内核的经典高阶逻辑；原理相同。

今天用在哪里。大型数学：Georges Gonthier 与 Benjamin Werner 于 2005 年在 Coq 中形式化了四色定理 [30]；Feit–Thompson 奇阶定理的 Coq 证明于 2012 年完成 [31]；Flyspeck 项目于 2014 年在 HOL Light 和 Isabelle 中完成了开普勒猜想的形式证明 [32]；Lean 社区的 mathlib 库收录了大量且不断增长的本科与研究级数学。已验证软件：CompCert C 编译器在 Rocq 中被证明正确，seL4 内核在 Isabelle/HOL 中被证明正确，两者都在形式化验证与程序综合中介绍。还有 AI：2024 年，Google DeepMind 的 AlphaProof 以银牌水平为国际数学奥林匹克题目生成了 Lean 证明，为每个证明作认证的是 Lean 的内核，而不是神经网络。

局限。形式证明代价高昂：大型开发需要若干人年，而证明的用处取决于命题本身。对错误定理的正确证明仍然是错的。信任还依赖内核、逻辑的一致性和硬件，这就是为什么内核要保持很小，有些系统还配有独立的证明检查器。

6. 时间线

逻辑编程与定理证明，1930 至 2025 年。年份为发表或首次发布的年份。
年份	技术或系统	人物
1930	Herbrand 定理；一阶逻辑的完全性	Herbrand；哥德尔
1936	一阶有效性不可判定	Church；Turing
1956	Logic Theorist	Newell、Shaw、Simon
1960	Davis–Putnam 过程	Davis、Putnam
1965	归结与合一	J. A. Robinson
1972	Prolog；Stanford LCF	Colmerauer、Roussel；Milner
1974	Horn 子句的过程式解释	Kowalski
1976	逻辑程序的最小模型语义；线性合一	van Emden、Kowalski；Paterson、Wegman
1977	逻辑与数据库研讨会（Datalog 的源头）	Gallaire、Minker
1978	否定即失败	Clark
1979	Edinburgh LCF	Gordon、Milner、Wadsworth
1982	SLD 归结得名并被证明完全	Apt、van Emden
1983	Warren 抽象机	D. H. D. Warren
1986	Isabelle	Paulson
1988	稳定模型语义；构造演算	Gelfond、Lifschitz；Coquand、Huet
1989	Coq 首次发布	INRIA
1995	ISO Prolog 标准	ISO/IEC
1996	EQP 解决 Robbins 问题	McCune
1999	回答集编程作为范式被提出	Marek、Truszczyński；Niemelä
2005	四色定理在 Coq 中形式化	Gonthier、Werner
2013	Lean 开始开发	de Moura
2014	开普勒猜想获得形式证明（Flyspeck）	Hales 等
2016	Soufflé Datalog 引擎	Jordan、Scholz、Subotić
2021	Lean 4	de Moura、Ullrich
2024	AlphaProof：由 Lean 检查的奥赛证明	Google DeepMind
2025	Coq 更名为 Rocq Prover（9.0）	Rocq 团队

7. 这些技术做不到什么

判定一切。一阶证明器是半判定过程。可判定的片段（命题逻辑、Datalog、有限域上的 ASP、描述逻辑）以放弃表达力换取终止性。
逃离组合爆炸。归结、SLD 搜索、接地和 SAT 都面临指数级的最坏情况。启发式让典型问题变得可解，但改变不了最坏情况。
自己写出知识。一个逻辑程序所知道的，恰好就是它的规则和事实所说的。编写和维护这些规则，就是限制了专家系统的知识获取瓶颈（见专家系统）。
检查规约本身。证明表明一个命题由公理推出。这个命题是否表达了人们真正想要的东西，在逻辑之外。
为符号接地。parent(ann, bill) 为真，只因为它被写在那里；见什么是符号系统？。

当今许多系统把这些技术与学习模型配合使用：神经网络提议证明步骤、引理或候选程序，符号检查器决定接受还是拒绝。这种模式见神经符号 AI。

8. 与失效安全模型的关系

证明助手的设计，是失效安全模型把“提议”与“接纳”分开的最清楚的先例。在 LCF 及其后继者中，策略可以很聪明、依赖启发式，甚至由神经网络编写；这些都不影响可靠性，因为只有一个小内核能够铸出定理。AlphaProof 也是这样：网络负责搜索，Lean 负责判定。失效安全模型把同样的分离用于事实和动作：模型可以提议；只有地板能接纳一条事实。

逻辑编程也说明了这个类比需要小心的地方。Prolog 的否定即失败把“无法证明”变成“为假”。失效安全模型不能这样做：当支持某个断言的证据缺失时，安全的回答是未知或弃权，而不是一个自信的否定。封闭世界推理对于按构造就完整的数据库是正确的；当知识不完整时，它就是一种失效模式。

Perslis Research 的 Peel，据我们所知，是第一个失效安全模型。它的知识是有类型、有来源的卡片，学习是可读的计数，在做决定的环路中没有神经网络。Peel 是研究原型，并非经过认证的安全系统。Perslis 更广泛地如何使用符号方法，见Perslis 的符号 AI；我们的论文 Traversing Data in Symbolic Systems 把类型化关系遍历（与上面的 Datalog 不动点是近亲）当作一种检索原语来研究 [33]。

9. 常见问题

什么是逻辑编程？: 逻辑编程是一种编程风格：程序是一组逻辑语句，通常是事实和“如果……那么……”规则，运行程序就是从这些语句出发证明一个查询。Prolog、Datalog 和回答集编程是主要的逻辑编程语言。查询的答案是使查询为真的替换，或事实的集合。
人工智能中的归结是什么？: 归结是子句形式逻辑的单一推理规则，由 J. A. Robinson 于 1965 年提出。它从两个含有互补文字的子句出发，在合一这两个文字之后，推出合并其余部分的新子句。一个子句集不可满足，当且仅当归结能推出空子句，因此定理是通过驳倒其否定来证明的。
什么是合一？: 合一是寻找变元替换、使两个项变得完全相同的过程。例如，p(X, f(Y)) 与 p(a, f(X)) 在 X = a、Y = a 时合一。两个项可以合一时，存在一个最一般合一子。合一是归结、Prolog 和类型推断内部的匹配步骤。
Prolog 现在还有人用吗？: 有。SWI-Prolog、SICStus Prolog 和 GNU Prolog 都在持续维护，Prolog 有 ISO 标准，用于基于规则的系统、语法分析、教学和研究。IBM Watson 曾用 Prolog 在句法分析树上做模式匹配。它的思想也延续在用于程序分析的 Datalog 引擎中。
Prolog 和 Datalog 有什么区别？: Datalog 是一种受限的逻辑编程，没有函数符号，从事实出发自底向上求值直到不动点。每个 Datalog 程序都会终止，结果也不依赖规则顺序。Prolog 允许函数符号，是图灵完备的，以深度优先搜索自顶向下运行，所以一个逻辑上正确的 Prolog 程序仍可能死循环。
什么是回答集编程？: 回答集编程是一种面向搜索问题的声明式编程，基于 Gelfond 与 Lifschitz（1988）的稳定模型语义。程序用选择规则描述候选解，用约束排除坏的候选；clingo 等求解器返回稳定模型，每个稳定模型就是一个解。
自动定理证明器和证明助手有什么区别？: Vampire 或 E 这样的自动定理证明器独立搜索证明，要么找到，要么放弃。Rocq、Isabelle 或 Lean 这样的证明助手让人交互式地编写证明，由一个小而可信的内核检查每一步。证明助手经常调用自动证明器来处理常规子目标。
计算机能判定任意一阶命题是否为真吗？: 不能。Church 和 Turing 在 1936 年证明一阶有效性不可判定。它是半可判定的：证明器终将确认每一个有效命题，但面对无效命题时可能永远运行下去。命题逻辑和 Datalog 等可判定片段以表达力换取了必然终止。

10. 参考文献

K. Gödel. Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik 37:349–360, 1930.
A. Church. A Note on the Entscheidungsproblem. Journal of Symbolic Logic 1(1):40–41, 1936.
A. M. Turing. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society s2-42:230–265, 1936.
J. Herbrand. Recherches sur la théorie de la démonstration. Doctoral thesis, Université de Paris, 1930.
M. Davis, H. Putnam. A Computing Procedure for Quantification Theory. Journal of the ACM 7(3):201–215, 1960. doi:10.1145/321033.321034.
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.
M. S. Paterson, M. N. Wegman. Linear Unification. Journal of Computer and System Sciences 16(2):158–167, 1978 (conference version STOC 1976). doi:10.1016/0022-0000(78)90043-0.
A. Martelli, U. Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems 4(2):258–282, 1982. doi:10.1145/357162.357169.
R. Kowalski. Predicate Logic as Programming Language. Proceedings of IFIP Congress 74, Stockholm, 569–574. North-Holland, 1974.
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. doi:10.1145/321978.321991.
K. R. Apt, M. H. van Emden. Contributions to the Theory of Logic Programming. Journal of the ACM 29:841–862, 1982.
A. Colmerauer, P. Roussel. The Birth of Prolog. Second ACM SIGPLAN Conference on History of Programming Languages (HOPL-II), 1993. doi:10.1145/154766.155362.
D. H. D. Warren. An Abstract Prolog Instruction Set. Technical Note 309, SRI International, 1983.
ISO/IEC 13211-1:1995. Information technology — Programming languages — Prolog — Part 1: General core.
K. L. Clark. Negation as Failure. In H. Gallaire, J. Minker (eds.), Logic and Data Bases, 293–322. Plenum Press, 1978.
S. Ceri, G. Gottlob, L. Tanca. What You Always Wanted to Know About Datalog (And Never Dared to Ask). IEEE Transactions on Knowledge and Data Engineering 1(1):146–166, 1989.
H. Jordan, B. Scholz, P. Subotić. Soufflé: On Synthesis of Program Analyzers. Computer Aided Verification (CAV), 2016.
M. Gelfond, V. Lifschitz. The Stable Model Semantics for Logic Programming. In R. Kowalski, K. Bowen (eds.), Logic Programming: Proceedings of the Fifth International Conference and Symposium, 1070–1080. MIT Press, 1988.
V. W. Marek, M. Truszczyński. Stable Models and an Alternative Logic Programming Paradigm. In The Logic Programming Paradigm: A 25-Year Perspective, 375–398. Springer, 1999. doi:10.1007/978-3-642-60085-2_17.
I. Niemelä. Logic Programs with Stable Model Semantics as a Constraint Programming Paradigm. Annals of Mathematics and Artificial Intelligence 25(3–4):241–273, 1999. doi:10.1023/A:1018930122475.
M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub. Multi-shot ASP Solving with clingo. Theory and Practice of Logic Programming 19(1):27–82, 2019. doi:10.1017/S1471068418000054.
W. McCune. Solution of the Robbins Problem. Journal of Automated Reasoning 19(3):263–276, 1997. doi:10.1023/A:1005843212881.
L. Kovács, A. Voronkov. First-Order Theorem Proving and Vampire. Computer Aided Verification (CAV 2013), LNCS, 1–35. Springer, 2013. doi:10.1007/978-3-642-39799-8_1.
S. Schulz. E — A Brainiac Theorem Prover. AI Communications 15(2–3):111–126, 2002.
M. J. Gordon, R. Milner, C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation. LNCS, Springer, 1979. doi:10.1007/3-540-09724-4.
L. C. Paulson. Natural Deduction as Higher-Order Resolution. Journal of Logic Programming 3(3):237–258, 1986.
T. Coquand, G. Huet. The Calculus of Constructions. Information and Computation 76(2–3):95–120, 1988.
L. de Moura, S. Kong, J. Avigad, F. van Doorn, J. von Raumer. The Lean Theorem Prover (System Description). CADE-25, LNCS, 378–388. Springer, 2015.
L. de Moura, S. Ullrich. The Lean 4 Theorem Prover and Programming Language. CADE-28, LNCS, 625–635. Springer, 2021.
G. Gonthier. Formal Proof — The Four-Color Theorem. Notices of the American Mathematical Society 55(11):1382–1393, 2008.
G. Gonthier et al. A Machine-Checked Proof of the Odd Order Theorem. Interactive Theorem Proving (ITP 2013), LNCS, 163–179. Springer, 2013.
T. Hales et al. A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi 5, 2017. doi:10.1017/fmp.2017.1.
Perslis Research. Traversing Data in Symbolic Systems: Typed-Relation Traversal as a First-Class Retrieval Primitive. 2026. research.perslis.com/traversal