归结反演

应用归结原理证明定理

步骤：

1. 将一直前提表示为谓词公式 F。
2. 将待证明的结论表示为谓词公式 Q，并否定得到 \neg Q。
3. 把谓词公式集 {F,\neg Q} 化为子句集 S。
4. 应用归结原理对子句集 S 中的子句进行归结，并把每次归结得到的归结式都并入到 S 中。如此反复进行，若出现了空子句，则停止归结，此时就证明了结论 Q 为真。

例 1： 某公司招聘工作人员，A,B,C 三人应试，经面试后公司表示如下想法：

• 三人中至少录取一人。
• 如果录取 A 而不录取 B, 则一定录取 C。
• 如果录取 B, 则一定录取 C.

求证：公司一定录取 C。

Proof: (1) 将公司想法用谓词公式表示：P(x): 录取 x 前提：

• P(A) \vee P(B)\vee P(C)
• P(A) \wedge \neg P(B) \rightarrow P(C)
• P(B) \rightarrow P(C)

待证结论：P(C)

(2) 将待证结论否定得：\neg P(C) (3) 将谓词公式集 {P(A) \vee P(B)\vee P(C),P(A) \wedge \neg P(B) \rightarrow P(C),P(B) \rightarrow P(C)} 化成子句集： S={P(A) \vee P(B)\vee P(C),\neg P(A) \vee P(B) \vee P(C),\neg P(B) \vee P(C),\neg P(C)} (4) 应用归结原理进行归结 C_1=P(A) \vee P(B)\vee P(C), C_2=\neg P(A) \vee P(B) \vee P(C), C_3=\neg P(B) \vee P(C), C_4=\neg P(C) 归结： C_1 \otimes C_2 = C_12=P(B)\vee P(C) C_3 \otimes C_12 = C_123 = P(C) C_4 \otimes C_123 = C_1234 = NIL 空子句 结论得证。

归结反演

例 2： 已知： 规则 1：任何人的兄弟不是女性 规则 2：任何人的姐妹必是女性 事实：Mary 是 Bill 的姐妹 求证：Mary 不是 Tom 的兄弟

(1) 谓词表示： brother(x,y): x 是 y 的兄弟 sister(x,y): x 是 y 的姐妹 woman(x): x 是女性

规则 1：\forall x \forall y(brother(x,y)\rightarrow \neg woman(x)) 规则 2：\forall x\forall y(sister(x,y)\rightarrow woman(x)) 事实：sister(Mary,Bill) 待证结论：\neg brother(Mary,Tom)

(2) 将待证结论否定得：brother(Mary,Tom) (3) 谓词公式集 {\forall x \forall y(brother(x,y)\rightarrow \neg woman(x)),\forall x\forall y(sister(x,y)\rightarrow woman(x)),sister(Mary,Bill),\neg brother(Mary,Tom)} 化成子句集： S= { C_1=\neg brother(x,y)\vee \neg woman(x), C_2=\neg sister(x,y)\vee woman(x), C_3=sister(Mary,Bill), C_4=brother(Mary,Tom) }

(4) 应用归结原理进行归结： C_23=woman(Mary) C_123=\neg brother(Mary,y) C_1234=NIL 空子句 结论得证。