自动化定理证明在等式理论与航空航天软件认证中的应用

# 自动化定理证明在等式理论与航空航天软件认证中的应用 ## 等式理论中的组合决策程序 ### 等式理论组合的基本原理 在等式理论的研究中，我们常常需要处理多个理论的组合问题。假设有三个等式理论 \(E_0\)、\(E_1\) 和 \(E_2\)，它们分别具有签名 \(\Sigma_0\)、\(\Sigma_1\) 和 \(\Sigma_2\)，并且满足一定的条件： - \(\Sigma_0 = \Sigma_1 \cap \Sigma_2\)； - \(E_0\) 是高斯的且有效局部有限； - 对于 \(i = 1, 2\)，\(E_i\) 与 \(E_0\) 兼容，并且是 \(E_0\) 的保守扩展。 如果 \(E_1\) 和 \(E_2\) 中的字问题是可判定的，那么 \(E_1 \cup E_2\) 中的字问题也是可判定的。这一结论是通过组合过程的总正确性得出的。 ### 模态逻辑中的融合可判定性 #### 模态逻辑的定义 我们所研究的模态逻辑是对应于布尔代数理论的等式扩展的逻辑。一个模态签名 \(\Sigma_M\) 是一组具有相应元数的操作符号集合。从 \(\Sigma_M\) 出发，使用可数多个命题变量、\(\Sigma_M\) 中的操作符号、布尔连接词以及常量 \(\top\)（表示真）和 \(\bot\)（表示假）来构建命题公式。 一个基于模态签名 \(\Sigma_M\) 的经典模态逻辑 \(L\) 是一组命题公式，满足以下条件： 1. 包含所有经典重言式； 2. 在命题变量的统一替换下封闭； 3. 在假言推理规则下封闭（从 \(t\) 和 \(t \Rightarrow u\) 推出 \(u\)）； 4. 对于每个 \(n\) 元操作符 \(o \in \Sigma_M\)，在以下替换规则下封闭：从 \(t_1 \Leftrightarrow u_1, \ldots, t_n \Leftrightarrow u_n\) 推出 \(o(t_1, \ldots, t_n) \Leftrightarrow o(u_1, \ldots, u_n)\)。 #### 模态逻辑与等式理论的关系 经典模态逻辑 \(L\) 可以与一个基于布尔代数的等式理论 \(E_L\) 相关联。反之，一个基于布尔代数的等式理论 \(E\) 也可以与一个经典模态逻辑 \(L_E\) 相关联。具体来说，给定一个经典模态逻辑 \(L\)，其对应的等式理论 \(E_L\) 的签名为 \(\Sigma_M \cup \Sigma_{BA}\)，公理集为 \(BA \cup \{t_{BA} \approx 1 | t \in L\}\)，其中 \(t_{BA}\) 是通过将 \(t\) 中的逻辑连接词替换为相应的布尔代数运算符得到的。反之，给定一个基于布尔代数的等式理论 \(E\)，其对应的经典模态逻辑 \(L_E\) 由公式集 \(\{t_L | \models_E t \approx 1\}\) 公理化，其中 \(t_L\) 是通过反向替换过程得到的。 #### 模态逻辑的融合与可判定性 对于两个经典模态逻辑 \(L_1\) 和 \(L_2\)，它们的融合 \(L_1 \oplus L_2\) 定义为 \([L_1 \cup L_2]\)。由于 \(E_{L_1 \oplus L_2}\) 与 \(E_{L_1} \cup E_{L_2}\) 演绎等价，因此 \(L_1 \cup L_2 \vdash t\) 的判定问题可以归结为 \(E_{L_1} \cup E_{L_2} \models t_{BA} \approx 1\) 的字问题。 为了应用组合定理，我们需要确保布尔代数的公共子理论 \(BA\) 满足组合过程的要求。我们将研究限制在一致的模态逻辑 \(L_1\) 和 \(L_2\) 上，即不包含 \(\bot\) 的逻辑。因为如果 \(L_1\) 或 \(L_2\) 不一致，那么 \(L_1 \oplus L_2\) 也不一致，其判定问题是平凡的。 已经证明 \(BA\) 满足有效局部有限性的要求，并且对于每个一致的经典模态逻辑 \(L\)，理论 \(E_L\) 是 \(BA\) 的保守扩展。此外，还需要证明 \(BA\) 是高斯的，并且 \(E_L\) 与 \(BA\) 兼容。对于 \(BA\) 的局部求解器，对于每个形式为 \(u(x, y) \approx 1\) 的 \(e\) - 公式（以及新变量 \(z\)），项 \(s(x, z) := (u(x, 1) \supset u(x, z)) \supset (z \cap (u(x, 0) \supset u(x, z)))\) 是 \(u(x, y) \approx 1\) 在 \(BA\) 中关于 \(y\) 的局部求解器。 #### 复杂度分析 如果 \(L_1\) 和 \(L_2\) 的判定程序在 PSPACE 中，那么 \(L_1 \oplus L_2\) 的组合判定程序在 EXPSPACE 中；如果判定程序在 EXPTIME 中，那么组合判定程序在 2EXPTIME 中。 ### 组合过程示例 考虑经典模态逻辑 \(KT\)，其模态签名为 \(\{2\}\)，通过向 \(K\) 添加公理模式 \(2x \Rightarrow x\) 得到。令 \(KT_1\) 和 \(KT_2\) 是 \(KT\) 的两个不相交签