一文了解定理证明器 ACL2

ACL2 源码：https://github.com/acl2/acl2

ACL2 用户手册：https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html

简介#

ACL2 是一个交互式定理证明器，基于 Common Lisp 编程语言，结合了 Formal 模型和用于证明这些模型属性的定理证明器。

  • 证明器：用户给它一个公式，它会为用户提供该公式的证明或告诉用户没有证明。

  • 交互式：ACL2 定理证明器可以自动查找证明。但大多数情况下，用户必须提供帮助（引导 ACL2 首先证明关键引理 Lemma）。

  • Common Lisp 是标准列表处理编程语言，ACL2 是其的一个子集。

  • Formal 模型：ACL2 用于构建计算机硬件和软件的数学模型。

工业应用#

ACL2 被广泛用于学术界和工业界，它被用于验证微处理器、微码、Sun Java 虚拟机、操作系统内核、其他验证器和有趣算法模型的特性，如 AMD 使用 ACL2 验证了 AMD Athlon™ 的基本浮点运算符与 IEEE 754 规范的兼容性；IBM 使用 ACL2 对 IBM Power 4 上的浮点除法和平方根进行了验证。

ACL2 系统架构#

ACL2 系统架构图

用户通过给出定义、定理和建议来与定理证明器进行交互。

可以将其他事件的某些经过认证的文件中的所有规则包含在数据库中。此类经过认证的文件称为 books。数据库包含 ACL2“知道”的所有规则。

证明通常建立在许多 books 的基础上，其中一些是专门针对该问题领域编写的，另一些则涉及常用领域，例如算术或列表处理。 ACL2 的发行版包括许多用户编写的 books。

定理证明器#

当你给定理证明者一个要证明的目标公式时，它会尝试通过将其分解为子目标来证明它，每个子目标都必须被证明才能证明原始目标。这种目标的分解是通过 ACL2 中内置的各种证明技术来完成的。不同的证明技术以不同的方式分解公式。

定理证明者的行为受到公理、定义和先前证明的定理的规则数据库的影响。

大多数时候，用户只需通过确定要证明的 Lemma 来指导定理证明。（Lemma 只是用户认为在其他定理的证明中有用的定理。）

ACL2 使用流程#

  1. 你向 ACL2 提出待证的猜想
  2. 通常情况下，它无法证明（或你终止了它的尝试），但它会输出一些关键检查点
  3. 你查看了关键检查点，并确定一个已知的有帮助的事实
  4. 将你的知识形式化为公式，并说明 ACL2 应如何将公式转化为规则；
  5. 递归地应用上述步骤，让 ACL2 来证明你的公式并将其存储为你指定的规则类型

ACL2 工作原理#

ACL2 使用六种内置证明技术来将目标公式分解为子目标。

  1. 简化（Simplification） — 运用决策程序和先前证明的规则进行重写，实际上包括一系列其他你可控制的技术。简化是唯一能将公式减少为 0 个子目标（即证明它）而不仅仅是将其转换为其他公式的证明技术。大多数证明中主要的活动就是简化。你可以通过多种方式影响简化器对公式的处理。优秀的用户大部分时间都在思考如何控制简化器。

  2. 析构消除（Destructor Elimination） — 通过用“构造”（如 (CONS A B)）替换变量（如 X）来摆脱“析构”（如 (CAR X) 和 (CDR X)）。你可以告诉 ACL2 新的析构器/构造器组合。

  3. 施肥（Fertilization） — 使用等价假设，用目标中的一侧替换另一侧。在归纳时，ACL2 可能会决定使用其所谓的交叉施肥启发法来限制替换，如下所示：仅替换到结论的一侧，从而使用归纳假设为另一次归纳之前的可能泛化做好准备。请注意，仅在启用泛化时才使用交叉施肥：使用提示：do-not ‘（泛化）时，仅应用完全施肥。

  4. 泛化（Generalization） — 用新变量替换一个项，并限制新变量具有某些项的性质。你可以控制对新变量施加的限制。这是一种启发式方法，为另一个归纳做准备。

  5. 无关性消除（Elimination of Irrelevance） — 丢弃不必要的假设。这是一种为另一个归纳做准备的启发式方法。

  6. 归纳（Induction） — 选择一个归纳方案来证明一个公式。归纳是由公式中出现的递归函数“建议”的。但是你可以通过项来控制什么样的归纳被提出。

你还可以添加其他技术，称为 clause processors 子句处理器。

依次尝试各种技术，首先是简化，最后是归纳。每种技术报告三个结果之一：它发现没有什么可以改变（即该技术不适用于该子目标），它决定中止证明尝试（通常是因为有理由相信证明失败），或者它将目标分解为 k 个子目标。

最后一个结果有一个特殊情况：如果 k 为 0，则该技术证明了目标。每当 k 不为 0 时，该过程就会重新开始，并对 k 个子目标中的每一个进行简化。然而，它保存了所有子目标，归纳法是唯一可以尝试的证明技术。这样，你就可以在启动另一个归纳之前了解它在每个基本案例和一个归纳的归纳步骤上的执行情况。

它会一直运行，直到你或其中一种证明技术中止证明尝试或直到所有子目标都得到证明。

请注意，如果简化产生子目标，则该子目标将被重新简化。这个过程一直持续到子目标无法进一步简化为止。只有这样才能尝试下一个证明技术。据说这样的子目标在简化下是稳定的。