分辨率证明 - 人工智能

Proof by resolution - Artificial Intelligence

我正在做一个练习,我需要证明 KB |= ~D

我知道知识库是:

 - (B v ¬C) => ¬A
 - (¬A v D) => B
 - A ∧ C

转换为 CNF 后:

A ∧ C ∧ (¬A v ¬B) ∧ (¬A v C) ∧ (A v B) ∧ (B v ¬D)

所以现在我已经转换为 CNF,但是从那里开始,我不知道如何继续。将不胜感激任何帮助。谢谢!

一般的解决规则是,对于任何两个子句 (即文字的析取)

P_1 v ... v P_n

Q_1 v ... v Q_m

在你的 CNF 中有 i 和 j,P_i 和 Q_j 是彼此的否定, 你可以添加一个新的条款

P_1 v ... v P_{i-1} v P_{i+1} ... v P_n v Q_1 v ... v Q_{j-1} v Q_{j+1} ... v Q_m

这只是一种严格的说法,你可以通过连接其中的两个来形成一个新的子句,减去每个中带有相反 "signs" 的文字。

例如

(A v ¬B)∧(B v ¬C)

等同于

(A v ¬B)∧(B v ¬C)∧(A v ¬C),

通过加入两个子句同时删除对立的B¬B,得到A v ¬C.

另一个例子是

A∧(¬A v ¬C)

相当于

A∧(¬A v ¬C) ∧ ¬C.

因为 A 算作具有单个文字的子句(A 本身)。所以这两个子句被连接起来,而 A¬A 被删除,产生一个新的子句 ¬C.

将此应用于您的问题,我们可以解决 A¬A v ¬B,获得 ¬B。 然后我们用 B v ¬D 解析这个新子句 ¬B,得到 ¬D.

因为 CNF 是连词,它成立的事实意味着其中的每个子句都成立。也就是说,CNF 隐含了它的所有条款。由于 ¬D 是其子句之一,因此 CNF 隐含了 ¬D。由于CNF相当于原来的KB,所以KB隐含¬D.