时态逻辑课件幻灯片.ppt

谓词逻辑中的推论规则 ⒋取代规则： 设A’(x1, x2, …,xn) ? B’(x1, x2, …,xn)都是含n个自由变量的谓词公式，且A’是A的子式。若在A中用B’取代A’的一处或多处出现后所得的新公式是B ，则有A ? B 。如果A是永真公式，则B也是永真公式。 谓词逻辑中的推论规则 ⒌全称规定规则US： 从?xA(x)可得出结论A(y)，其中y是个体域中任一个体。即， ?xA(x) ? A(y) 使用US规则的条件是对于y，公式A(x)必须是自由的。根据US规则，在推论过程中可以移去全称量词。 谓词逻辑中的推论规则 ⒍存在规定规则ES： 从?xA(x)可得出结论A(y)，其中y是个体域中某一特殊个体。即， ?xA(x) ? A(y) 使用ES规则的条件是y必须在以前没有出现过的，以避免发生混淆。即， ①在给定的所有前提中，y都不是自由的。②在以前的任何推导步骤上，y也不是自由的。根据ES规则，在推论过程中可以移去存在量词。 谓词逻辑中的推论规则 ⒎存在推广规则EG： 从A(x) 可得出结论?yA(y) ，其中x是个体域中某一个体。即， A(x) ? ?yA(y) 使用EG规则的条件是对于y，公式必须是自由的。根据EG规则，在推论过程中可以附上存在量词。 谓词逻辑中的推论规则 ⒏全称推广规则UG： 从A(x) 可得出结论?yA(y) ，其中x应是个体域中任一个体。即， A(x) ? ?yA(y) 使用UG规则的条件是：①在任何给定前提中，x都不是自由的。②在使用ES规则而得到的一个以前步骤上，如果x是自由的，则由于使用ES规则而引入的任何新变量在A(x)中都不是自由出现。根据UG规则，在推论过程中可以附上全称量词。 Peterson算法 Var turn : integer; enter1, enter2 : boolean; turn := 1; enter1 := enter2 := false; cobegin P1 :: repeat enter1 := true; turn := 2; While enter2 and turn = 2 do ; 互斥部分； enter1 := false; 非互斥部分； forever; P2 :: repeat enter2 := true; turn := 1; While enter1 and turn = 1 do ; 互斥部分； enter2 := false; 非互斥部分； forever; coend Peterson算法框图 Peterson算法的安全性和活动性 【证明】 我们必须证明 ⑴进程P1和P2不能同时进入互斥 部分，即成立□~(at ?4 ? at ?4) ⑵假定在进入临界区后，有限时 间区边内都能释放，则从入口点 开始，进程最终一定能进入互斥 部分，即成立 Peterson算法的安全性和活动性 at ?1 ? ◇at ?4 at ?1 ? ◇at ?4 首先，我们证明□~(at ?4 ? at ?4)。 反证法。假定~(□~(at ?4 ? at ?4)) ? ◇(at ?4 ? at ?4) 由程序框图知成立下面两式： at ?4?enter1?(~enter2?(turn=1)) 和at?4?enter2?(~enter1?(turn=2))， Peterson算法的安全性和活动性 即at ?4 ? at ?4 ? enter1?(~enter2?(turn=1)) ?enter2?(~enter1?(turn=2))，（式1） 令 P?enter1,Q ?enter2, R?(turn=1),则~R ? (turn=2), （式1）变为 Peterson算法的安全性和活动性 at ?4 ? at ?4 ? P?(~Q?R)?Q?(~P?~R)， 但是 P?(~Q?R)?Q?(~P?~R) ?P?((~Q?Q)?(R?Q))?~(P?R) ?P?(false?(R?Q))?~(P?R) ?P?R?Q?~(P?R)?false， 因此，◇False，导致矛盾。⑴得证。 Peterson算法的安全性和活动性 其次，证明⑵。 只要证明at ?1?◇at ?4就可以， 另一个类似。 反证法。假定 ~(at ?1 ?◇at ?4) ? at ?1?~◇at ?4 ? at ?1?□~at ?4。 我们证明成立下面（式2） (at ?1?□