利用依赖对改进模块化终止证明及右（基或变量）重写系统性质判定

### 利用依赖对改进模块化终止证明及右（基或变量）重写系统性质判定 在自动化定理证明领域，重写系统的终止性、可达性、可合并性等性质的判定是重要的研究内容。本文将围绕利用依赖对改进模块化终止证明，以及右（基或变量）重写系统（RGV系统）性质判定展开探讨。 #### 利用依赖对改进模块化终止证明 在依赖对的终止证明中，存在一些复杂情况。例如对于循环 `{PLUS(s(x), y) → PLUS(p(s(x)), y), PLUS(x, s(y)) → PLUS(x, p(s(y)))}`，传统的参数过滤和满足特定定理约束的约简对方法失效。原因在于 `p` 的规则使得过滤不能丢弃 `p` 的参数，且“缩小依赖对”的转换技术也不适用，因为依赖对的左右两边会相互合一。 不过，通过特定定理和多项式解释的约简对，能有效解决这类问题。如使用多项式解释 `Pol(PLUS(x, y)) = x + y`，`Pol(s(x)) = x + 1`，`Pol(p(x)) = x`，`p` 的规则严格递减可被移除，此时 `p` 成为构造函数。若使用“实例化依赖对”技术，第二个依赖对可被替换，从而打破循环，不产生约束。 若添加规则 `p(0) → 0`，同样可移除 `p(s(x)) → x`，但 `p` 不是构造函数，不能删除整个循环。不过，通过特定的参数过滤和字典序路径序（LPO）能满足产生的约束。 为了自动化应用相关定理，采用基于系数为 `{0, 1}` 的线性多项式解释的约简对。由于约简关系必须单调，`n` 元函数符号只有两种可能的解释，搜索空间小。而且多项式序能高效解决约束问题，无需回溯。因此，该定理应反复应用，直到不再有规则可删除。 在应用定理时，不必区分规则和依赖对的约束，只要在任何约束中找到严格递减，就可解决相关问题。 以下是不同定理和方法在终止证明实验中的表现： |定理及方法|Emb| LPO |Polo| | ---- | ---- | ---- | ---- | |Thm. 7|39 s, 28 %|606 s, 51 %|9 s, 61 %| |Thm. 11|7 s, 30 %|569 s, 54 %|8 s, 66 %| |Thm. 17|42 s, 38 %|261 s, 59 %|5 s, 73 %| |Thm. 22|50 s, 52 %|229 s, 61 %|5 s, 78 %| |Thm. 22, 23|51 s, 65 %|234 s, 75 %|6 s, 85 %| |Thm. 22, 23, tr|82 s, 78 %|256 s, 84 %|9 s, 91 %| |Inn|8 s, 78 %| - | - | 从表格数据可以看出，随着定理的不断细化，终止证明能力不断增强，对于较复杂的序，效率也显著提高。使用“Polo”进行预处理以及依赖对转换能进一步提升证明能力。 #### 右（基或变量）重写系统性质判定 RGV系