首页 百科知识 证明的实例

证明的实例

时间:2022-08-23 百科知识 版权反馈
【摘要】:第一个是来自第9.3节的犯罪例子。我们的第二个实例利用了 Skolem 化并涉及非确定子句。不幸的是,归结对于存在目标可能生成非构造性证明。注意,在该证明中,w具有两种不同的绑定;归结告诉我们:是的,某人杀害了Tuna——可能是Jack也可能是Curiosity。非构造性证明可能会生成子句Answer∨Answer,该子句无法构成一个解。

9.5.3 证明的实例

归结通过证明KB∧¬α 不可满足,也就是通过导出空语句,来证明Kb|= α 。这个算法所采用的方法和如图7.12所描述的命题逻辑的情况是完全一样,所以我们这里不再重复它,而是给出两个证明的实例。第一个是来自第9.3节的犯罪例子。CNF语句为

¬American(x)∨¬Weapon(y)∨¬Sells(x,y,z)∨¬Hostile(z)∨Criminal(x).

¬Missile(x)∨¬Owns(Nono,x)∨Sells(West,x,Nono).

¬Enemy(x,America)∨Hostile(x).

¬Missile(x)∨Weapon(x).

Owns(Nono,M1).    Missile(M1).

American(West).    Enemy(Nono,America).

我们把否定目标¬Criminal(West)也包含在CNF语句中。归结证明如图9.11所示。注意这个结构:从目标子句开始的单一“骨干”,与来自知识库的子句相归结,直到产生空子句。这是霍恩子句知识库上的归结特征。实际上,主要骨干上的子句恰好和图 9.6 中反向链接算法的目标变量的相继值对应。这是因为我们总是选择正文字能和骨干上“当前”子句最左边的文字合一的子句参与归结;这正是在反向链接中发生的情况。因此,反向链接实际上只是在归结方法的特殊情况,它使用特殊控制策略以决策下一步将执行的归结。


图9.11 West是个罪犯的归结证明

我们的第二个实例利用了 Skolem 化并涉及非确定子句。这就造成了一个多少有点复杂的证明结构。用英语来表示,该问题可以表示成:

Everyone who loves all animals is loved by someone.

Anyone who kills an animal is loved by no one.

Jack loves all animals.

Either Jack or Curiosity killed the cat, who is named Tuna.

Did Curiosity Kill the cat?

(爱所有动物的人被某个人爱着。

任何杀了动物的人没有人爱。

Jack爱所有的动物。

Jack和Curiosity其中的一个人杀死了那只名叫Tuna的猫。

是Curiosity杀害了那只猫吗?)

首先,我们将这些原始语句、某些背景知识和目标G的否定用一阶逻辑形式表达:


D. Kills(Jack,Tuna) ∨ Kills(Curiosity,Tuna)

E. Cat(Tuna)

¬G. ¬Kills(Curiosity,Tuna)

现在我们利用转换过程将每个语句转换成CNF:

A1. Animal(F(x)) ∨ Loves(G(x),x)

A2. ¬ Loves(x,F(x)) ∨ Loves(G(x),x)

B. ¬Animal(y) ∨ ¬Kills(x,y) ∨ ¬Loves(z,x)

C. ¬Animal(x) ∨ Loves(Jack,x)

D. Kills(Jack,Tuna) ∨ Kills(Curiosity,Tuna)

E. Cat(Tuna)

F. ¬Cat(x) ∨ Animal(x)

¬G. ¬Kills(Curiosity,Tuna)

Curiosity杀了那只猫的归结证明如图9.12所示。在自然语言中,证明可以释义成:

假设Curiosity没有杀害Tuna。我们知道不是Jack就是Curiosity做的;因此一定是Jack干的。现在,Tuna是一只猫,而猫是动物,所以Tuna是一只动物。因为杀了动物的任何人没有人爱,那么我们知道没有人爱Jack。另一方面,Jack喜爱所有的动物,因此一定有某人爱他;如此,就出现了矛盾。所以,是Curiosity杀害了那只猫。

证明解答了问题“是 Curiosity 杀害了那只猫吗?”,但是我们经常想提出更一般的问题,如“是谁杀害了那只猫?”。归结可以做到这一点,但是它需要做更多工作才能得到答案。目标为∃w Kills(w, Tuna),它的CNF否定式为¬Kills(w,Tuna)。对这个新的否定目标重复图9.12的证明,我们得到一棵类似的证明树,但是在某一步骤中增加了置换{w / Curiosity}。所以,在这种情况下,找出是谁杀害了那只猫只需要记录证明过程中查询变量的绑定情况。

不幸的是,归结对于存在目标可能生成非构造性证明。例如,¬Kills(w, Tuna)与Kills(Jack, Tuna)∨Kills(Curiosity, Tuna)归结得到Kills(Jack, Tuna),而Kills(Jack, Tuna)再次和¬Kills(w, Tuna)归结将得到一个空子句。注意,在该证明中,w具有两种不同的绑定;归结告诉我们:是的,某人杀害了Tuna——可能是Jack也可能是Curiosity。这没什么可大惊小怪的!一个解决方案就是限制允许的归结步骤,这样在给定的证明中,查询变量只能绑定一次;那么我们需要有能力回溯可能的绑定。另一个解决方案是给否定目标增加特殊的解文字,使其变成¬Kills(w, Tuna)∨Answer(w)。至此,每生成一个只包含单个解文字的子句,归结过程就生成一个答案。对图9.12中的证明,解就是Answer(Curiosity)。非构造性证明可能会生成子句Answer(Curiosity)∨Answer(Jack),该子句无法构成一个解。


图9.12 Curiosity杀害了那只猫的归结证明。注意在子句Loves(G(Jack),Jack)的推导中对归并的使用

免责声明:以上内容源自网络,版权归原作者所有,如有侵犯您的原创版权请告知,我们将尽快删除相关内容。

我要反馈