数理逻辑（讲义）(4)

A?(B?C),A?B?A?C

A?(B?C),A?B,A?CA?(B?C),A?C,A

A?(B?C),A,B?C

A,B?A,C

A,B,(B?C)?C

A,B?C,B

A,B,C?C

二、表方法

原理： 将A1?......?An)?B]为重言式。 1,......,An|?B的证明转换为证明[(A标记公式：F.?（指：公式?取假） T.?（指：公式?取真） 根结点：F.[(A1?......?An)?B]

指：假定公式[(A1?......?An)?B]取假。

分解规则：（逐步取消联结词。如果己出现矛盾路径，则不再分解）

15

T.??

F.??

F.?

T.?

F.???

T.???

F.?

T.?

T.?

F.?

T.???

F.???

T.?

F.?

F.?

T.?

16

F.???

T.???

T.?

F.?T.?

F.?

T.???

F.???

T.?

F.?

T.? F.?

T.?

F.?

F.?

T.?

矛盾路径：从根到叶结点的路径上出现矛盾对T.A, F.A。 终结树：每一叶结点路径上或出现矛盾，或不可再分解。 矛盾树：每条路径均为矛盾路径。

17

F.[((A?(B?C))?(A?B))?(A?C)] 待递归分解 T.[(A?(B?C))?(A?B)] F.(A?C) T.A

F.C

18

形式推理与证明

推理规则系统: (Ref)： A|?A.

(单调)：若 ?|?A，???'，则?'|?A。

(??)：若 ?,?A|?B，?,?A|??B，则?|?A。 (??)：若 ?|?A?B,?|?A，，则?|?B。 (??)：若 ?,A|?B，则?|?A?B。 (??)：若 ?|?A?B，则?|?A,?|?B。 (??)：若 ?|?A,?|?B，则?|?A?B。 (??)：若 ?,A|?C,?,B|?C,则?,A?B|?C。 (??)：若 ?|?A，则?|?A?B,?|?B?A。 (??)：若 ?|?A?B,?|?A,则?|?B。 若 ?|?A?B,?|?B,则?|?A。 (??)：若 ?,A|?B,?,B|?A，则?|?A?B。

补：(12) (?) ： 若A??，则?|?A。(可由Ref和单调性证明) 形式化推理：?|?A

设A?Form(LP)，??Form(LP)。称A可由?形式化可推理。如果存在一个序列：

?1|?A1,?2|?A2,........,?n|?An满足如下条件： (1) ?1|?A1 (使用 (?) 或(Ref)引入)； (2) ???n,A?An；

(3) 对每一个1?k?n，?k|?Ak由下列情形之一引入： (3.1) 使用 (?)，

(3.2) 使用(Ref)， (3.3) 使用其它规则.

19