avatar

归结反演

应用归结原理证明定理

步骤:

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

文章作者: Liam
文章链接: https://www.ccyh.xyz/p/fba.html
版权声明: 本博客所有文章除特别声明外,均采用 CC BY-NC-SA 4.0 许可协议。转载请注明来自 屿
ღ喜欢记得五星好评哦~
打赏
  • 微信
    微信
  • 支付寶
    支付寶

评论