ICS与E0.81定理证明器的技术解析

# ICS与E 0.81定理证明器的技术解析 ## 1. ICS决策过程 ### 1.1 数组上下文表示 ICS中数组上下文以等式形式表示，等式右边是变量，左边是扁平数组项。例如，通过引入新变量（如 `a!3`）来扁平化项。当有等式 `a!3 = b[k := y]` 时，会推导出 `y = a!3[k]`。在当前上下文中，`a[k]` 的规范形式为 `y`。 ```plaintext ics> show. ... arr: {a!3=b[k:=y], y=a!3[k], a!3=a[j:=x], x=a!3[j], y=a[k]} ``` ### 1.2 规范器操作 规范器会返回输入文字的一个子集，用于证明等式的有效性。例如： ```plaintext ics> can a[k]. :term y :justification {i = k, b[k := y] = a[j := x], i <> j} ``` ### 1.3 基于SAT的约束满足 ICS可解决命题可满足性问题，结合了多种理论的文字。例如： ```plaintext ics> sat [x > 2 | x < 4 | p] & 2 * x > 6. :sat s2 :model [p |-> :true][-6 + 2 * x >0] ``` 具体操作步骤如下： 1. 定义公式 `φ`，并通过映射 `L` 将其转换为命题公式 `L−1[φ]`。 2. 使用SAT求解器检查 `L−1[φ]` 的可满足性。 3. 若得到的真值赋值 `l1∧...∧ln` 是虚假的（即 `L[l1∧...∧ln]` 不是基可满足的），则添加子句 `(¬l1 ∨... ∨¬ln)`，并重新调用SAT求解器检查 `(¬l1 ∨... ∨¬ln) ∧L−1[φ]` 的可满足性。 ### 1.4 SAT命令的优化 - **非时间回溯**：SAT求解器在搜索过程中会通知地面决策过程每个变量的赋值，地面决策过程可能触发非时间回溯并确定合适的回溯点。 - **剪枝搜索空间**：利用地面决策过程提供的不一致性理由进一步剪枝搜索空间。 ### 1.5 ICS的应用 ICS主要应用于SAL中，用于无限状态系统的有界模型检查（BMC(∞)）和归纳证明。转换系统用SAL语言编码，BMC(∞) 问题以命题约束公式的可满足性问题形式生成。目前支持UCLID、CVC、SVC和ICS作为验证后端，在多种基准测试中表现良好。 ## 2. E 0.81定理证明器 ### 2.1 简介 E是用于带等式的子句逻辑的高性能定理证明器，在CADE ATP系统竞赛的UEQ和MIX类别中一直名列前茅，可应用于软硬件验证和数学领域。最新版本E 0.81 Tumsong有诸多改进，系统可在GNU GPL下获取，源码易于安装，能在多种现代UNIX方言下编译。 ### 2.2 演算 - **饱和反驳过程**：通过推导空子句来证明子句集的不可满足性。 - **叠加演算SP**：是[BG94]中描述的演算的变体，增强了多种显式冗余消除技术和伪分裂。 - **等式表示**：非等式原子编码为与保留常量 `$true` 的等式，一阶项和原子用两个不相交的类别表示。 - **推理规则**：主要的生成推理规则是叠加（受限参数化），负责生成超过99%的子句。 - **简化技术**：包括重言式消除、重写、子句规范化、包容和AC冗余消除，还新增了等式定义展开和上下文文字切割。 ### 2.3 等式定义展开 等式定义是形式为 `f(X1, ..., Xn) = t` 的单位子句（其中 `f` 不在 `t` 中且 `t` 不包含额外变量）。在预处理步骤中，用等式定义替换 `f` 并删除该子句，可完全消除函数符号 `f`，便于找到更好的项排序。 ### 2.4 上下文文字切割 将子句视为条件事实，选择一个文字作为活动文字，其他文字作为条件。若条件在另一个子句的上下文中成立，则用活动文字简化该子句。目前仅用于切割相反极性的隐含文字： ```plai ```