第二章 归结推理方法

　　2.4.3 归结推理过程
　　为证明├A→B，其中A，B是谓词公式。使用反演过程，先建立
　　　　G＝A∧～B
　　进而做出相应的子句集S，只需证明S是不可满足的。
　　归结法是仅有一条推理规则的推理方法。对S中的可归结的子句做归结，求得归结式，并将这归结式（新子句）仍放入S中，反复这个归结过程直至产生空子句□为止。这时S必是不可满足的。从而├A→B得证。
　　因为□的出现，必是S中或归结式加入S后同时出现子句P与～P所致。由于∧R(,)所以这个矛盾的原因必在S，或说S本身有矛盾，也就是S必是不可满足的。
例题 例1:
  　证明 (x)(A(x)→(B(x)∧C(x))∧(x)(A(x)∧D(x))
　　　　　　　　→(x)(D(x)∧C(x))
　使用归结法的证明步骤。
　第一步：使用反演法，先写出公式G：
　(x)(A(x)→(B(x)∧C(x)))∧(x)(A(x)∧D(x))∧～(x)(D(x)∧C(x)
　第二步：将G的各合取项分别化成SKOLEM标准形，得子句集{S1,S2,S～B}。
　　(x)(A(x)→(B(x)∧C(x)))
　　=(x)(～A(x)∨(B(x)∧C(x)))
　　=(x)((～A(x)∨B(x))∧(～A(x)∨C(x)))
　S1={～A(x)∨B(x),～A(x)∨C(x)}
　对(x)(A(x) ∧ D(x))有
　S2={A(a),D(a)}
　　　～(x)(D(x) ∧C(x))
　　=(x)(～D(x) ∧ C(x))
　　=(x)(～D(x) ∨ ～C(x))
　S～B={～D(x)∨～C(x)}
　从而得子句集
　S={～A(x)∨B(x),～A(x)∨C(x),A(a),D(a),～D(x)∨～C(x)}
　第四步 使用归结规则建立推理过程
　（1）～A(x)∨ B(x)
　（2）～A(x)∨C(x)
　（3）A(a)
　（4）D(a)
　（5）～D(x)∨～C(x)
　（6）C(a) 　　　　　　(2)(3)归结
　（7）～C(a) 　　　　　(4)(5)归结
　（8）□ 　　　　　　　(6)(7)归结
　2.2.5节的例子，已建立了相应的子句集了，可直接使用归结推理规则了。
例题 例2:
  　证明梯形的对角线与上下底构成的内错角相等。
　（1）～T (x,y,u,v) ∨P(x,y,u,v)
　（2）～P(x,y,u,v) ∨ E(x,y,v,u,v,y)
　（3）T(a,b,c,d)
　（4）～E(a,b,d,c,d,b)
　（5）～P(a,b,c,d) 　　　　(2)(4)归结
　（6）P(a,b,c,d) 　　　　　(1)(3)归结
　（7）□　　　　　　　　　 (5)(6)归结
例题 例3:
  　猴子香蕉问题
　（1）～P(x,y,z,s) ∨ P(z,y,z,walk(x,z,s))
　（2）～P(x,y,x,s) ∨ P(y,y,y,Carry(x,y,s))
　（3）～P(b,b,b,s) ∨R(Climb (s))
　（4）P(a,b,c,s)
　（5）～R(s) ∨ ANS(s)
　（6）～P(b,b,b,s) ∨ ANS(Climb(s))　(3)(5)归结
　（7）～P(x,b,x,s) ∨ANS(Climb(Carry(x,b,s))) (2)(6)归结
　（8）～P(x,b,z,s) ∨ANS(Climb(Carry(z,b,walk(x,z,s)))) (1)(7)归结
　（9）□∨ANS(Climb(Carry(c,b,walk(a,c,s)))) (4)(8)归结
　于是猴子吃香蕉的问题的答案是
　　　Climb (Carry(c,b,walk(a,c,s)))
例题 例4:
  　若A，B为两个集合，试证明
　　　A∩BA
　先写出逻辑描述，建子句集，再使用归结推理过程。
　A1：(x)(A)(B)(x∈A∧x∈B←→x∈A∩B)
　S1：{ xA∨xB∨x∈A∩B,x∈A∨xA∩B,x∈B∨xA∩B}
　A2：(A)(B)(x)(x∈A→x∈B)←→AB)
　S2：{ xA∨x∈B∨AB,f(A,B)∈A∨AB,f(A,B)B∨AB}
　～B：～( A)( B)(A∩BA)
　S～B：C∩DC
　证明
　（1）xA∨xB∨x∈A∩B
　（2）x∈A∨xA∩B
　（3）x∈B∨xA∩B
　（4）xA∨x∈B∨AB
　（5）f(A，B)∈A∨AB
　（6）f(A,B)B∨AB
　（7）C∩DC
　（8）f(C∩D,C)∈C∩D (5)(7)归结
　（9）f(C∩D,C)C (6)(7)归结
　（10）f (C∩D,C)∈C　(2)(8)归结
　（11）□　　　　　　 (9)(10)归结