自动推理（四）

为了实现逻辑编程语言的理想，Prolog 必须解决至少两个广泛的问题。逻辑程序由描述真实情况的事实和规则组成；任何不能从程序中证明的东西都被认为是错误的。对于我们之前的示例，flight(toronto, boston) 不正确，因为无法从程序中推导出该文字。在大多数 Prolog 实现中，通过合并运算符 not，进一步利用了对虚假性和不可证明性的识别，该运算符允许程序员在程序中显式表达文字（甚至子条款）的否定。根据定义，如果文字 l 本​​身无法推导，则 not l 会成功。这种被称为“失败否定”的机制一直受到批评。失败否定并没有完全体现否定的标准概念，两者之间存在显着的逻辑差异。标准逻辑，包括霍恩逻辑，是单调的，这意味着通过添加新公理来扩大公理集只会扩大从中推导出来的定理集；然而，失败否定是非单调的，向现有 Prolog 程序添加新的程序子句可能会导致某些目标不再是定理。第二个问题是控制问题。目前，如果程序要达到可接受的效率水平，程序员需要提供相当数量的控制信息。例如，程序员必须注意程序中子句的列出顺序，或者子句中文字的排序方式。未能做好正确的工作可能会导致程序效率低下，或更糟糕的是，程序无法终止。程序员还必须在程序子句中嵌入提示，以防止证明者重新访问搜索空间中的某些路径（通过使用 cut 运算符）或完全修剪它们（通过使用失败）。最后但并非最不重要的一点是，为了提高其效率， Prolog 的许多实现并没有完全实现统一，并且绕过了耗时但关键的测试（所谓的发生检查），该测试负责检查正在计算的统一符的适用性，这会导致不健全的结果。微积分，并且可能导致 Prolog 程序（从计算的角度）包含一个目标，而事实上它不应该（从逻辑的角度来看）。

Prolog 有多种变体旨在扩展其范围。通过实施模型消除过程，Prolog 技术定理证明器 (PTTP)（Stickel 1992）将 Prolog 扩展到完整的一阶逻辑。该实施实现了健全性和完整性。 λProlog (Miller & Nadathur 1988) 超越了一阶逻辑，将语言建立在高阶构造逻辑的基础上。

4.2 SAT 求解器

确定逻辑公式的可满足性问题由于其在工业中的重要适用性而受到自动推理界的广泛关注。如果命题公式的变量的真值赋值使公式成立，则该命题公式是可满足的。例如，赋值 (P← true, Q← true, R← false) 不会使 (P∨R)&∼Q true，但 (P← true, Q← false, R← false) 可以，因此，式可满足。确定一个公式是否可满足称为布尔可满足性问题（简称 SAT），对于有 n 个变量的公式，SAT 可以这样解决：检查 2n 个可能的赋值中的每一个，看看是否至少有一个满足该公式，即使其成立。这个方法显然是完整的：如果原始公式是可满足的，那么我们最终会找到一个这样令人满意的分配；但如果公式是矛盾的（即不可满足的），我们也能够确定这一点。同样清楚的是，特别是在后一种情况下，这种搜索需要指数级的时间，并且构思更有效的算法的愿望是充分合理的，特别是因为许多具有重大实际意义的计算问题，例如图论问题、网络设计、存储和检索、调度、程序优化等（Garey & Johnson 1979）可以表示为 SAT 实例，即表示问题的某些命题公式的 SAT 问题。鉴于 SAT 是 NP 完全的（Cook 1971），它不太可能存在多项式算法；然而，这并不排除针对 SAT 问题的特定情况存在足够有效的算法。

Davis-Putnam-Logemann-Loveland (DPLL) 算法是最早的 SAT 搜索算法之一（Davis & Putnam 1960；Davis, Logemman & Loveland 1962），并且仍然被认为是最好的完整 SAT 求解器之一；当今存在的许多完整的 SAT 程序都可以被视为 DPLL 的优化和推广。本质上，DPLL 搜索过程通过考虑选择分配以使原始公式成立的方式来进行。例如，考虑 CNF 中的公式

P&∼Q&(∼P∨Q∨R)&(P∨∼S)

由于 P 是一个合取词，同时也是一个单位子句，因此如果整个公式要为真，则 P 必须为真。此外，∼P 的值对 ∼P∨Q∨R 的真实性没有贡献，并且无论 S 如何，P∨∼S 都是真实的。因此，整个公式简化为

∼Q&(Q∨R)

类似地，∼Q 必须为真，公式进一步简化为

右

这迫使 R 为真。从这个过程中，我们可以恢复赋值（P← true，Q← false，R← true，S← false），证明原始公式是可满足的。公式可能会导致算法出现分支；当一个子句被认为是假的（一个冲突的子句）时，通过分支的搜索就到达了死胡同，并且到目前为止已经部分构造的赋值的所有变体都可以被丢弃。示例说明：

1 R&(P∨Q)&(∼P∨Q)&(∼P∨∼Q) 给定

2 (P∨Q)&(∼P∨Q)&(∼P∨∼Q) 通过让 R← true

3 Q&∼Q 通过让 P← true

4 ?冲突：Q 和 ∼Q 不能同时为真

5 (P∨Q)&(∼P∨Q)&(∼P∨∼Q) 回溯到(2)：R← true 仍然成立

6 ∼P 通过让 Q← true

7 true 通过让 ∼P 为 true，即 P← false

因此，该公式可满足(P←假，Q←真，R←真)的存在。 DPLL 算法通过术语索引（以有利的方式对公式变量进行排序）、时间回溯（如果过程导致冲突子句，则撤消到前一个分支点的工作）和冲突驱动学习等策略来提高效率。确定要保留的信息以及回溯的位置）。这些策略的组合导致搜索空间的大量修剪；对于更广泛的讨论，感兴趣的读者可以参阅Zhang & Malik 2002。

快速后包络计算揭示了 SAT 类型问题（算法）的惊人计算时间，这些问题由仅包含 60 个变量的公式表示。也就是说：一个由 10 个变量的布尔公式表示的问题，如果公式分别有 40 个和 60 个变量，则只需百分之四秒和百分之六秒即可完成。与此形成鲜明对比的是，如果问题的解决方案是指数级的（比如 2n），那么完成 10、40 和 60 个变量的工作的时间将分别是千分之一秒、13 天和 365 个世纪。它真实地证明了自动推理社区的独创性和当前基于 SAT 的搜索算法的力量，可以以合理的效率处理具有数千个变量的现实世界问题。 Küchlin & Sinz 2000 讨论了工业汽车产品数据管理领域的 SAT 应用程序，其中使用 18,000 个（基本）布尔公式和 17,000 个变量来表达对客户订单的约束。作为另一个例子，Massacci & Marraro 2000 讨论了逻辑密码分析中的应用，即验证表示为 SAT 问题的密码算法的属性。他们演示了通过加密攻击查找密钥与查找布尔公式的模型（赋值）有何相似之处；他们的应用程序中的公式对美国数据加密标准 (DES) 的商业版本进行编码，该编码需要 60,000 个子句和 10,000 个变量。

尽管 SAT 在概念上非常简单，但其内在本质还没有被很好地理解——没有可以普遍应用的标准来回答为什么一个 SAT 问题比另一个问题更难。因此，在某些 SAT 实例上表现良好的算法在其他实例上表现不佳就不足为奇了，人们正在努力设计混合算法解决方案，结合互补方法的优势 - 参见 Prasad、Biere 和 Gupta 2005 年，该混合方法在硬件设计验证中的应用。

SAT 混合策略的最新进展与超级计算能力相结合，使得由三名计算科学家组成的团队能够解决布尔毕达哥拉斯三元组问题，这是拉姆齐理论中一个长期悬而未决的问题：集合 {1,2,...} 可以自然数字被分成两部分，没有部分包含三元组（a，b，c），使得a2+b2=c2？ Heule, Kullmann & Marek 2016 通过证明集合 {1,2,…,n} 可以在 n=7824 时进行划分，但在 n≥7825 时这是不可能的，从而证明了这是不可能的。将这个看似简单的问题表达为 SAT 问题需要接近 38,000 个子句和 13,000 个变量，其中大约一半表示当 n = 7824 时问题可满足，另一半表示当 n = 7825 时问题不可满足；在两者中，证明后者更具挑战性，因为它需要不可满足性的证明，即不存在这样的划分。考虑所有 27825 个可能的两部分分区的朴素暴力方法显然是不可能的，并且通过在基于 SAT 的多阶段框架中使用“聪明”算法来解决该问题，该框架用于解决组合数学中的难题，该框架由五个组成阶段：编码（将问题编码为 SAT 公式）、变换（使用子句消除和对称性破缺技术优化编码）、拆分（使用拆分将问题有效地划分为子问题）启发式）、解决（使用快速处理来搜索令人满意的作业或缺少作业）和验证（验证早期阶段的结果）。特别重要的是立方体与征服的应用，这是一种混合 SAT 策略，对于解决困难组合问题特别有效。该策略将前瞻与冲突驱动子句学习（CDCL）相结合，前者旨在使用全局启发式构建小型二叉搜索树，后者旨在使用局部启发式找到简短的反驳。

将问题拆分为 106 个硬子问题（称为“立方体”）后，将这些子问题交给 Stampede 超级计算机上并行工作的 800 个核心，经过 2 天的进一步拆分和 CDCL 子句处理，解决了问题并交付了验证工作的 200 TB 证据。在当之无愧地庆祝自动推理的这一重大成就，并在欣赏了增强型 SAT 方法所能提供的所有新应用（特别是在硬件和软件验证领域）之后，我们应该问一些对数学家特别重要的问题：是否有一种更有洞察力的方法来建立这个结果，涉及更传统和智力上令人满意的数学证明方法？或者，就增加我们对给定领域（在本例中为组合学）的理解而言，当没有人可以检查证明并因此无法从中获得见解时，解决问题的价值是什么？甚至负责结果的团队也承认，“从人类的角度来看，来自 SAT 求解器的不可满足性证明是一大堆随机信息（不涉及直接理解）”。猜想已经解决，但我们基本上不知道是什么让 7825 如此特别。也许从这些考虑中得出的真正价值在于，它们引导我们思考更深层次的问题：特定问题的结构是什么，使其适合标准数学处理，而不是需要无意识的暴力方法？ 在思考这个问题的同时，SAT 可能提供解决某些数学问题的最佳途径。

DPLL 搜索过程已扩展到量化逻辑。 MACE 是一个基于 DPLL 算法的流行程序，用于搜索具有等式的一阶公式的有限模型。举个例子（McCune 2001），为了表明并非所有群都是可交换的，我们可以指示 MACE 寻找同样伪造交换律的群公理模型，或者等效地寻找以下模型：

e⋅x=x（左恒等式）

i(x)⋅x=e（左逆）

x(⋅y)⋅z=x⋅(y⋅z) （结合性）

a⋅b≠b⋅a（否定交换律）

MACE 找到这些公理的六元素模型，其中 ⋅ 定义为：

· 0 1 2 3 4 5

0 0 1 2 3 4 5

1 1 0 4 5 2 3

2 2 3 0 1 5 4

3 3 2 5 4 0 1

4 4 5 1 0 3 2

5 5 4 3 2 1 0

其中 i 定义为：

x 0 1 2 3 4 5

i(x) 0 1 2 3 4 5

这个例子也再次说明了使用自动演绎系统的好处：人类研究人员需要多长时间才能提出上述或类似的模型？对于更具挑战性的问题，该程序被用作基于分辨率的定理证明器 Prover9（以前称为 Otter）的实用补充，Prover9 搜索证明，MACE 联合寻找（反）模型。为了找到这样的模型，MACE 将一阶问题转换为一组“扁平”子句，为了增加模型大小，这些子句被实例化为命题子句并作为 SAT 问题求解。该方法也已在其他自动推理系统中实现，最引人注目的是在 Paradox 模型查找器中，其中 MACE 式方法通过四种附加技术得到了增强，从而显着提高了效率（Claessen & Sörensson 2003）：减少扁平化子句中的变量数量）、静态对称归约（以减少同构模型的数量）、排序推理（以更精细的级别应用对称归约）和增量 SAT （重复使用连续模型大小之间的搜索信息）。将单独的自动推理系统的互补功能配对的策略也已应用于高阶逻辑，例如 Nitpick，Isabelle/HOL 的反例生成器（Blanchette & Nipkow 2010）。 Brown 2013 描述了高阶逻辑的定理证明过程，该过程使用 SAT 求解来完成大部分工作；该过程是一个完整的、无割断的、基本反驳演算，其中包含对实例化的限制，并已在 Satallax 定理证明器中实现（Brown 2012）。

可满足性模理论 (SMT) 是解决一阶逻辑 SAT 问题的一种非常有趣的方法，其中问题表述中符号的解释受到背景理论的约束。例如，在线性算术中，函数符号仅限于 + 和 -。另一个例子，在数组的外延理论（McCarthy 1962）中，数组函数 read(a,i) 返回索引 i 处的数组 a 的值，而 write(a,i,x) 返回与 a 相同的数组，但是其中 i 处 a 的值为 x。更正式地说，

（读写公理 1）

∀a:数组.∀i,j:索引.∀x:值.i=j → 读(写(a,i,x),j)=x

（读写公理2）

∀a:数组.∀i,j:索引.∀x:值.i≠j → 读(写(a,i,x),j)=读(a,j)

（外延性）

∀a,b:数组.∀i:索引.a=b → 读取(a,i)=读取(b,i)

在这些公理的背景下，SMT 求解器将尝试建立给定一阶公式或数千个与此相关的公式的可满足性（或者双重有效性），例如

i−j=1&f(读(写(a,i,2),j+1)=读(写(a,i,f(i−j+1)),i)

（Ganzinger 等人，2004 年）讨论了一种称为 DPLL(T) 的 SMT 方法，该方法由通用 DPLL(X) 引擎组成，该引擎与背景理论的求解器 SolverT 结合使用。 (2008) 提出了阵列理论设置中的方法，其中 DPLL 引擎负责枚举给定公式的命题模型，而 SolverT 检查这些模型是否与阵列理论一致。他们的方法是健全和完整的，并且可以平滑地扩展到多维数组。

SMT 在验证应用中尤其成功，尤其是软件验证。通过 SMT 提高了 SAT 求解器的效率后，现在的工作是设计更高效的 SMT 求解器 (de Moura 2007)。还需要对不同的基于 SMT 的验证方法提供的技术进行全面的比较和潜在的整合，包括有界模型检查、k 归纳、谓词抽象和插值的惰性抽象 (Beyer, Dangl & Wendler 2018和 2021 年）。

4.3 演绎计算机代数

要自动证明即使是最简单的数学事实也需要大量的领域知识。通常，自动定理证明者缺乏如此丰富的知识，并试图通过应用基本演绎规则从第一原理构建证明。这种方法会导致非常冗长的证明（假设找到了证明），并且每个步骤都在最基本的逻辑层面上得到了证明。然而，通过让定理证明者与计算机代数系统（也称为符号计算系统）交互，可以获得更大的推理步骤和数学推理能力的显着提高。计算机代数系统是一种帮助用户进行数学表达式的符号操作和数值计算的计算机程序。例如，当要求计算不正确积分时

∫

无穷大

0

e−a2t2cos(2bt)dt

一个有能力的计算机代数系统会快速回复答案

√

π

2a

e−b2/a2

本质上，计算机代数系统的运行方式是获取用户输入的输入表达式，并依次对其应用一系列转换规则，直到结果不再改变（有关更多详细信息，请参阅术语重写部分）。这些转换规则编码了大量的领域（数学）知识，使符号系统成为应用数学家、科学家和工程师手中的强大工具，试图解决从微积分和方程求解到组合数学等各种领域的问题。数论。