自动推理系统：公理相关性排序与实例化推理的探索

### 自动推理系统：公理相关性排序与实例化推理的探索 在自动推理领域，公理相关性排序和实例化推理是两个重要的研究方向。本文将深入探讨基于公理相关性排序的 Divvy ATP 元系统，以及实例化自动推理的相关内容。 #### 基于 LSA 的公理相关性计算 在计算公理与猜想的相关性时，可将公式视为文档，谓词和函数符号视为其中的术语。使用潜在语义分析（LSA）计算公理相关性是一个三步过程： 1. **计算符号对之间的关系强度**：首先基于符号在公式中的共现情况以及包含这些符号的公式总数计算初始关系强度。然后，通过反复结合现有关系强度以及两个符号与其他符号之间的关系强度，计算最终关系强度，即考虑符号之间的传递关系。 2. **为每个公式计算关系强度向量**：向量的每个符号都有一个条目。一个符号的条目是所有其他符号的关系强度与该符号在公式中出现次数的乘积之和。 3. **计算每个公理与猜想的相关性**：通过它们的符号关系强度向量的点积来计算。 LSA 方法已在 C 语言中实现为 APRILS 工具，可通过 SystemB4TPTP 接口使用。APRILS 在 1337 个 TPTP 问题上与 Prophet 进行了比较，结果显示 APRILS 在 49%的问题上表现优于 Prophet，在 23%的问题上与 Prophet 打平。APRILS 的方法更适合包含大量公理的问题，因为这些问题包含更多的语义信息。 #### Divvy ATP 元系统 Divvy ATP 元系统使用相关性排序来选择用于证明给定猜想的公理子集，并尝试从所选公理中证明该猜想。其基本思想是从选择排序中的前一半公理开始，尝试证明猜想。如果猜想被证明，则停止；如果猜想相对于所选公理是不可满足的，则需要更多的公理；如果没有关于猜想的结论，则需要更多或更少的公理。然后考虑前四分之一、前三分之四的公理，依此类推，直到达到粒度限制或全局资源限制。 Divvy 系统的基本过程通过以下优化得到改进： 1. 在划分和选择开始之前，可以使用所有公理进行一次证明尝试。 2. 用户可以指定要选择的最大公理数，并且只考虑相关性排序列表中的该数量的公理。 3. 在每次证明尝试之前，可以运行模型查找器来尝试证明猜想相对于所选公理是不可满足的。 4. 证明尝试可以使用仅确定证明存在性的 ATP 系统，最终使用输出完整证明的 ATP 系统。 5. 用户可以指定用于证明保证、证明查找和模型查找的 ATP 系统。 6. 用户可以指定用于计算公理相关性排序的工具。 Divvy 系统在 C 语言中实现，依赖于 TPTP 世界基础设施来处理公式、运行相关性测量工具和运行 ATP 系统。它可通过 SystemOnTPTP 接口使用。 #### Divvy 系统的评估 Divvy 系统使用 Prophet 和 APRILS 在 MPTP 挑战问题上进行了评估。这些问题分为“Bushy”和“Chainy”两组，每组包含 252 个问题。“Bushy”组的问题包含 MPTP 过程确定可能用于证明的公理，而“Chainy”组的问题包含所有先前的 Mizar 知识作为公理。 评估结果如下表所示： | System | Bushy | | | Chainy | | | | --- | --- | --- | --- | --- | --- | --- | | | Total | <60s | >60s | Total | <60s | >60s | | E | 141 | 139 | 2 | 91 | 80 | 11 | | Divvy(E)+Original | 163 | 139 | 24 | 80 | 80 | 0 | | Divvy(E)+Rever