归结反演

应用归结原理证明定理

步骤:

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

正文完
 
yhlin
版权声明:本站原创文章,由 yhlin 2023-01-19发表,共计1498字。
转载说明:除特殊说明外本站文章皆由CC-4.0协议发布,转载请注明出处。
评论(没有评论)
验证码