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