有界片段的归结决策过程

# 有界片段的归结决策过程 ## 1. 引言 在逻辑推理和定理证明领域，有界片段（Guarded Fragment）的可判定性问题一直是研究的热点。此前，对于有界片段相关问题存在两个疑问：一是是否仅将某些关系用作保护；二是一元有界片段 GF2 的精确复杂度是多少。Szwast 和 Tendera 在 2001 年肯定地回答了第一个问题，他们通过复杂的模型论构造，证明了带有传递保护的有界片段 GF[TG] 在 2EXPTIME 内可判定。Kieroński 在 2003 年证明了带有传递性的一元 GF2 的 2EXPTIME 下界，从而回答了第二个问题。 基于结构枚举的过程存在实际缺点，若不进一步优化，这些方法会展现出完整的最坏情况复杂度。而基于归结的方法是模型论过程的合理替代方案，其目标导向的性质和众多改进使其能在问题的“简单”和“困难”实例之间良好扩展。本文将展示归结改进的实际能力，如冗余消除以及结合选择函数使用排序约束，并提出针对 GF[TG] 的第一个基于归结的决策过程。同时，还将展示如何将归结用作决策过程的规范语言，引入特殊的方案符号来简洁描述归结策略。 ## 2. 预备知识 ### 2.1 一阶逻辑子句逻辑的标准符号 - **表达式**：表达式可以是项或文字。文字符号 \(l\) 为 \(a\) 或 \(\neg a\)，其中 \(a\) 是谓词符号；表达式符号 \(e\) 可以是函数符号 \(f\) 或文字符号 \(l\)。文字和表达式可表示为 \(L = l(t_1, \ldots, t_n)\)，\(E = e(t_1, \ldots, t_n)\)。 - **子句**：子句是文字的析取，即 \(C = L_1 \vee \cdots \vee L_n\)，空语句用 \(\square\) 表示。 - **表达式深度**：表达式 \(E\) 的深度 \(dp(E)\) 递归定义如下： - \(dp(x) := 0\)； - \(dp(e(t_1, \ldots, t_n)) := \max\{0, dp(t_1), \ldots, dp(t_n)\} + 1\)。 - 子句 \(C = L_1 \vee \cdots \vee L_n\) 的深度 \(dp(C) := \max\{0, dp(L_1), \ldots, dp(L_n)\}\)。 - **公式宽度**：公式 \(F\) 的宽度 \(wd(F)\) 是 \(F\) 的子公式中自由变量的最大数量。 ### 2.2 归结定理证明框架 为描述决策过程，使用带有选择的有序归结演算 \(OR^{\succ}_{Sel}\)，并增强了额外的简化规则。该演算由可允许排序 \(\succ\) 和选择函数 \(Sel\) 参数化。 #### 2.2.1 可允许排序 - **可提升性**：对于原子的偏序 \(\succ\)，若 \(A_1 \succ A_2\) 意味着对于任何替换 \(\sigma\) 都有 \(A_1\sigma \succ A_2\sigma\)，则称 \(\succ\) 是可提升的。 - **全归约排序**：\(\succ\) 是基原子上的全归约排序。可允许排序在现有定理证明器中被广泛使用，例如带状态的递归路径排序 \(RPOS\) 和 Knuth - Bendix 排序 \(KBO\)。 排序 \(\succ\) 扩展到文字上，将 \(L = A\) 视为多重集 \(\{A\}\)，\(L = \neg A\) 视为多重集 \(\{A, A\}\)；子句上的排序是文字排序的多重集扩展。 #### 2.2.2 选择函数 选择函数 \(Sel\) 为每个子句分配一组负文字，称为选定文字。文字 \(L\) 在子句 \(C\) 中是合格的，如果它是选定的（\(L \in Sel(C)\)），或者没有选定文字且 \(L\) 在 \(C\) 中是最大的。 #### 2.2.3 有序归结演算的推理规则 - **有序（超）归结**： \[ HR: \frac{C_1 \vee A_1^* \quad \cdots \quad C_n \vee A_n^* \quad D \vee \neg B_1^* \vee \cdots \vee \neg B_n^*}{C_1\sigma \vee \cdots \vee C_n\sigma \vee D\sigma} \] 其中 \(\sigma = mgu(A_i, B_i)\)，且 \(A_i\) 和 \(\neg B_i\) 是合格的（\(1 \leq i \leq n\)）。 - **有序因式分解**： \[ OF: \frac{C \vee A^* \vee A'}{C\sigma \vee A\sigma} \] 其中 \(\sigma = mgu(A, A')\)，且 \(A\) 是合格的。 传统的有序归结规则 \(OR\) 是有序（超）归结规则在 \(n = 1\) 时的特殊情况。演算 \(OR^{\succ}_{Sel}\) 对于任何可允许排序 \(\succ\) 和选择函数 \(Sel\) 的选择都是反驳完全的，并且与一般的冗余概念兼容，允许使用额外的简化规则。 #### 2.2.4 冗余和简化规则 - **冗余子句**：基子句 \(C\) 相对于一组基子句 \(N\) 是冗余的，如果 \(C\) 可从 \(N\) 中小于 \(C\) 的子句集合 \(N_{\prec C}\) 推出；非基子句 \(C\) 相对于 \(N\) 是冗余的，如果 \(C\) 的每个基实例 \(C\sigma\) 相对于 \(N\) 的所有基实例集合 \(N^{gr}\) 是冗余的。 - **冗余推理**：基推理 \(S \vdash C\) 相对于子句集合 \(N\) 是冗余的，如果其结论 \(C\) 可从 \(N^{gr}_{\prec \max(S)}\) 推出，其中 \(\max(S)\) 是 \(S\) 中的最大子句；非基推理 \(S \vdash C\) 相对于 \(N\) 是冗余的，如果该推理的每个基实例 \(S\sigma \vdash C\sigma\) 相对于 \(N\) 是冗余的。 - **饱和子句集**：如果子句集合 \(N\) 中每个相对于 \(N\) 非冗余的推理的结论都包含在 \(N\) 中，则称 \(N\) 是相对于冗余饱和的。 定理 1：设 \(N\) 是在 \(OR^{\succ}_{Sel}\) 中相对于冗余饱和的子句集合，则 \(N\) 是可满足的当且仅当 \(N\) 不包含空子句。 对于决策过程，不需要冗余的全部能力，而是使用额外的简化规则。非确定性推理规则 \(S \vdash S_1 || S_2 \cdots || S_k\) 是可靠的，如果 \(S\) 的每个模型都可以扩展为某个 \(S_i\)（\(1 \leq i \leq k\)）的模型。如果每个 \(S_i\) 使 \(S\) 中的某个子句冗余，则该规则称为简化规则。 在本文中使用的简化规则是： - **消除重复文字**： \[ ED: \frac{[[ C \vee D \vee D ]]}{C \vee D} \] ### 2.3 约束子句 有序归结演算在非基级别是基级别演算的直接提升版本。在决策过程中，使用形式为 \(C | R\) 的约束子句，其中 \(C\) 是非基子句，\(R\) 是形式为 \(t \succ s\) 或 \(t \succeq s\) 的排序约束集合。约束子句 \(C | R\) 表示 \(C\) 的基实例 \(C\sigma\) 的集合，使得 \(R\sigma\) 中的每个约束都为真。有序归结演算和所有冗余概念都可以直接应用于约束子句，只需考虑满足约束的替换。 ### 2.4 表达式和子句的方案 为描述基于归结的决策过程，需要对一组子句进行推理，因此引入特殊符号来紧凑表示子句集合。扩展词汇表，引入表示函数符号集合（函数组）、谓词符号集合（谓词组）或文字符号集合（文字组）的签名组，用带“帽子”的小写字母 \(\hat{g}\) 表示。 #### 2.4.1 方案的定义 - **项方案**： \[ \hat{Tm} ::= x | \hat{f}(\hat{t}_1, \ldots, \hat{t}_n) | \hat{f}\langle!\hat{t}_1, \ldots,!\hat{t}_n, \hat{s}_1, \ldots, \hat{s}_m\rangle, \quad n \geq 0, m \geq 0 \] - **文字方案**： \[ \hat{Lt} ::= \hat{l}(\hat{t}_1, \ldots, \hat{t}_n) | \hat{l}\langle!\hat{t}_1, \ldo