第5章-基于谓词逻辑的机器推理.

第5章基于谓词逻辑的机器推理第5章基于谓词逻辑的机器推理5.1一阶谓词逻辑5.2归结演绎推理5.3应用归结原理求取问题答案5.4归结策略5.5归结反演程序举例5.6Horn子句归结与逻辑程序5.7非归结演绎推理第5章基于谓词逻辑的机器推理5.1一阶谓词逻辑5.1.1谓词、函数、设a1,a2,…,an表示个体对象,A表示它们的属性、状态或关系,则表达式A(a1,a2,…,an)在谓词逻辑中就表示一个(原子)命题。例如,(1)素数(2),就表示命题“2是个素数”。(2)好朋友(张三,李四),就表示命题“张三和李四是好朋友”。第5章基于谓词逻辑的机器推理P(x1,x2,…,xn)一般地,表达式在谓词逻辑中称为n元谓词。其中P是谓词符号，也称谓词，代表一个确定的特征或关系(名)。x1,x2,…,xn称为谓词的参量或者项，一般表示个体。个体变元的变化范围称为个体域（或论述域），包揽一切事物的集合称为全总个体域。第5章基于谓词逻辑的机器推理为了表达个体之间的对应关系，我们引入通常数学中函数的概念和记法。例如我们用father(x)表示x的父亲，用sum(x,y)表示数x和y之和，一般地，我们用如下形式：f(x1,x2,…,xn)表示个体变元x1,x2,…,xn所对应的个体y，并称之为n元个体函数，简称函数（或函词、函词命名式）。其中f是函数符号，有了函数的概念和记法，谓词的表达能力就更强了。例如，我们用Doctor(father(Li))表示“小李的父亲是医生”，用E(sq(x),y))表示“x的平方等于y”。第5章基于谓词逻辑的机器推理以后我们约定用大写英文字母作为谓词符号,用小写字母f,g,h等表示函数符号,用小写字母x,y,z等作为个体变元符号,用小写字母a,b,c等作为个体常元符号。我们把“所有”、“一切”、“任一”、“全体”、“凡是”等词统称为全称量词,记为x;把“存在”、“有些”、“至少有一个”、“有的”等词统称为存在量词,记为x。))()((xNxMx其中M(x)表示“x是人”,N(x)表示“x有名字”,该式可读作“对于任意的x,如果x是人,则x有名字”。这里的个体域取为全总个体域。如果把个体域取为人类集合,则该命题就可以表示为)(xxN第5章基于谓词逻辑的机器推理同理,我们可以把命题“存在不是偶数的整数”表示为))()((xExGx其中G(x)表示“x是整数”,E(x)表示“x是偶数”。此式可读作“存在x,x是整数并且x不是偶数”。第5章基于谓词逻辑的机器推理不同的个体变元,可能有不同的个体域。为了方便和统一起见,我们用谓词表示命题时,一般总取全总个体域,然后再采取使用限定谓词的办法来指出每个个体变元的个体域。具体来讲,有下面两条：(1)对全称量词,把限定谓词作为蕴含式之前件加入,即(2)对存在量词,把限定量词作为一个合取项加入,即这里的P(x)就是限定谓词。我们再举几个例子。......))((xPx......)P(x)(x第5章基于谓词逻辑的机器推理例5.1不存在最大的整数,我们可以把它翻译为)),()(()((yxDyGyxGx或)),()(()((xyDyGyxGx例5.2对于所有的自然数,均有x+yx)),,()()((xyxSyNxNyx例5.3某些人对某些食物过敏)),()()((yxGyFxMyx第5章基于谓词逻辑的机器推理5.1.2谓词公式定义1(1)个体常元和个体变元都是项。(2)设f是n元函数符号,若t1,t2,…,tn是项,则f(t1,t2,…,tn)是项。(3)只有有限次使用(1),(2)得到的符号串才是项。第5章基于谓词逻辑的机器推理定义2设P为n元谓词符号，t1,t2,…,tn为项，则P(t1,t2,…,tn)称为原子谓词公式，简称原子公式或者原子。从原子谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。下面我们给出谓词公式的严格定义，即谓词公式的生成规则。第5章基于谓词逻辑的机器推理定义3(1)原子公式是谓词公式。(2)若A,B是谓词公式，则A,A∧B,A∨B,A→B,AB,xA,xA也是谓词公式。(3)只有有限步应用(1)，(2)生成的公式才是谓词公式。由项的定义，当t1,t2,…,tn全为个体常元时，所得的原子谓词公式就是原子命题公式（命题符号）。所以，全体命题公式也都是谓词公式。谓词公式亦称为谓词逻辑中的合适（式）公式，记为Wff。第5章基于谓词逻辑的机器推理紧接于量词之后被量词作用(即说明)的谓词公式称为该量词的辖域。例如：(1)xP(x)。(2)x(H(x)→G(x,y))。(3)xA(x)∧B(x)。其中(1)中的P(x)x的辖域,(2)中的H(x)→G(x,y)x的辖域,(3)中的A(x)x的辖域,但B(x)x的辖域。第5章基于谓词逻辑的机器推理量词后的变元如x,y中的x,y称为量词的指导变元(或作用变元),而在一个量词的辖域中与该量词的指导变元相同的变元称为约束变元,其他变元(如果有的话)称为自由变元,例如(2)中的x为约束变元,而y为自由变元,(3)中A(x)中的x为约束变元,B(x)中的x为自由变元。例如(3),一个变元在一个公式中既可约束出现,又可自由出现,但为了避免混淆,通常通过改名规则,使得一个公式中一个变元仅以一种形式出现。第5章基于谓词逻辑的机器推理约束变元的改名规则如下：(1)对需改名的变元,应同时更改该变元在量词及其辖域中的所有出现。(2)新变元符号必须是量词辖域内原先没有的,最好是公式中也未出现过的。例如公式xP(x)∧Q(x)yP(y)∧Q(x),但两者的意义相同。在谓词前加上量词,称作谓词中相应的个体变元被量化,例xA(x)中的x被量化,yB(y)中y被量化。如果一个谓词中的所有个体变元都被量化,则这个谓词就变为一个命题。例如,设P(x)表示“x是素数”,则xP(x),xP(x)就都是命题。这样我们就有两种从谓词(即命题函数)得到命题的方法：一种是给谓词中的个体变元代入个体常元,另一种就是把谓词中的个体变元全部量化。第5章基于谓词逻辑的机器推理把上面关于量化的概念也可以推广到谓词公式。于是，我们便可以说，如果一个公式中的所有个体变元都被量化，或者所有变元都是约束变元（或无自由变元），则这个公式就是一个命题。特别地，我们称xA(x)为全称命题，xA(x)为特称命题。对于这两种命题，当个体域为有限集时（设有n个元素），有下面的等价式：xA(x)A(a1)∧A(a2)∧…∧A(an)xA(x)A(a1)∨A(a2)∨…∨A(an)这两个式子也可以推广到个体域为可数无限集。第5章基于谓词逻辑的机器推理定义4设A为如下形式的谓词公式：B1∧B2∧…∧Bn其中Bi(i=1,2,…,n)形如L1∨L2∨…∨Lm，Lj(j=1,2,…,m)为原子公式或其否定，则A称为合取范式。例如：(P(x)∨Q(y))∧(乛P(x)∨Q(y)∨R(x,y))∧(乛Q(y)∨乛R(x,y))就是一个合取范式。第5章基于谓词逻辑的机器推理定义5设A为如下形式的命题公式：B1∨B2∨…∨Bn其中Bi(i=1,2,…,n)形如L1∧L2∧…∧Lm，Lj(j=1,2,…,m)为原子公式或其否定，则A称为析取范式。例如：(P(x)∧乛Q(y)∧R(x,y))∨(乛P(x)∧Q(y))∨(乛P(x)∧R(x,y))就是一个析取范式。第5章基于谓词逻辑的机器推理定义6设P为谓词公式，D为其个体域，对于D中的任一解释I：(1)若P恒为真，则称P在D上永真（或有效）或是D上的永真式。(2)若P恒为假，则称P在D上永假（或不可满足）或是D上的永假式。(3)若至少有一个解释,可使P为真，则称P在D上可满足或是D上的可满足式。第5章基于谓词逻辑的机器推理定义7设P为谓词公式，对于任何个体域：(1)若P都永真，则称P为永真式。(2)若P都永假，则称P为永假式。(3)若P都可满足，则称P为可满足式。第5章基于谓词逻辑的机器推理5.1.3谓词逻辑中的形式演绎推理由上节所述，我们看到，利用谓词公式可以将自然语言中的陈述语句表示为一种形式化的符号表达式。那么，利用谓词公式，我们同样可以将形式逻辑中抽象出来的推理规则形式化为一些符号变换公式。表3.1和表3.2就是形式逻辑中常用的一些逻辑等价式和逻辑蕴含式，即推理规则的符号表示形式。第5章基于谓词逻辑的机器推理表5.1常用逻辑等价式第5章基于谓词逻辑的机器推理第5章基于谓词逻辑的机器推理第5章基于谓词逻辑的机器推理第5章基于谓词逻辑的机器推理表5.2常用逻辑蕴含式第5章基于谓词逻辑的机器推理第5章基于谓词逻辑的机器推理例5.4设有前提：(1)凡是大学生都学过计算机；(2)小王是大学生。试问：小王学过计算机吗？解令S(x)：x是大学生;M(x)：x学过计算机;a：小王。则上面的两个命题可用谓词公式表示为(1)x(S(x)→M(x))(2)S(a)第5章基于谓词逻辑的机器推理下面我们进行形式推理：(2)x(S(x)→M(x))［前提］(2)S(a)→M(a)［(1),US］(3)S(a)［前提］(4)M(a)［(2),(3),I3］得结果：M(a)，即“小王学过计算机”。第5章基于谓词逻辑的机器推理例5.5证明乛P(a,b)是xy(P(x,y)→W(x,y))和乛W(a,b)的逻辑结果。证(1)xy(P(x,y)→W(x,y))［前提］(2)y(P(a,y)→W(a,y))［(1),US］(3)P(a,b)→W(a,b)［(2),US］(4)乛W(a,b)［前提］(5)乛P(a,b)［(3),(4),I4］第5章基于谓词逻辑的机器推理例5.6证x(P(x)→Q(x))∧x(R(x)乛Q(x))x(R(x)→乛P(x))。证(1)x(P(x)→Q(x))［前提］(2)P(y)→Q(y)［(1),US］(3)乛Q(y)→乛P(y)［(2),E24］(4)x(R(x)→Q(x))［前提］(5)R(y)→乛Q(y)［(3),US］(6)R(y)→乛P(y)［(3),(5),I6］(7)x(R(x)→乛P(x))［(6),UG］第5章基于谓词逻辑的机器推理5.2.1子句集定义1原子谓词公式及其否定称为文字，若干个文字的一个析取式称为一个子句，由r个文字组成的子句叫r—文字子句，1—文字子句叫单元子句，不含任何文字的子句称为空子句，记为或NIL。例如下面的析取式都是子句P∨Q∨乛RP(x,y)∨乛Q(x)5.2归结演绎推理第5章基于谓词逻辑的机器推理定义2对一个谓词公式G，通过以下步骤所得的子句集合S，称为G的子句集。(1)消去蕴含词→和等值词←→。可使用逻辑等价式:①A→BA∨B②A←→B(乛A∨B)∧(乛B∨A)第5章基于谓词逻辑的机器推理(2)缩小否定词的作用范围，直到其仅作用于原子公式。可使用逻辑等价式:①乛(乛A)A②乛(A∧B)乛A∨乛B③乛(A∨B)乛A∧乛B④乛xP(x)x乛P(x)⑤乛xP(x)x乛P(x)第5章基于谓词逻辑的机器推理(3)适当改名，使量词间不含同名指导变元和约束变元。(4)消去存在量词。消去存在量词时，同时还要进行变元替换。变元替换分两种情况：①若该存在量词在某些全称量词的辖域内，则用这些全称量词指导变元的一个函数代替该存在量词辖域中的相应约束变元，这样的函数称为Skolem函数；②若该存在量词不在任何全称量词的辖域内，则用一个常量符号代替该存在量词辖域中的相应约束变元，这样的常量符号称为Skolem常量。第5章基于谓词逻辑的机器推理(5)消去所有全称量词。(6)化公式为合取范式。可使用逻辑等价式:①A∨(B∧C)(A∨B)∧(A∨C)②(A∧B)∨C(A∨C)∧(B∨C)(7)适当改名，使子句间无同名变元。(8)消去合取词∧，以子句为元素组成一个集合S。第5章基于谓词逻辑的机器推理例5.7求下面谓词公式的子句集x{yP(x,y)→y［Q(x,y)→R(x,y)］}解由步(