逻辑程序转换的自动正确性证明与CoreTuLiP信任管理系统

### 逻辑程序转换的自动正确性证明与CoreTuLiP信任管理系统 #### 逻辑程序转换的自动正确性证明 在逻辑程序转换领域，有一种方法可以自动证明基于规则的逻辑程序转换的正确性。当我们有一个由展开、折叠和目标替换转换规则构建的转换序列时，会给该序列中程序的子句关联一些被称为权重的未知自然数。同时，会构建一组线性约束，这些权重必须满足这些约束，才能保证转换序列的完全正确性。 例如，通过对折叠规则的对称应用，从子句 F2 可以得到： ```plaintext F3. new2([H|T ], L2, L3, [H|R]) ←new2(T, L2, L3, R) u9 ``` 同时有约束 `u9 = u2`。最终的程序 `Append ∪{E1, E3}` 和 `Append ∪{F1, F3}` 通过谓词重命名 ρ 语法等价，其中 `ρ(new1) = new2`。转换序列 `Append ∪{D2} →· · · →Append ∪{F1, F3}` 是对称的。 与转换序列 `Append ∪{D1} →· · · →Append ∪{E1, E3}` 相关的正确性约束系统如下： ```plaintext C1: {u1≥1, u2 ≥1, w1 + u1 ≥1, u8 ≥1, u8 ≤2u2} ``` 与转换序列 `Append ∪{D2} →· · · →Append ∪{F1, F3}` 相关的正确性约束系统如下： ```plaintext C2: {u1≥1, u2 ≥1, w2 + u1 ≥1, u9 ≥1, u9 =u2} ``` 由于 C1 和 C2 都是可满足的，我们可以推断： ```plaintext ⟨Append, γ, C12⟩⊢UF (a(L1, L2, M)∧a(M, L3, L), w1) ⇒{L1,L2,L3,L} (a(L2, L3, R)∧a(L1, R, L), w2) ``` 其中 C12 是集合 `{w1 + u1 ≥w2 + u1, u8 ≥u9} ∪C1 ∪C2`。通过消除仅在定律 (α) 的证明中出现的未知数 `u8` 和 `u9`，并进行一些简单的简化，我们得到约束集合 C：`{u1 ≥1, u2 ≥1, w1 ≥w2, w2 + u1 ≥1}`。 这种方法的新颖之处在于，与其他方法不同，它会为每个需要证明正确性的转换序列自动生成特定的子句度量，而不是像某些方法那样提前固定子句度量。为了更准确地比较，进行了一些实际实验。该方法在 MAP 转换系统中实现，使用 SICStus Prolog (v. 3.12.5) 运行，并使用 clpq SICStus 库来检查约束集合在自然数上的可满足性。实验结果表明，即使是最复杂的推导，系统也能在毫秒内检查转换的完全正确性。 #### CoreTuLiP信任管理系统 CoreTuLiP 是一种基于逻辑编程的信任管理语言的核心。它基于模式化逻辑编程的一个子集，但具备 RT 等信任管理语言的特性，特别是子句由不同的权威机构发布并以分布式方式存储。 ##### 逻辑程序基础 在介绍 CoreTuLiP 之前，先了解一些逻辑程序的基础知识。这里主要涉及无函数（类似 Datalog）的逻辑程序。原子用 A、B、H 等表示，查询用 A、B、C 等表示（查询是原子的合取，可能为空），子句用 c、d 等表示，程序用 P 表示，空查询用 □ 表示。 模式化程序中，模式表示关系的参数应该如何使用，即每个原子的输入和输出位置。对于一个 n 元谓词符号 p，模式是一个从 `{1, ..., n}` 到 `{In, Out}` 的函数。如果 `mp(i) = In`（或 `Out`），则称 i 是 p 的输入（或输出）位置。程序需要是良模式的，即要满足一些将输入参数与输出参数相关联的正确性条件。 例如，一个子句 `H ←B1, ..., Bn` 是良模式的，需要满足： - 对于 `∀i ∈[1, n]`，`VarIn(Bi) ⊆ ∪i−1j=1 VarO