断开表中变量的广义处理

### 断开表中变量的广义处理 在逻辑推理和证明自动化领域，断开表（Disconnection Tableaux）是一种重要的方法，它在处理变量时有着独特的方式。本文将深入探讨断开表中变量的广义处理，包括其合理性证明、完备性分析以及相关的正则性问题，同时还会介绍相关的工作。 #### 1. 合理性证明 为了证明断开表的合理性，我们将表 \(T\) 转换为一个可以根据一般表规则关闭的表。具体步骤如下： 1. **替换共享变量**：将 \(T\) 中所有共享变量替换为同一个任意常量，这不会影响 \(l\) - 封闭性。 2. **替换包含局部变量的文字**：将每个包含局部变量 \(u_1, \ldots, u_n\) 的文字 \(k\) 替换为 \(k\) 在 \(l\) - 封闭步骤中使用的所有实例 \(k\theta_i\) 的有限合取 \(C_k\)。这是合理的，因为满足 \(\forall u_1 \cdots u_n k\) 的变量赋值和解释对也满足 \(C_k\)。 3. **模拟 \(l\) - 封闭步骤**：使用标准的 \(\alpha\) - 规则，从合取 \(C_k\) 中选择相应的文字 \(k\theta_i\)，模拟使用 \(k\) 和叶文字 \(k_i\) 的 \(l\) - 封闭步骤。这样，相应的分支在标准意义上是互补的。 #### 2. 带局部变量的断开表的完备性 证明新方法的完备性比证明合理性要困难得多。关键在于 \(l\) - 链接规则，因为断开方法是一种基于实例化的方法，通过生成输入子句的实例来工作。而 \(l\) - 链接规则削弱了子句实例的生成，因为某些子句没有以其完全特化的形式放在表上。问题在于 \(l\) - 封闭规则是否足够强大，以弥补这一点并保持完备性。 为了解决这个问题，我们引入了实例保留枚举（Instance Preserving Enumeration，ipe）的概念。 **定义 1（实例保留枚举）**：设 \(P\) 是一条路径，\(S\) 是 \(P\) 中元素的子句集。\(P\) 的实例保留枚举（ipe）是任何序列 \(E = L_1, L_2, L_3, \ldots\)，其中恰好出现 \(P\) 的元素，并且对于任何 \(L_i = \langle c_i, l_i \rangle\) 和 \(L_j = \langle c_j, l_j \rangle\)，当 \(c_i\theta\) 是 \(c_j\theta\) 的一个适当实例（其中 \(\theta\) 是将所有变量映射到同一个变量的替换）时，有 \(i > j\)。 对于任何 \(P\) 的实例保留枚举 \(E\)，存在一条通过 \(S\) 的 Herbrand 集 \(S^*\) 的路径 \(P^*\)，满足以下性质： - 文字出现 \(L = \langle c, l \rangle\) 在 \(P^*\) 中，当且仅当在 \(E\) 中存在文字出现 \(L_k = \langle c_k, l_k \rangle\) 和替换 \(\sigma\)，使得 \(\langle c_k\sigma, l_k\sigma \rangle = \langle c, l \rangle\)，并且在 \(E\) 中不存在 \(j > k\) 的 \(L_j = \langle c_j, l_j \rangle\) 使得 \(c\) 是 \(c_j\) 的实例。 我们称 \(L_k\) 为子句 \(c\) 或文字出现 \(\langle c, l \rangle\) 在 \(E\) 中的最小匹配器。这样的路径 \(P^*\) 称为 \(E\) 和 \(P\) 的 Herbrand 路径。 接下来，我们定义断开表序列和 \(l\) - 饱和的概念。 **定义 2（断开表序列）**：给定子句集 \(S\) 和通过 \(S\) 的初始路径 \(P\)，\(S\) 和 \(P\) 的断开表序列是任何（可能无限的）序列 \(T = T_0, T_1, T_2, \ldots\)，满足以下性质： - \(T_0\) 是仅由根节点组成的平凡表。 - \(T\) 中的任何 \(T_{i + 1}\) 可以通过对 \(T_i\) 应用 \(l\) - 链接步骤得到。 这样的序列 \(T\) 中的任何表都称为 \(S\) 和 \(P\) 的断开表。 由于断开方法的非破坏性，序列 \(T\) 中的任何表都包含序列中索引较小的所有表作为初始段。因此，我们可以形成 \(T\) 中所有表的树并 \(\bigcup T\)。在有限序列的情况下，\(\bigcup T\) 就是序列中的最后一个元素。一般来说，\(\bigcup T\) 可能是一个无限表，我们称其为序列 \(T\) 的极限表。 **定义 3（\(l\) - 饱和）**：一个（可能无限的）表中的分支 \(B\) 称为 \(l\) - 饱和的，如果 \(B\) 不是 \(l\) - 封闭的，并且对于 \(B\) 上的任何链接 \(\ell = \{ \langle c_1, l_1 \rangle, \langle c_2, l_2 \rangle \}\)，分支 \(B\) 包含文字出现 \(\langle c_3, l_3 \rangle\)，使得存在 \(c_1\) 或 \(c_2\) 关于 \(\ell\) 的 \(l\) - 链接实例 \(c_4\)，它不是 \(c_1\) 或 \(c_2\) 的 \(\forall\) - 变体，\(c_4 \neq_{\forall} c_3\) 且 \(c_4\) 是 \(c_3\) 的实例。断开表序列的极限表称为 \(l\) - 饱和的，如果它的所有分支都是 \(l\) - 封闭的，或者它有一个 \(l\) - 饱和的分支。 由于初始路径只是用于启动表的构建过程，它不受变体自由度条件的限制。因此，可能会出现两个文字出现 \(\langle c, l \rangle\) 和 \(\langle c', l' \rangle\)，其中 \(c\) 和 \(c'\) 是变体，一个在初始分支上，另一个在表分支上，但 \(l\) 和 \(l'\) 可能不是变体。为了解决这个问题，我们定义了调整后的分支。 **定义 4（调整后的分支）**：设 \(B\) 是具有初始路径 \(P\) 的断开表中的一个分支。\(P - B\) 是通过从 \(P\) 中删除所有文字出现 \(\langle c, l \rangle\) 得到的，其中在 \(B\) 中存在 \(\langle c', l' \rangle\)，\(c' =_{\forall} c\) 且 \(c'\) 比 \(c\) 更一般。我们称 \(B^+ = B \cup P - B\) 为 \(P\) 和 \(B\) 的调整后的分支。 下面是一个关于模型特征的命题。 **命题 1（模型特征）**：设 \(B\) 是子句集 \(S\) 和初始路径 \(P\) 的断开表序列的极限表的一个分支。如果调整后的分支 \(B^+\) 是 \(l\) - 饱和的，那么 \(B^+\) 的任何 Herbrand 路径 \(P^*\) 的文字集 \(I\) 是 \(S\) 的一个 Herbrand 模型。 **证明**：首先，\(P^*\) 必须是通过 \(S\) 的整个 Herbrand 集 \(S^*\) 的 Herbrand 路径，因为 \(S\) 中的所有子句都在 \(B^+\) 的域中。然后，主要部分是证明 \(P^*\) 是通过 \(S^*\) 的开放 Herbrand 路径。假设 \(P^*\) 不是开放的，即 \(P^*\) 包含两个文字出现 \(\langle c, l \rangle\) 和 \(\langle c', \neg l \rangle\)。由于 \(P^*\) 是 \(B^+\) 的实例保留枚举 \(E\) 的 Herbrand 路径，\(B^+\) 必须包含两个比 \(\langle c, l