高级数理逻辑第7讲

  • 格式:doc
  • 大小:347.96 KB
  • 文档页数:10

5.5 归结策略归结算法:::用归结原理来证明定理,我们最终倒出空子句。

怎么样最快的得到空子句是我们考虑的最主要问题。

如果人用归结的方法,得到空子句通常是根据人们对子句集中子句的认识,可以最快的得到空子句。

然而,归结原理的主要思想是用机械的方法使计算机能够快速得到空子句。

这需要我们考虑高效的计算算法来提高得到空子句的效率。

本节主要目的是给出各种得到空子的算法,这些算法都从不同角度提高了得到空子句的归结效率。

这些算法又称作为归结策略。

5.5.1 宽度优先宽度优先是归结策略中最简单的算法。

下图说明了,宽度优先策略的主要思想:S 将S 重所有能归结的子句间都归结S 1归结产生的子句集S ∨S 1 将归结产生的子句集与原子句集析取 将S ∨S 1与S 1上能归结的子句间都归结S 2 归结产生的子句集┆ 重复以上过程□这样的归结过程中,有大量的冗余存在。

因为,在每个归结步骤中,将有所能够归结的子句之间都归结,从而避免不了产生大量多余的归结步骤。

例如:对于子句集{P ⌝,Q P ∨,Q P ⌝∨,Q P ⌝∨⌝},宽度优先归结策略将产生以下步骤完成:{Q,~Q,~P,P }(1) 对子句集中,能够归结的子句之间进行归结。

归结产生的子句集为:{Q ⌝,Q ,Q Q ∨⌝,P P ∨⌝,Q Q ⌝∨⌝}(2) 将归结得到的子句集与原子句集合并得到{P ⌝,Q P ∨,Q P ⌝∨,Q P ⌝∨⌝,Q ⌝,Q ,Q Q ∨⌝,P P ∨⌝,Q Q ⌝∨⌝},与{Q ⌝,Q ,Q Q ∨⌝,P P ∨⌝ }子句进行归结。

(3) 在进行归结得到{□,…}.这个归结过程中存在了Q Q ∨⌝,P P ∨⌝两个多余的归结步骤。

虽然,这种归结的方法存在了大量的冗余归结步骤,但是这个归结能够保持归结的完备性。

既对于不能满足的子句集,一定能够得到空子句。

5.5.2 删除策略为了提高归结的效率,我们首先考虑的是按着宽度优先方法得到各个归结集合之间的关系。

也就是考虑那些归结步骤是没有用的。

首先,任何子句与重言式都不可能归结出空子句。

因此,对于重言式没有必要考虑其与其他子句之间的归结。

其次,设子句11P c =,212P P c ∨=,对于子句3c 能够与2c 得到逻辑结果c4,A →{c1^c2}如果赋值映射f ,使得f(C2)=f(C3)=1,则f(C4)=1。

如果赋值映射f ,使得f(C1)=f(C3)=1, f(C4)=1则一定是1c 和3c 归结结果;并且3c 与1c 归结序列的长度一定小于3c 与2c 归结序列的长度。

{11P c =,212P P c ∨=}用数学的方法来表述以上的观点:● 设子句集{}n c c c S ......21=不可满足,若i c 为重言式,{}i c S -为不可满足,反之成立;{C1,-1,Cn=1}=C1&C2,…&Cn-1= { C1,-1}● 设子句集{}n c c c S ......21=不可满足,若j i c c ⊆θ中,(称i c 嵌入到j c 中)θi c →j c ,则{}j c S -为不可满足的,反之成立;C1<=C2{C1,C2,…Cn}=C1^C3…^Cn=0;;;; C1&C3…&Cn=0S 是不可满足的充分必要条件S-Ci 是不可满足。

根据这两点,我们可以从宽度优先归结策略中删除一些没有必要的步骤,从而提高归结的效率。

这种方法,我们称之为删除策略。

对于给定的子句集S ,删除策略我们可以表述如下:1、 在S 中将可被嵌入的子句删除得到子句集1S ;2、 对1S 中可以归结的子句之间进行归结得到2S ;3、 将21S S ∨中的重言式和可被嵌入的子句删除得到3S ;4、 3S 上的子句进行归结;5、 重复以上过程,最终得到空子句。

删除策略同样是完备的,主要是因为删除后的子句集与原子句集是同不可满足的。

下面例子说明了删除策略的过程:例子:对于子句集,(1))()()(x R x Q x P ⌝∨∨(2))(a Q ⌝(3))()(a Q a R ∨⌝(4))(y P(5))()(z R z P ∨⌝step1:删除(1),因为(1)可被(4)嵌入;得到S 1={2, 3, 4, 5};step2:在S 1上归结,得到)()6(a R ⌝ (2,3)(7)~P(a)vQ(a)(8))(z R (4,5) {}8,7,6,5,4,3,21=∨S Sstep3:在S 1∨S 中删除(3)可被(6)嵌入,删除(5)可被(7)嵌入;{}8,7,6,4,22=Sstep4:在S 2中,(6),(8)归结 {□};S 是不可满足的,用删除策略是否一定能找到空子句?5.5.3 支持集策略我们知道人们在进行子句的归结时候,主要是通过感觉上,那些子句之间有可能产生空子句来归结,从而效率非常高。

支持集策略从人们在归结时的一些想法出发,首先把子句集进行划分。

划分成支持集和非支持集两个部分。

空子句一定是由支持集中的子句参与得到的。

● 定义:设子句集S 为不可满足的,如果S T ⊂,且集合T S -是可满足,则称子句集T 为子句集S 的支持集。

● 支撑集策略:在S 中求导出空子句的归结序列时,在每一归结母式中至少有一个子句不在T S -中。

意味着,可以在T 中或者归结结果中。

● 支持集策略,也是一种完备的归结策略。

即对于不可满足的子句集S ,利用支持集策略一定能够得到空子句。

下面通过一个例子来说明支持集策略的使用。

例子:对于以下给定的子句集,利用支持集策略进行归结。

(1)),),,((1111y x y x f P(2))),,(,(2222y y x g x P ⌝(3)),,(),,(),,(),,(333333333333w z u P w v x P v z y P u y x P ∨⌝∨∨⌝(4)))(,),((444x h x x h P ⌝我们可以看出(4),(2),(3)是可以满足的,因此(1)为支持集。

根据支持集粗略,得到:(5)))(,,(),,())(,,(333333333z h v x P v z y P z h y x P ⌝∨∨⌝ 在(4)(3)中利用43/x z 和3343/)(,/)(u z h w z h ,并归结得到。

对(5)进行33/y v 得到),,())(,,(333333v z v P z h v x P ∨⌝;(6))),((,,(3333v y g h v x P ⌝,对(2)进行2323/,/y v x y 后)),,(,(3333v v y g y P ⌝;对(5)进行333/),(z v y g 后得到)),,(,())),((,,(33333333v v y g v P v y g h v x P ∨⌝;归结后得到的。

(7)通过合一131313311/)),((,/,/))),((,(y v x g h y x x v x g h x f 得到(1)和(6)归结的空子句。

5.5.4 线性策略线性归结是指除第一次归结外,其它各次归结中,至少有一个母式是上次的归结结果。

线性归结是完备的,即对于不可满足的子句集S ,用线性归结的方法一定可以得到空子句。

练习,利用归结原理证明,以下的子句集是不可满足的。

)()()7()()()6()(),()5()()4()()3())(()()()2())(,()()()1(x c x P x v x P y P y a w a E a P x f C x v x E x f x w x v x E ⌝∨⌝⌝∨⌝∨⌝∨∨⌝∨∨⌝以上的四种归结策略都是完备的归结策略。

实际上,为了提高归结的效率,还有其他不完备的归结策略,如:锁归结、输入归结、单位归结等。

在此并不详细叙述,感兴趣的同学参见王元元的书。

5.6 归结原理应用归结原理在计算机科学中,有着非常广泛的应用。

目前来说归结原理主要有四个方面的主要应用:(1) 定理证明:对于给定的公理系统证明一个公式是否为定理。

是一个是非性的答案。

例如,几何定理的机器证明等。

(2) 问题解决:问题解决(Problem Solving )是人工智能中的一个主要问题。

这时待证的定理通常是)(x xA 是否成立。

给出答案通常为:“是,x= ”或者为“否”;(3) 程序分析验证:分析和验证程序是否能够给出预定的结果。

主要的应用方面是航天航空等,而非商业程序。

(4) 规划生成:根据给出的目标,规划出一系列步骤。

实际上,是对于给定的定理,找到他的归结序列的过程。

目前被应用到智能主体的行为规划上。

目前在(2)和(4)中更多地采用基于数据处理的方法;或者称为机器学习的方法来解决。

产生这样转变得原因主要有两个:(1) 信息时代的突出特点是数据多,这些数据中有成功的,也有失败的。

对于同样的方法,即可能对于某些案例是成功的,而对于另外一些反而是失败。

因此,人们更愿意从大量数据中蕴涵的道理来确定解决方案。

(2) 逻辑的方法总是非常严格,给出了非常具体的答案(非白即黑)。

因此,很难让人接受。

例如,天气预报说下雨是非常肯定的答案,但是没有下的话就使大家陷入的尴尬的境地。

因此,人们更喜欢概率和数据挖掘的方法。

这样给出的答案总是带有一定的不确定性。

对于这类方法中,目前主要热门的Learning Bayes Network ,例如微软的Windows XP 中就重点使用了这种技术,也就是说,以后对Windows XP 出现的任何问题,人们都得不到的确切的回答。

得到只是,某种情况的可能性最大,某种方法的有效性最高等。

目前数据处理的方法,比逻辑分析的方法来说,占有极大的优势。

不单个大公司都在推崇数据处理分析方法-例如Intel 中国研究院的一个重点任务就是研究Learning Bayes Network ,而且这种方法也越来越多地被人们接受-主要的原因是比逻辑分析方法更容易掌握。

也许不久能够出现一种,将逻辑分析与数据分析结合起来的方法;但这种方法绝对不是目前的模糊逻辑和模糊系统等方法。

A(X)→B(x)B(Y)→(XXXXX)RETE →规则引擎→Ilog →Drools5.7 HORN 子句程序设计子句集是一种标准的形式,利用计算机可以在这样的子句集上进行推理。

要形成计算机程序来进行逻辑推理,重要的一条就是让人们在理解和使用的时候,非常方便,也就是高级程序设计语言的基本要求。

人类在推理时,总是分成条件结论等。

而子句集淡化这些概念,从而使人难于理解。

HORN 子句正是解决这样的问题。

HORN 子句是一种逻辑程序设计语言。

5.7.1 HORN 子句定义:子句n P P P ∨∨∨ 21中,如果至多只含有一个正文字,那么称该子句为HORN 子句。