第三章基于谓词逻辑的机器推理

第三章基于谓词逻辑的机器推理本章主要内容：3.1一阶谓词逻辑3.2归结演绎推理3.3应用归结原理求取问题答案3.4归结策略3.5归结反演程序举例第一节一阶谓词逻辑本节主要内容：谓词、函数、量词谓词公式谓词逻辑中的形式演绎推理谓词、函数、量词谓词：表达式P(x1,x2,…,xn)说明：（1）其中，P是谓词符号（简称谓词）约定用大写英文字母打头作为谓词符号(Prolog?)。（2）xi(i=1,2,…n)是参数项（简称项）（3）由于有n个参数项，P(x1,x2,…,xn)表示了一个n元谓词公式。举例：P（x），Q（x，y）谓词、函数、量词函数：表达式f(x1,x2,…,xn)说明：（1）其中，f是函数符号（简称函数）约定用小写英文字母打头作为函数符号。（2）xi(i=1,2,…n)是个体变元（3）由于有n个变元，f(x1,x2,…,xn)成为n元个体函数举例：father（li），sum（x，y）约定：如果为单个项，用小写字母x，y，z等作为变元的符号，小写字母a，b，c等作为个体常元符号谓词、函数、量词量词：全称量词--以符号（x）P(x)来表示对于某个论域中的所有个体x,都有P(x）真值为T。（一切，任一，全体，凡是等）存在量词--以符号（$x）P(x)来表示某个论域中至少存在一个个体x，使P(x)真值为T。（存在，有些，至少有一个，有的）这里，P(x)是任意逻辑语句，也称作量词的管辖范围（简称辖域）。谓词、函数、量词量词举例：(x)[Robot(x)=Color(x,Gray)],所有机器人都是灰色的；(x)[Road(x)Lead(x,Roma)],条条大路通罗马；（$x)[Isa(x,Robot)∧Inroom(x,R1)],至少有一个机器人在房间R1中；（x)($y)[Person(x)∧Book(y)∧Give(Mary,x,y)]，Mary给每个人一本书。（x)[Person(x)∧Give（Mary,x,y）],Mary给每人某个同样的东西。谓词公式谓词公式的一般形式是：P(x1,x2,…,xn)其中，P是谓词符号（简称谓词），xi(i=1,2,…n)是参数项（简称项）；由于有n个参数项，P(x1,x2,…,xn)表示了一个n元谓词公式。项可以是常量、变量或函数。例如，谓词公式Inroom(Robot,L1)包括2个常量项，Married(father(L1),x)包括函数项father(L1)和变量项x,father(L1)映射L1到他的父亲。为避免混淆和增加表示的清晰性，谓词和常量项通常以首字母大写的形式来表示，而函数和变量则以小写字母的形式表示。当一谓词公式中不含变量，或变量值均取定时，谓词公式所表示的事物间的关系也就唯一确定。若这种关系在应用域确实存在，则谓词公式取值为真（记为T），否则为假（记为F）。在这个意义上，每个谓词公式均有一个确定的真值：T或F。谓词公式是谓词演算的基本单元，也称为原子公式。通过引入连词和量词，可以把原子公式组合为复合谓词公式。1）连词谓词演算中使用的连词主要有:¬（非）、∧（与）、∨（或）、=（蕴涵，也表示为-）和（等价，也表示为↔）。看几个例子：¬Inroom(Robot,R2)Isa(Liming,Student)∧Lives(Liming,House-1)∧Color(House-1,White)Isa(Wang,Teacher)∨Isa(Wang,Officer)At(Liming,School)=At(Wang,School)At(Liming,School)At(Wang,School)谓词公式：连词和量词（见上）一阶谓词若限定不允许对谓词、连词、量词和函数名进行量化处理，且参数项不能是谓词公式，则这样的谓词演算是一阶的。例如:（P）P(A)、（P）（x）P(x)、Married(y(L1),Mary，y)（y是变量）都不是一阶谓词公式。本书中所用到的谓词演算均是一阶的。谓词公式谓词公式的永真性和可满足性1）谓词公式的永真性若某谓词公式P对于某论域D上的所有可能的解释都有真值T，则称P在D上是永真的；若P在每个可能的非空论域上均永真，则称P是永真的。2）谓词公式的可满足性对于谓词公式P，若在论域D上至少可以建立一个解释，使P有真值T，则称P在D上是可满足的；若至少有一个论域使P可满足，则称P是可满足的。3）谓词公式的永假性若某谓词公式P对于论域D上的所有可能的解释都有真值F，则称P在D上是永假的(即不可满足的)；若P在每个可能的非空论域上均永假，则称P是永假的。谓词公式谓词逻辑中的形式演绎推理（谓词公式的性质）尽管谓词公式具有强大的形式化表示功能，但由于包括了多种连词和量词以及它们的嵌套应用，会使表示形式过于复杂，不利于演绎推理系统的设计和高效运作。为此，化简谓词公式到某些约定的标准形式是很有意义的，谓词公式的性质则为化简工作提供了依据。下面给出关于谓词公式的常用性质：1）双重否定¬(¬P)P2）蕴涵式转化PQ¬P∨Q3）狄·摩根定律¬(P∨Q)¬P∧¬Q¬(P∧Q)¬P∨¬Q4)分配律P∧(Q∨R)(P∧Q)∨(P∧R）P∨(Q∧R)(P∨Q)∧(P∨R)5）交换律P∨QQ∨P,P∧QQ∧P6）结合律(P∧Q)∧RP∧(Q∧R）(P∨Q)∨RP∨（Q∨R）7）逆否律PQQP8）量词否定¬($x)P(x)(x)(¬P(x))¬(x)P(x)（$x)(¬P(x))9)量词分配(x)[P(x)∧Q(x)](x)P(x)∧(x)Q(x)($x)[P(x)∨Q(x)]（$x）P(x)∨($x)Q(x)10)约束变量的虚元性（约束变量名的变换不影响合适公式的真值）(x)P(x)(y)P(y)($x)P(x)($y)P(y)第二节归结演绎推理本节主要内容：子句集命题逻辑中的归结原理替换与合一谓词逻辑中的归结原理子句集定义：原子谓词公式及其否定称为文字，若干个文字的一个析取式称为一个子句，若干个子句的集合成为子句集。一个文字子句叫单元子句不含任何文字的子句叫空子句，记做口或NIL子句集（求子句集的步骤）消去蕴涵量词缩小否定量词的作用范围，直至仅作用于原子公式适当改名，使量词间不在含有同名变元消去存在量词消去全称量词化公式为合取范式适当改名，使子句间无同名变元消去合取量词，以子句为元素组成一个子句集谓词公式的标准化1.标准化需求谓词公式的标准化是为基于谓词演算的演绎推理服务的，常见的基于谓词演算的推理有归结反演和规则演绎。这二种演绎推理都要求以所谓的量词前束范式来表示谓词公式，形如：（Q1x1）（Q2x2）…（Qkxk）M其中M称为母式，不包括任何量词，量词全都集中置于M的前面，Qi可以是量词符号或$，xi是量词的约束变量（i=1,2,…,k）。谓词公式的标准化归结反演要求母式M标准化为合取范式，定义如下：M=W1∧W2∧…∧WnWi=Li1∨Li2∨…∨Lim(i=1,2,…,n)Lij=Pij|¬Pij(j=1,2,…,m)Lij称为文字（Literal）,只能是原子谓词公式Pij或其取反。与合取范式对偶的是析取范式，定义如下：M=W1∨W2∨…∨WnWi=Li1∧Li2∧…∧Lim(i=1,2,…,n)Lij=Pij|¬Pij(j=1,2,…,m)2.合取范式的标准化过程将谓词公式化简为标准的合取范式,实际上就是应用谓词公式性质将公式逐步转化的过程。尽管对转化过程步骤的顺序并无严格的规定，但遵从一个合理顺序可以降低化简的困难和减少差错。下面是我们提倡的一个较合理的化简过程（请参见后面实例）：（0）消去多余的量词若一个量词的辖域内并未出现量词的约束变量，则该量词是多余的，应将其消去。例如($x)P(y),则($x)可以消去。正常情况下，合适公式中不应出现多余的量词，后面的实例中就未出现多余的量词。(1)消去蕴涵符号应用蕴涵式转化性质，例如后面实例中就有：Q(x,y)P(y)¬Q(x,y)∨P(y)(2)内移否定符号使其只出现在原子谓词公式前面，以构成否定文字。¬（$y）[¬P(y)∨P(f(x,y))]（y）[P(y∧¬P(f(x,y)))](3)变量换名使所有量词都具有不同的约束变量名，这可以依据约束变量的虚元性来进行变换。鉴于约束变量的作用域仅限于量词辖域，但量词前束后又会使同名变量的辖域无法区分，所以为避免差错，换名是必要的。例如，(y)($w)[¬Q(x,y)∨P(y,w)](z)($w)[¬Q(x,z)∨P(z,w)](4)消去存在量词，分二种情况：存在量词出现在全称量词的辖域内和不在辖域内.（z)($w)[┐Q(x,z)∨P(z,w)],（$w）在（z）辖域内，（$x){P(x)∧{…}},（$x）不出现在全称量词辖域内。※对于前一情况，意味着w的存在依赖于z，这种依赖关系可以由某个假设的函数w=g(z)来定义，我们称这种函数为Skölem函数，只要用Skölem函数g(z)取代约束变量w,就可消去存在量词（$w）:（z）[┐Q(x,z)∨P(z,g(z))]有时一存在量词可以出现在多个全称量词的辖域内，例如:(x)（y)(z)（$w）P(x,y,z,w)。则可设想一个多元Skölem函数g(x,y,z)取代约束变量w并消去存在量词（$w）:（x）（y）（z）P(x,y,z,g(x,y,z))。※对于后一情况，我们可以任意设想一个常量，例如A(称为Skölem常量)，用于取代约束变量x，而取消存在量词（$x）：P(A)∧{…}(5)全称量词前束化鉴于经过第（3）步的变量换名后，所有量词的约束变量均有不同的名字，所以只要简单地将这些量词移动到合适公式的最前面集中存放即可，并不会导致约束变量作用范围的变化。（6）消去全称量词我们假设所有变量均受全称量词的约束，则可以简单地删去全称量词，只留下母式。(7)把母式转化为合取范式应用合适公式的分配律可以将母式转化为合取范式，例如：[P(y)∧┓P(f(A,y))]∨[┓Q(A,z)∨P(z,g(z))][P(y)∨┓Q(A,z)∨P(z,g(z))]∧[┓P(f(A,y))∨┓Q(A,z)∨P(z,g(z))]作为实例，现在让我们来观察一个合适公式的化简：（x）{P(x){($y)[P(y)P(f(x,y))]∧（y）($w)[Q(x,y)P(y,w)]}}（x）{P(x){($y)[P(y)P(f(x,y))]∧（y）($w)[Q(x,y)P(y,w)]}}(1)（x）{P(x)∨{($y)[P(y)∨P(f(x,y))]∧（y）($w)[Q(x,y)∨P(y,w)]}（x）{P(x){($y)[P(y)P(f(x,y))]∧（y）($w)[Q(x,y)P(y,w)]}}(1)（x）{P(x)∨{($y)[P(y)∨P(f(x,y))]∧（y）($w)[Q(x,y)∨P(y,w)]}(2)($x){P(x)∧{（y）[P(y)∧P(f(x,y))]∨（y）($w)[Q(x,y)∨P(y,w)]}}（x）{P(x){($y)[P(y)P(f(x,y))]∧（y）($w)[Q(x,y)P(y,w)]}}(1)（x）{P(x)∨{($y)[P(y)∨P(f(x,y))]∧（y）($w)[Q(x,y)∨P(y,w)]}(2)($x){P(x)∧{（y）[P(y)∧P(f(x,y))]∨（y）($w)[Q(x,y)∨P(y,w)]}}(3)($x){P(x)∧{（y）[P(y)∧P(f(x,y))]∨（z）($w)[Q(x,z)∨P(z,w)]}}（x）{P(x){($y)[P(y)P(f(x,y))]∧（y）($w)[Q(x,y)P(y,w)]}}(1)（x）{P(x)∨{($y)[P(y)∨P(f(x,y))]∧（y）($w)[Q(x,y)