A Strategy Language for Controlled Proof Search

技术摘要：一种用于受控证明搜索的策略语言

问题陈述
在自动推理领域，逻辑演算的静态完备性（即对于任何定理都存在证明的存在性）并不能保证证明器（prover）的动态完备性（即实际找到该证明的能力）。在半可判定逻辑中，推理规则可能会生成无限个后继状态。如果证明搜索策略采用了不公平的探索方式——例如一种无限优先考虑某一分支的朴素深度优先方法——它可能会永远推迟相关的推理，从而导致即使证明存在也无法发现有效证明。这一问题在像 Pgeon 这样将推理规则与证明搜索策略分离的框架中尤为突出，因为探索策略的设计成为了决定成败的关键因素。

方法论
本文为 Pgeon 引入了一种形式化的策略语言。Pgeon 是一个元证明器框架，它将逻辑演算的声明式规范编译为可执行的证明器。其核心方法论转变是将证明搜索建模为通过流（streams）对证明状态进行枚举，而非仅仅将其视为状态间的关系。

1. 形式语义： 证明状态 ($\Sigma$) 被视为一个部分构建的证明树。策略被定义为一个函数 $s: \Sigma \to \text{Str}(\Sigma)$，将一个状态映射为一个后继状态的流（有限或无限）。这使得非确定性变得显式化：

   • 空流表示失败。
   • 单元素流表示确定性成功。
   • 包含多个元素的流表示非确定性分支。
   • 无限流表示可以生成无界后继项的规则。

2. 组合子： 该语言提供了一组用于组合这些策略的算子，区分了有偏（深度优先）和公平（交错）的探索：

   • 顺序复合 ($;$)： 将一个策略应用于另一个策略的结果。
   • 左偏选择 ($\parallel$)： 尝试第一个策略；如果其失败（空流），则回退到第二个策略。
   • 公平顺序复合 ($\&;$)： 使用对角线法 ($\triangle$) 交错应用顺序结果，确保如果某个结果在有限步内是可达的，它最终会被探索到。
   • 公平选择 ($\&|$)： 公平地交错两个备选策略的结果。
   • 重复 ($*$)： 定义为使用公平顺序复合的最小不动点 ($\mu X. \text{id} \&; (s \&; X)$)，确保所有有限的迭代深度都会被探索，而不是严格进行深度优先搜索。

3. 原语操作： 该语言包括原语规则 ($r$) 和穷尽应用算子 ($r!$)，后者将规则应用于状态中所有可容纳的匹配项。

核心贡献

• 组合流语义： 本文提供了一种用于策略组合子的组合代数，其中搜索空间被具象化为一个一等对象（流）。这使得能够独立于实现细节（如栈控制或延续）来对公平性和枚举进行推理。
• 公平机制： 通过引入基于对角线交错的算子 ($\&;$ 和 $\&|$)，该框架解决了“饥饿”问题，即无限分支可能导致无法发现有限证明的问题。
• Pgeon 的形式化策略语言： 本研究将 Pgeon 框架中的策略组件形式化，将证明搜索的控制流抽象为一种声明式语言。

结果与案例研究
本文通过两个案例研究展示了该方法的表达能力和有效性：

1. 一阶逻辑 (LK)： 作者探讨了闭合（统一化/unification）与规则饱和之间的相互作用。朴素的重复规则应用策略往往会失败，因为它过早地承诺了特定的实例化。所提出的策略 $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$ 利用公平复合来交错闭合尝试与规则饱和。这确保了在所有搜索深度上都会探索不同的统一化选择，从而防止系统陷入无限实例化循环，同时遗漏闭合推导。

2. 模态逻辑 (S4)： 在 S4 中，非确定性规则 $\theta$（任意移除公式）对于启用 S4 模态规则是必要的，但也带来了丢弃对闭合有用的公式的风险。不受控地使用 $\theta$ 会导致死路。作者提出了结合策略 $\theta^* \&; \text{S4}$，它公平地探索所有移除公式以启用 S4 应用的方式。该策略被集成到一个更大的策略 $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$ 中，确保如果 S4 的成功应用需要特定子集的移除公式，该配置最终会被触达，从而避免饥饿。

意义
本文声称，这种方法为指定和分析证明过程提供了原则性和模块化的基础。通过将推理规则与搜索策略分离，并提供具有组合语义的形式化语言，该框架允许对半可判定逻辑中的搜索空间进行系统的探索。它证明了即使在朴素的深度优先策略失效的情况下，通过显式管理通过流交错实现的公平性，也可以实现动态完备性。这项工作使得在抽象层面（独立于特定证明器的实现）对证明搜索过程进行推理成为可能。