归结反演

应用归结原理证明定理

步骤：

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$ 空子句
结论得证。