A Non-Binary Method for Finding Interpolants: Theory and Practice

这是一份关于论文《寻找插值项的非二元方法：理论与实践》（A Non-Binary Method for Finding Interpolants: Theory and Practice）的详细技术总结。

1. 研究问题 (Problem)

在经典命题逻辑中，Craig 插值定理指出：如果公式 $A \to B$ 是有效的，且 $A$ 和 $B$ 共享至少一个命题变量，则存在一个插值项（interpolant）$C$，使得 $A \to C$ 和 $C \to B$ 均有效，且 $C$ 仅包含 $A$ 和 $B$ 共有的变量。

尽管已有多种寻找插值项的方法（如基于 Maehara、Kleene、Smullyan 的理论证明，以及基于 HKP 系统的自动化定理证明方法），但现有的主流方法通常依赖于二元归结（Binary Resolution）。二元归结在每一步中只消除一对互补文字，这可能导致证明步骤较多，且某些基于归结的插值构造在理论上较为复杂，难以直接转化为高效的实现。

本文旨在提出一种新的、基于非二元（Non-Binary）视角的插值项寻找方法，并验证其在实际编程实现中的可行性与性能。

2. 方法论 (Methodology)

2.1 理论基础：反驳系统 (Refutation Systems)

作者没有采用传统的“证明有效性”的公理系统，而是基于反驳系统（Refutation Systems）。

• 核心思想：反驳系统关注的是哪些公式是**无效（非有效）**的。它包含一组反驳公理（非有效公式）和一组保持非有效性的反驳规则。
• 系统构建：基于 Skura (2013) 为经典命题逻辑设计的反驳系统。
  • 公理：秩（Rank）为 0 的范式（即不包含互补文字对 $l, l^*$ 的公式）且非有效。
  • 规则：通过消除一对互补文字 $l$ 和 $l^*$ 来分解公式。
• 关键性质 (†)：一个公式 $F$ 是有效的，当且仅当通过消除 $l, l^*$ 生成的两个子公式 $F_1$ 和 $F_2$ 同时有效。这与传统归结中“只要有一个分支有效”的逻辑不同，体现了非二元的特性。

2.2 插值项寻找算法

作者将上述反驳系统转化为寻找插值项的构造性算法：

1. 输入：两个公式 $X$（合取范式 CNF）和 $Y$（析取范式 DNF），满足 $X \to Y$ 有效。
2. 递归过程：
   • 如果 $X$ 和 $Y$ 没有公共变量，直接返回 $\bot$（若 $X$ 可满足）或 $\top$（若 $Y$ 可满足）。
   • 如果存在互补文字对 $l, l^*$ 分别出现在 $X$ 和 $Y$ 的不同子句中：
     • 应用反驳规则将原问题分解为两个子问题 $G_1$ 和 $G_2$（秩降低）。
     • 递归求解 $G_1$ 和 $G_2$ 的插值项 $I(G_1)$ 和 $I(G_2)$。
     • 构造当前插值项 $I(G)$：
       • 若 $l, l^*$ 仅出现在 $X$ 中：$I(G) = I(G_1) \land I(G_2)$
       • 若 $l, l^*$ 仅出现在 $Y$ 中：$I(G) = I(G_1) \lor I(G_2)$
       • 若 $l, l^*$ 同时出现在 $X$ 和 $Y$ 中：$I(G) = (l \lor I(G_1)) \land (l^* \lor I(G_2))$
3. 终止条件：当秩降为 0 时，根据空子句的情况返回 $\bot$ 或 $\top$。

2.3 实现细节

• 语言：Python。
• 设计原则：为了验证理论，实现采用了“证明概念（Proof-of-concept）”策略，未进行过度优化（如未利用人类可识别的捷径），以展示算法的原始逻辑。
• 输入处理：支持任意数量的变量（扩展版），但在初步实验中限制在 4 个变量以内以控制复杂度。
• 数据结构：使用列表表示子句（D 代表析取，C 代表合取），通过递归消除文字对来构建插值树。

3. 主要贡献 (Key Contributions)

1. 理论创新：

   • 提出了一种基于非二元归结（Non-binary Resolution）思想的插值项寻找方法。
   • 证明了该方法的正确性（扩展插值定理），其证明过程简洁且具有构造性。
   • 揭示了反驳系统性质 (†) 在插值构造中的核心作用，这是以往插值算法中未被充分利用的特性。

2. 与现有方法（HKP 系统）的区别：

   • 步骤更少：由于不局限于二元归结（一次只消去一对文字），该方法可以在更少的步骤中完成插值项的构造。
   • 实现更直接：基于反驳系统的构造性证明使得算法逻辑清晰，易于转化为代码。

3. 实践验证：

   • 开发了 Python 实现，并进行了大规模实验测试。
   • 提供了开源代码和实验数据集，展示了该方法在实际运行中的表现。

4. 实验结果 (Results)

作者进行了两部分实验：

• 实验设置：
  • 使用伪随机生成器生成 $X \to Y$ 为永真式的公式对。
  • 测试了不同子句数量（conjuncts/disjuncts）和变量数量（限制在 4 个变量及扩展至 10 个变量）的情况。
  • 测试了 100,000 次（小变量集）和 1,000 次（大变量集）的插值查找。
• 性能指标：
  • 执行时间：在 4 变量限制下，平均执行时间极短（约 0.0032 秒至 0.011 秒）。
  • 插值项大小：随着输入公式规模的增加，插值项的大小和执行时间呈线性增长趋势。
  • 步骤对比：在特定示例中（如 D'Silva [2010] 中的例子），传统 HKP 系统需要 5 步，而该方法仅需 2 步即可得出结论。
• 观察：
  • 虽然生成的原始插值项形式复杂（包含大量 $\bot$ 和 $\top$），但经过简化后符合逻辑直觉。
  • 算法在处理大变量集时表现依然稳定，线性关系表明其具有良好的可扩展性潜力。

5. 意义与展望 (Significance & Future Work)

• 理论意义：提供了一种从“反驳”视角理解插值定理的新途径，简化了证明过程，并展示了非二元逻辑在插值构造中的优势。
• 应用价值：证明了基于反驳系统的插值算法在自动化定理证明和模型检测（Model Checking）等需要插值项的领域具有实际应用潜力。
• 局限性：目前的实现主要针对命题逻辑，且生成的插值项未经过深度简化（虽然这不影响正确性，但影响可读性）。
• 未来工作：
  • 扩展至一阶逻辑：这是最大的挑战，需要将当前的命题逻辑方法推广到一阶逻辑（First-Order Logic）的插值系统中。
  • 优化实现：开发更高效的简化算法，减少插值项的冗余，提升实际工程应用中的性能。

总结：这篇论文成功地将抽象的反驳系统理论转化为具体的插值项寻找算法，并通过实验证明了其高效性和可行性。其核心创新在于利用非二元归结特性，提供了一种比传统二元归结方法步骤更少、逻辑更直观的插值构造方案。