1人工智能2.3谓词逻辑2.4归结推理22.3谓词逻辑2.3.1语法一阶谓词演算标点符号、括号、逻辑联结词、常量符号集、变量符号集、n元函数符号集、n元谓词符号集、量词谓词演算合法表达式(原子公式、合式公式wff),表达式的演算化简方法,标准式(合取的前束范式或析取的前束范式)3语法元素:·常量符号。·变量符号。·函数符号。·谓词符号。·联结词:┐、∧、∨、→、。·量词:全称量词、存在量词。和后面跟着的x叫做量词的指导变元。4定义2.13项可递归定义如下:(1)单独一个个体是项(包括常量和变量)。(2)若f是n元函数符号,而是项,则f()是项。(3)任何项仅由规则(1)(2)所生成。定义2.14若P为n元谓词符号,t1,…,tn都是项,则称P(t1,…,tn)为原子公式。5定义15一阶谓词逻辑的合式公式:(1)原子谓词公式是合式公式(也称为原子公式)。(2)若P、Q是合式公式,则(┐P)、(P∧Q)、(P∨Q)、(P→Q)、(P←→Q)也是合式公式。(3)若P是合式公式,x是任一个体变元,则(x)P、(x)P也是合式公式。(4)没了。62.3.2语义语义是赋予它的一个数学结构,包括:(1)非空集合U——个体域(2)映射I——解释,它指称(FC)中的常元、函词、谓词:对任一常元a,I(a)∈U,I(a)常简记为,为个体域中一个元素。对每一函词f(n),I(f(n))为U上的一个n元函数。对每一n元谓词P(n),I(P(n))为U上的一个n元关系。当n=1时,为U的一个子集。当使用零元谓词作为命题常元时,I(P(0))∈{T,F},即I对命题常元指定真值。7定义16公式A在结构U、指派s下真,即定义|=A[s]如下:(l)A为原子公式P(n)t1…tn时…….(2)A为公式┐B时……………….(3)A为公式B→C时…………..(4)A为公式vB时………….8定义18设P与Q是D上的两个谓词公式,若对D上的任意指派,P与Q都有相同的真值,则称P和Q在D上是等价的。如果D是任意非空个体域,则称P与Q是等价的,记作PQ。常用的等价式(书pp40-41)定义17对于谓词公式A,如果至少存在结构U和指派s,使公式A在此结构和指派下的真值为T,则称公式A是可满足的。9定义19对谓词公式P和Q,如果P→Q永真,则称P永真蕴涵Q,且称Q为P的逻辑推论,P为Q的前提,记作PQ。常用的永真蕴涵式(书p41)102.3.3谓词逻辑形式系统FC谓词逻辑的公理组由下列公理模式及其所有全称化所组成。AX(l.1).A→(B→A)AX(l.2).(A→(B→C))→((A→B)→(A→C))AX(l.3).(┐A→┐B)→(B→A)AX2.vA→Atv(t对A中变元v可代入)AX3.v(A→B)→(vA→vB)AX4.A→vA(v在A中无自由出现)推理规则模式仍为rmp11定理10如果├A,那么├vA定理11Γ;A├B当且仅当Γ├A→B定理12├A蕴涵着|=A。定理13|=A蕴涵着├A。12定义20一类问题称为是可判定的,如果存在一个算法或过程,该算法用于求解该类问题时,可在有限步内停止,并给出正确的解答。如果不存在这样的算法或过程则称这类问题是不可判定的。定理14任何至少含有一个二元谓词的一阶谓词演算系统都是不可判定的。定理15一阶谓词演算是半可判定的。13给出定理的推理过程及所使用的推理规则序列就构成了该定理的一个证明。在证明定理的演绎过程中,经常要对量化的表达式进行匹配操作,因而需要对项作变量置换使表达式一致起来,这个过程称作合一。14前束范式化简步骤(1)消去多余的前束(量词)。(2)消去蕴涵符号(→联结词)。(3)内移否定词┓的辖域范围。(4)变量标准化。对变量作必要的换名,使每一量词只约束一个唯一的变量名。(5)把所有量词都集中到公式左面,移动时不要改变其相对顺序。15(6)消去存在量词。对于待消去的存在量词,若不在任何全称量词辖域之内(即它的左边没有全称量词),则用Skolem常量替代公式中存在量词约束的变量,若受全称量词约束(即左边有全称量词),则要用Skolem函数(即与全称量词约束变量有关的函数)替代存在量词约束的变量,然后就可消去存在量词。16例F=(x)(y)(z)(u)(v)(w)(P(x,y,z,u,v,w)∧(Q(x,y,z,u,v,w)∨┓R(x,z,w)))其中母式各变量中,四个存在量词所约束的变量应分别用如下所示的Skolem函数和常量替代:x=a,y=b,u=f(z),w=g(z,v)消去存在量词后得Fl=(z)(v)(P(a,b,z,f(z),v,g(z,v))∧(Q(a,b,z,f(z),v,g(z,v))∨┐R(a,z,g(z,v)))17(7)把母式化成合取范式。反复使用结合律和分配律,将母式表达成合取范式的标准型,最后得到一个Skolem化的前束范式Fs。(8)隐略去前束式。由于母式的变量均受量词的约束,可省略掉全称量词,但剩下的母式仍假设其变量受全称量词量化。18(9)把母式用子句集表示。把母式中每一个合取元称为一个子句,省去合取联结词,这样就可把母式写成集合的形式表示,每一个元素就是一个子句。如上例的子句集是S={P(a,b,z,f(z),v,g(z,v)),Q(a,b,z,f(z),v,g(z,v))∨┐R(a,z,g(z,v))}19(10)子句变量标准化。对某些变量重新命名,使任意两个子句不会有相同的变量出现。由于每一个子句都对应一个不同的合取元,变量都由全称量词量化,因而实质上两个子句的变量之间不存在任何关系,变量标准化不影响公式的真值。在使用子句集进行证明推理过程,有时要例化某一个全称量词量化的变量,这时就可能使公式尽量保持其一般化形式,增加了应用过程的灵活性。20标准式的应用问题得到的标准式是经过Skolem化的前束范式(S-标准形)。S-标准形不是唯一的,若把它记为Fs,则Fs仅仅是F的一个特例,取用不同的Skolem函数会得到不同的结果。当F为非永假公式时,Fs与F并不等价,但当F为永假时,Fs也一定是永假的,即Skolem化并不影响F的永假特性。21定理:若S是合式公式F的S-标准形之子句集,则F为永假的充要条件是S为不可满足的。Story高耀清22子句,它是S-标准形母式中的合取元,因而每一个子句是若干文字(原子公式和原子公式否定式)的析取式。不含有文字的子句——空子句,空子句的取值总为假,简记为□或NIL。23一个子句的文字中,其变量被常量替代,就得到一个文字的基例,由基文字组成的子句称基子句。子句集中所有元素(即子句)的合取式不为真,则称该子句集为不可满足的。242.3.4一阶谓词逻辑的应用例2.4“某些患者喜欢所有医生。没有患者喜欢庸医。所以没有医生是庸医。”解:P(x)表示“x是患者”,D(x)表示“x是医生”,Q(x)表示“x是庸医”,L(x,y)表示“x喜欢y”。目的是证明G是F1和F2的逻辑结论。25例2.5每个去临潼游览的人或者参观秦始皇兵马俑,或者参观华清池,或者洗温泉澡。凡去临潼游览的人,如果爬骊山就不能参观秦始皇兵马俑,有的游览者既不参观华清池,也不洗温泉澡。因而有的游览者不爬骊山。解:定义G(x)表示“x去临潼游览”;A(x)表示“x参观秦始皇兵马俑”;B(x)表示“x参观华清池”;C(x)表示“x洗温泉澡”;D(x)表示“x爬骊山”。26前提:∀x(G(x)→A(x)∨B(x)∨C(x))(1)∀x(G(x)∧D(x)→¬A(x))(2)x(G(x)∧¬B(x)∧¬C(x))(3)结论:x(G(x)∧¬D(x))证明:(4)G(a)∧¬B(a)∧¬C(a)由(3)(5)G(a)→A(a)∨B(a)∨C(a)由(1)(6)G(a)∧D(a)→¬A(a)由(2)(7)A(a)→¬G(a)∨¬D(a)由(6)(8)G(a)由(4)(9)A(a)∨B(a)∨C(a)由(5)(8)(10)¬B(a),¬C(a)由(4)(11)A(a)由(9)(10)(12)¬D(a)由(7)(8)(11)(13)x(G(x)∧¬D(x))由(8)(12)272.4归结推理归结方法,1965年Robinson提出归结方法的基本思想命题逻辑归结原理谓词逻辑归结原理28什么是归结原理在定理证明系统中,已知一公式集F1,F2,…,Fn,要证明一个公式W(定理)是否成立,即要证明W是公式集的逻辑推论时,一种证明法就是要证明F1∧F2∧…∧Fn→W为永真式。反证法:证明F=F1∧F2∧…∧Fn∧┐W为永假,这等价于证明F对应的子句集S=S0∪{┐W}为不可满足的。29思路:设法检验扩充的子句集Si是否含有空子句,若S集中存在空子句,则S不可满足。若没有空子句,则就进一步用归结法从S导出S1。然后再检验S1是否有空子句。用归结法导出的扩大子句集S1,其不可满足性是不变的,所以若S1中有空子句,也就证得了S的不可满足性。通过归结过程演绎出S的不可满足性来,从而使定理得到证明。302.4.1命题逻辑的归结原理(1)归结式的定义及性质对子句C1和C2,若C1中有一个文字L1,而C2中有一个与L1成互补的文字L2,则分别从C1,C2中删去L1和L2,并将其剩余部分组成新的析取式,则称该子句为归结式。例:设两个子句C1=L∨C1',C2=(┐L)∨C2',则归结式C=Cl’∨C2’。当C1'=C2’=□时,C=□。31证:设C1=L∨C1',C2=(┐L)∨C2'关于解释I为真,则需证明C=Cl’∨C2’关于解释I也为真。关于解释I,L和┐L二者中必有一个为假。若L为假,则C1’必为真,否则C1为假,这与前提假设矛盾,所以只能是C1’为真。同理,若┐L为假,则C2’必为真。最后有C=C1’∨C2’关于解释I为真,即C是C1和C2的逻辑推论。定理:二个子句C1和C2的归结式C是C1和C2的逻辑推论。32推论:子句集S={C1,C2,…,Cn}与子句集S1={C,C1,C2,…,Cn}的不可满足性是等价的(其中C是C1和C2的归结式)。证:设S是不可满足的,则C1,C2,…,Cn中必有一为假,因而S1必为不可满足的。设S1是不可满足的,则对于不满足S1的任一解释I,可能有两种情况:(1)I使C为真,则C1,C2,…,Cn中必有一子句为假,因而S是不可满足的。(2)I使C为假,则根据定理有C1∧C2为假,即I或使C1为假,或使C2为假,因而S也是不可满足的。由此可见S和S1的不可满足性是等价的。33同理可证Si和Si+1(由Si导出的扩大的子句集)的不可满足性也是等价的,其中i=1,2,…。归结原理就是从子句集S出发,应用归结推理规则导出子句集S1。再从S1出发导出S2,依此类推,直到某一个子句集Sn出现空子句为止。根据不可满足性等价原理,已知若Sn为不可满足的,则可逆向依次推得S必为不可满足的。用归结法,过程比较单钝,只涉及归结推理规则的应用问题,因而便于实现机器证明。34(2)命题逻辑的归结过程命题逻辑中,若给定前提集F和命题P,则归结证明过程可归纳如下:(1)把F转化成子句集表示,得子句集S0;(2)把命题P的否定式┐P也转化成子句集表示,并将其加到S0中,得S=S0∪S┐P,(3)对子句集S反复应用归结推理规则,直至导出含有空子句的扩大子句集为止。即出现归结式为空子句的情况时,表明已找到了矛盾,证明过程结束。35证明:化成子句集S={P,┐P∨┐Q∨R,┐S∨Q,┐T∨Q,T,┐R}归结可用图的演绎树表示,由于根部出现空子句,因此命题R得证。例:设已知前提集为P………………(1)(P∧Q)→R………(2)(S∨T)→Q………(3)T…………………………(4)求证R。362.4.2谓词逻辑的归结原理在谓词逻辑中,要考虑变量的约束问题,在应用归结法时,要对