Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,计算机学院,*,计算机学院,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,归结法原理,马殿富,北航计算机学院,20,12-4,主要内容,机械证明简介,命题逻辑归结法,谓词逻辑归结法,自动推理早期的工作主要集中在机器定理证明。,机械定理证明的中心问题是寻找判定公式是否是有效的通用程序。,对命题逻辑公式，由于解释的个数是有限的，总可以建立一个通用判定程序，使得在有限时间内判定出一个公式是有效的或是无效的。,对一阶逻辑公式，其解释的个数通常是任意多个，丘奇（,A.Church,）和图灵（）在,1936,年证明了不存在判定公式是否有效的通用程序。,如果一阶逻辑公式是有效的，则存在通用程序可以验证它是有效的,对于无效的公式这种通用程序一般不能终止。,1930年希尔伯特（Herbrand）为定理证明建立了一种重要方法，他的方法奠定了机械定理证明的基础。,开创性的工作是赫伯特西蒙（H.A.Simon）和艾伦纽威尔（A.Newel）的 Logic Theorist。,机械定理证明的主要突破是1965年由鲁宾逊（）做出的，他建立了所谓归结原理，使机械定理证明达到了应用阶段。,归结法推理规则简单,而且在逻辑上是完备的,因而成为逻辑式程序设计语言Prolog的计算模型。,主要内容,机械证明简介,命题逻辑归结法,谓词逻辑归结法,基本原理,Q,1,Q,n,|=R,，当且仅当,Q,1,Q,n,R,不可满足,证明,Q,1,Q,n,|=R,(1).Q,1,Q,n,R,化为合取范式；,(2).,构建,子句集合，,为,Q,1,Q,n,R,合取范式的所有简单析取范式组成集合；,(3).,若,不可满足，则,Q,1,Q,n,|=R,。,机械式方法,若证明,Q,1,Q,n,|=R,，只要证明,Q,1,Q,n,R,不可满足。,机械式,证明：,公式,Q,1,Q,n,R,的合取范式,；,合取范式的所有简单析取范式,，即,；,证明,不可满足,则有,Q,1,Q,n,|=R,。,机械式地证明,不可满足是关键问题,子句与空子句,定义：原子公式及其否定称为文字,(literals),；文字的简单析取范式称为子句，不包含文字的子句称为空子句，记为。,例如,p,、,q,、,r,和,s,都是文字,简单析取式,p,q,r,s,是子句,字,p,、,q,、,r,和,s,因为,p,q,r,s,不是简单析取范式，所以,p,q,r,s,不是子句。,定义：设,Q,是简单析取范式，,q,是,Q,的文字，在,Q,中去掉文字,q,，记为,Q-q,。,例如，,Q,是子句,p,q,r,s,，,Q-,q,是简单析取范式,p,r,s,。,归结子句,定义：设,Q,1,Q,2,是子句，,q,1,和,q,2,是相反文字，并且在子句,Q,1,和,Q,2,中出现，称子句,(Q,1,-q,1,),(Q,2,-q,2,),为,Q,1,和,Q,2,的归结子句。,例如，,Q,1,是子句,p,q,r,，,Q,2,是子句,p,q,w,s,，,q,和,q,是相反文字，子句,p,r,w,s,是,Q,1,和,Q,2,的归结子句。,例如，,Q,1,是子句,q,，,Q,2,是子句,q,，,q,和,q,是相反文字，子句是,Q,1,和,Q,2,的归结子句。,例如，,Q,1,是子句,p,q,r,，,Q,2,是子句,p,w,s,，在子句,Q,1,和,Q,2,中没有相反文字出现，子句,Q,1,Q,2,，即,p,q,r,w,s,不是,Q,1,和,Q,2,的归结子句。,定理：如果子句,Q,是,Q,1,Q,2,的归结子句，则,Q,1,Q,2,|=Q,证明：,设,Q,1,=p,q,1,q,n,，,Q,2,=,p,r,1,r,m,。,赋值函数,(Q,1,)=1,，即,(p,q,1,q,n,)=1,，,(p),(q,1,q,n,)=1.,赋值函数,(Q,2,)=1,，即,(,p,r,1,r,m,)=1,，,(p),(r,1,r,m,)=1.,有,(q,1,q,n,r,1,r,m,)=1,，即,(Q)=1,。,证毕,反驳,定义：设,是子句集合，如果子句序列,Q,1,Q,n,满足,如,下条件，则称子句序列,Q,1,Q,n,为子句集合,的一个反驳。,(1).,对于每个,1,k,n,，,Q,k,Q,k,是,Q,i,和,Q,j,的归结子句，,ik,，,jk,。,(2).,Q,n,是。,例题：,(Q,R),Q,Q,皮尔斯律,证明：,因为,(Q,R),Q),Q,的合取范式,Q,(,R,Q),Q,，所以子句集合,=Q,R,Q,Q,Q,1,=Q Q,1,Q,2,=,Q Q,2,Q,3,=,Q,3,=(Q,1,-Q),(Q,2,-,Q),定理：子句集合,是不可满足的当且仅当存在,的反驳。,证明：设为,Q,1,Q,n,是反驳。,(1).,若,Q,k,，,|=Q,k.,(2).,若,|=Q,i,，,|=Q,j,并且,Q,k,是,Q,i,Q,j,的归结子句，则,Q,i,Q,j,|=Q,k,。因此，,|=Q,k,。,(3).,因为,Q,n,=,，所以有,Q,n-1,和,Q,k,是相反文字，不妨设是,q,和,q,。,因此，,|=q,，,|=,q,。,|=q,q,，,不可满足。,又证：设子句集合,是不可满足的。,(1).,不妨设子句集合,不含永真式。因为从,中去掉永真式不改变,的不可满足性。,(2).,若,含有相反文字，不妨设是,q,，则,Q,1,=q Q,1,Q,2,=,q Q,2,Q,3,=,因此，,Q,1,Q,2,Q,3,是反驳,.,(3).,根据命题逻辑紧致性定理，若子句集合,不可满足，则有有穷子句集合,0,，,0,，使得,0,是不可满足的。,若有穷子句集合,0,是不可满足的，则,0,中的子句必出现相反文字。,假设有穷子句集合,0,是不可满足的，且,0,中的子句不出现相反文字，那么，对于,0,中子句的每个文字,q,k,，有赋值函数,使得,(q,k,)=1,，因此，,(,0,)=1,，,0,是可满足的，这样与,0,是不可满足的相矛盾。,设,0,有,n,种相反文字，有相反文字,q,和,q,，,0,中的子句分为三类，,一类是有文字,q,的子句，,另,一类是有文字,q,的子句，,再一类是没有文字,q,和,q,的子句,q,=q,P,k,|q,P,k,，,q,=,q,Q,k,|,q,Q,k,，,C,=-,q,-,q,|,q,|=m,1,，,|,q,|=m,2,，,|,C,|=m,3,。,R,=P,i,Q,j,|q,P,i,q,q,Q,j,q,1,=,C,R,1,有,n-1,个命题变元。,若有,r,1,并且,r,1,，则存在反驳。,若,q,q,C,不可满足，则,1,=,C,R,不可满足。,若,1,是可满足的，则有赋值函数,，使得,(,1,)=1,。,如果,(P,i,)=1,，,i,=1,.,m,1,，那么有,(q)=0,，而其他命题变元,r,有,(r)=(r),。,(q,P,i,)=1,，其中，,q,P,i,q,(,q,Q,j,)=1,，其中，,q,Q,j,q,(R,k,)=1,，其中，,R,k,C,因此，若,1,是可满足的，则有,，使得,(,0,)=1,，这样就产生了矛盾，所以，,1,是不可满足的。,如果,(P,i,)=0,，,i,m,1,，则有,P,i,Q,j,1,，,j=1,m,2,。,因为,(,1,)=1,，所以有,(P,i,Q,j,)=1,，即,(Q,j,)=1,，,j=1,m,2,。,设,(q)=1,，而其他命题变元,r,有,(r)=(r),。,(q,P,i,)=1,，其中，,q,P,i,q,(,q,Q,j,)=1,，其中，,q,Q,i,q,(R,k,)=1,，其中，,R,k,C,若,1,是可满足的，则有,，使得,(,0,)=1,，这样就产生了矛盾，所以，,1,是不可满足的。,因此，,1,有,n-1,个命题变元并且,1,是不可满足的。,对于所有的,n,进行处理获得,n,，必有反驳，否则必有,n,可满足，进而有,0,可满足。,证毕,例题：,P,(Q,R),(P,Q),(P,