Page 17 - 《软件学报》2025年第9期

3928 软件学报 2025 年第 36 卷第 9 期

证明: 由 poloc 的非对称性可证.
定理 3 (RR 模式). ∀a,b∈R, perloc(a,b)→¬perloc(b,a) .
证明: 根据表 3, 将目标替换为已知 poloc(a,b), 求证¬poloc(b,a). 由引理 2 可证.
引理 3. ∀a,b∈E, fr(a,b)→¬poloc(b,a).
证明: 已知 fr(a,b) 证明¬poloc(b,a).
(1) 反证法. 假设 poloc(b,a) 成立.
(2) 由已知条件 fr(a,b) 以及 fr 的定义可得: ∃x∈E, rf(x,a)∧co(x,b). 其中, b∈W∧x∈W.
(3) 由公理 4 可知: rf(x,a)→∄y∈W, loc(y,a)∧gmo(x,y)∧(po(y,a)∨gmo(y,a)).
(4) 由 co 的定义可知: co(x,b)→gmo(x,b).
(5) 由 (1) 中假设条件 poloc(b,a) 以及 poloc 定义可知: po(b,a)∧loc(b,a).
(6) 由 (4) 和 (5) 可知: loc(b,a)∧gmo(x,b)∧po(b,a). 结合 (2)、(3) 和 (4) 推出矛盾. 得证.
引理 4. ∀a,b∈E, rf(a,b)→¬fr(b,a).
证明: 已知 rf(a,b) 证明¬fr(b,a).
(1) 反证法. 假设 fr(b,a) 成立.
(2) 由 (1) 以及 fr 的定义可得: ∃ x∈E, rf(x,b)∧co(x,a).
(3) 由公理 2 以及 rf(a,b) 可知: ∄x∈E, x≠a∧rf(x,b). 与 (2) 推出矛盾. 得证.
引理 5. ∀a,b∈E, rf(a,b)→¬poloc(b,a).
证明: 已知 rf(a,b) 证明¬poloc(b,a).
(1) 反证法. 假设 poloc(b,a) 成立.
(2) 由 rf(a,b) 可知: a∈W, b∈R. 由 (1) 中假设 poloc(b,a) 可知: ppo1(b,a).
(3) 由 (2), ppo 的定义以及公理 2 可得: gmo(b,a), 又由 gmo 的非对称性可知: ¬gmo(a,b).
(4) 由 rf(a,b) 以及公理 4 可知: po(a,b)∨gmo(a,b).
(5) 由 (1) 中假设 poloc(b,a) 可知: po(b,a). 由 po 关系的非对称性可知: ¬po(a,b).
(6) 由 (3)、(4) 和 (5) 推出矛盾.
定理 4 (RW 模式). ∀a∈R, ∀b∈W, perloc(a,b)→¬perloc(b,a) .
证明: 根据表 3, 将目标替换为: 已知 poloc(a,b)∨fr(a,b), 求证¬poloc(b,a)∧¬rf(b,a).
(1) 由引理 2 和引理 5 的逆否命题可知: poloc(a,b)→¬poloc(b,a)∧¬rf(b,a).
(2) 由引理 3 和引理 4 的逆否命题可知: fr(a,b)→¬poloc(b,a)∧¬rf(b,a).
(3) 由 (1) 和 (2) 可知: poloc(a,b)∨fr(a,b)→¬poloc(b,a)∧¬rf(b,a). 得证.
引理 6. ∀a,b∈E, fri(a,b)→poloc(a,b).
证明: 已知 fri(a,b) 证明 poloc(a,b). 由 fri 的定义可知: int(a,b)∧loc(a,b), 这里只证明 po(a,b). 又因为 int(a,b) 以
及 po 定义的推论, 将证明目标转为¬po(b,a).
(1) 反证法. 假设 po(b,a) 成立.
(2) 由 (1)、loc(a,b) 以及 loc 的对称性可得: poloc(b,a).
(3) 由引理 3: fr(a,b)→¬poloc(b,a). 由 fri 的定义以及 (2) 推出矛盾.
引理 7. ∀a,b∈E, rfi(a,b)→poloc(a,b).
证明: 已知 rfi(a,b) 证明 poloc(a,b). 由 rfi 的定义可知: int(a,b)∧loc(a,b), 这里只证明 po(a,b). 又因为 int(a,b) 以
及 po 定义的推论, 将证明目标转为¬po(b,a).
(1) 反证法. 假设 po(b,a) 成立.
(2) 由 (1) 以及 loc 的对称性可得: poloc(b,a).
(3) 由 (2)、ppo1 的定义以及公理 2 可得: gmo(b,a).
(4) 由 rfi(a,b) 以及公理 4 可得: po(a,b)∨gmo(a,b).