工智能及专家系统敖志刚第4章逻辑的知识表示和推理

工智能及专家系统敖志刚第4章逻辑的知识表示和推理敖志刚

编制第4章逻辑的知识表示和推理

4．1命题与逻辑4．1．1命题与命题定律4．1．2谓词逻辑4．2谓词逻辑知识表示4．2．1谓词逻辑知识表示方法4．2．2谓词逻辑表示的优缺点4．3逻辑推理的技术与算法4．3．1子句集及其化简4．3．2置换与合一4．3．3鲁滨逊消解(归结)原理第4章逻辑的知识表示和推理

4．1命题与逻辑

4.1.1

命题与命题定律命题、真命题、假命题、原子命题、不是命题。命题的表示——大写A、B、C┈┈P、Q、R。2.联结词（Connectives）

①

否定或补的联结词用“～”表示②

合取用“∧”表示，③

析取用“∨”表示，④

单条件联结词用“→”⑤

双条件联结词“”联结词运算的先后次序为～、∧、∨、→、，同级联结词先出现先运算3.定义真值指派：设一个由n个变元P1，P2，…，Pn组成的命题表达式A，则A的取值由这n个变元唯一确定。把变元的一组取值(T或F)叫做该表达式的一个真值指派。

真值表：真值表是由命题表达式所有的真值指派和对应的表达式真值所组成的一张表。永真式永假式等价式：设P与Q是D上的两个谓词公式，若对D上的任意解释，P与Q都有相同的真值，则称P与Q在D上是等价的。如果D是任意非空个体域，则称P与Q是等价的，记作P⇔Q。

永真蕴含式：对谓词公式P和Q，如果P→Q永真，则称P永真蕴含Q，且称Q为P的逻辑结论，P为Q的前提，记作P⇒Q。4.真值表

PQ～PP∧QP∨QP→QPQFFTFFTTFTTFTTFTFFFTFFTTFTTTT5.常用的等价命题定律⑴双重否定律～～PP⑵交换律

①P∧QQ∧P

②P∨QQ∨P⑶结合律①（P∧Q）∧RP∧（Q∧R）②（P∨Q）∨RP∨（Q∨R）

5.常用的等价命题定律⑷分配律①P∧（Q∨R）（P∧Q）∨（P∧R）②P∨（Q∧R）（P∨Q）∧（P∨R）③P→（Q→R）（P→Q）→（P→R）⑸狄·摩根定律①～（P∧Q）～P∨～Q②

～（P∨Q）～P∧～Q⑹吸收律①P∧（P∨Q）P②P∨（P∧Q）P⑺联结词化规律①P→Q～P∨Q②PQ（P→Q）∧（Q→P）③PQ（P∧Q）∨（～P∧～Q）⑻变换等价式P（P∧Q）∨（P∧～Q）

5.常用的等价命题定律6.永真蕴含式常用的永真蕴含式如下：

(1)化简式P∧Q⇒P，P∧Q⇒Q(2)附加式P⇒P∨Q，Q⇒P∨Q(3)析取三段论~P,P∨Q⇒Q(4)假言推理P,P→Q⇒Q(5)拒取式~Q,P→Q⇒P(6)假言三段论P→Q,Q→R⇒P→R(7)二难推理P∨Q,P→R,Q→R⇒R(8)全称固化(∀x)P(x)⇒P(y)其中，y是个体域中任一个体，依此可消去谓词公式中的全称量词

(9)存在固化(∃x)P(x)⇒P(y)其中，y是个体域中某一个可以使P(y)为真的个体，依此可消去谓词公式中的存在量词。7.利用命题定律证明等价式逻辑推理的步骤：⑴利用联结词化规律化掉→、；⑵利用狄·摩根定律将～深入到变元；⑶利用分配律进行变换。

8.示例例4-1试证明：（P∧（P→Q））∨Q（P∧Q）∨（～P∧Q）例4-2证明等价式：（P→Q）∧（R→Q）（P∨R）→Q1．2谓词逻辑

1.谓词和个体个体是指可以独立存在的事物，如花（桃花，玫瑰，犁花）、计算机、智能等等。谓词是用来刻划个体的性质或关系的。例如张三和李四是工人。通常用大写英文字母表示谓词，用小写英文字母表示个体。如果x的集合为a1，a2，…，an，则STUDENT（an）为真（T）。与一个个体相联的谓词叫一元谓词，与多个个体相联的谓词叫多元谓词。一个n元的谓词常可表示为P（x1，x2，…，xn），一般来说，在多元谓词中，个体间的次序不可随意交换。

2.

量词

首先来考察两个谓词P（x）：x2-1＝（x+1）（x–1）Q（x）：x+3＝１对于ｘ＝-２时为T。1．全称量词

通常把“所有”、“一切”、“任一”、“全体”、“凡是”等词统称为全称量词，记为；符号“”表示对于个体域中所有的个体x，p(x)谓词均为T。2．存在量词通常把“存在”、“有些”、“至少有一个”、“有的”等词统称为存在量词，记为；符号“”表示对于个体域中存在某些个体x，Q(x)谓词均为T。3.量词的集合表示设个体域x是有限集合S：

S={a1，a2，…，an}由量词的意义可知

A(a1)∧A(a2)∧…∧A(an)A(a1)∨A(a2)∨…∨A(an)4.量词之间的关系对于二元谓词P(x,y)，存在以下量化的可能：一般来讲，量词的先后次序不可交换。例如，x和y的个体域都是所有鞋子的集合，P(x,y)表示一只鞋子x可与另一只鞋子y配对，则表示“存在一只鞋子x，它可以与任何一只鞋子y配对”,这是不可能的，是个假命题。而表示“对任何一只鞋子y，总存在一些鞋子x可以与它配对”，这是真命题。3.含有量词的等价式⑴量词的转换律①②⑵量词的分配律①②③④3.含有量词的等价式⑶量词辖域扩张及收缩律①②③④3.含有量词的等价式⑷其他等价式①②③④⑤⑸量词消去规则①②4.定理证明～(A(a1)∧A(a2)∧…∧A(an))

～A(a1)∨～A(a2)∨～A(an)(A(a1)∧B(a1))∧(A(a2)∧B(a2))∧…∧(A(an)∧B(an))(A(a1)∧A(a2)∧…∧A(an))∧(B(a1)∧B(a2)∧…∧B(an))5.谓词表达式的范式⑴前束范式若有一谓词表达式W，它的所有量词均非否定地出现在表达式的前面，而它们的辖域为整个表达式，则称W为前束范式。前束范式的一般形式为：

例如就是一个前束范式。⑵Skolem范式在前束范式中，如果所有的存在量词都出现在全称量词之前，则称这种形式的范式表达式为Skolem范式。例如4．2谓词逻辑知识表示

4．2．1谓词逻辑知识表示方法

1.用谓词逻辑表示简单事实

RAINING；SUNNY；MAN（zhangsan）；INROOM（robot，room1）；MARRIED（father（lisi），mather（lisi））。2.联结词和量词的应用1、～INROOM（robot，room2）；2．LIKE（i，music）∧LIKE（i，painting）；

LIVE(lisi,house1)∧COLOR(house1,yellow)；3．PLAY(lihao,basketball)∨PLAY(lihao,football)；4．OWNS(heming,book-1)→COLOR(book-1,blue);5．GRASP(i，you)GRASP(you，i)；6．COLOR(x,gray)〕;7.()INROOM(x，room-1)

3.谓词逻辑的一般表示方法例4-4用谓词逻辑表示“所有的整数不是偶数就是奇数”。定义谓词:INTEGER(x):表示x是整数；EVEN(x):表示x是偶数；ODD(x):表示是奇数。该知识表示为:()(INTEGER(x)→EVEN(x)∨ODD(x))3.谓词逻辑的一般表示方法例4-5用谓词逻辑表示如下知识:“王宏是计算机系的一名学生”；“李明是王宏的同班同学”；“凡是计算机系的学生都喜欢编程序”。①首先定义谓词:COMPUTER(x):表示x是计算机系的学生；CLASSMATE(x，y):表示x是y的同班同学；LIKE(x，y):表示x喜欢y。②用谓词公式表示上述知识:COMPUTER(wanghong)；CLASSMATE(liming，wanghong)；()(COMPUTER(x)→LIKE(x，programing))。4.用谓词逻辑表示状态例4-6积木状态问题：假如给定积木世界的一个状态，桌子(Table)上放有三块积木A、B和C，且B在A上，C放在A、B的左边，如图4-1所示。用谓词逻辑给予描述这一积木世界问题的状态。①先定义几个谓词:ON(x，y)：x在y上；

ONTABLE（x)：x在桌子上；

CLEAR（x)：x顶上是空的;RIGHT(x，y)：x在y的右边。x，y的个体域都是A、B、CTableCAB图4-1积木世界的一个状态4.用谓词逻辑表示状态这个积木世界的状态可以表示成:ON(B，A)；RIGHT(B，C)；RIGHT(AC)；ONTABLE(A)；ONTABLE(C)；CLEAR(C)；CLEAR(B)。显然有以下关系：

()(CLEAR(x)～()ON(y，x))TableCAB图4-1积木世界的一个状态4.用谓词逻辑表示状态例4-6机器人移盒子问题：在一个包含有凹室(Alcove)的房间内有两张桌子A和B，一个机器人(Robot)和一个盒子(Box)，如图4-2所示。我们的任务是让机器人从凹室出发，把桌子A上的盒子移到桌子B上，然后回到凹室。试用谓词逻辑描述这一行动过程。图4-2机器人移盒子初始状态Robot首先定义以下几个谓词:①TABLE(x)：X是桌子；②EMPTYHANDED(y)：y手中是空的；③AT(y，z)：y在z的附近；④HOLDS(y，w)：y手中拿着w；⑤ON(w，x)：w在x桌面上。其中x，y，z，w个体域分别是{a，b}，{robot}，{a，b，alcove}，{box}。

图4-2机器人移盒子初始状态Robotabalcove

box4.用谓词逻辑表示状态例4-6机器人移盒子问题：在一个包含有凹室(Alcove)的房间内有两张桌子A和B，一个机器人(Robot)和一个盒子(Box)，如图4-2所示。我们的任务是让机器人从凹室出发，把桌子A上的盒子移到桌子B上，然后回到凹室。试用谓词逻辑描述这一行动过程。图4-2机器人移盒子初始状态Robot首先定义以下几个谓词:①TABLE(x)：X是桌子；②EMPTYHANDED(y)：y手中是空的；③AT(y，z)：y在z的附近；④HOLDS(y，w)：y手中拿着w；⑤ON(w，x)：w在x桌面上。其中x，y，z，w个体域分别是{a，b}，{robot}，{a，b，alcove}，{box}。

图4-2机器人移盒子初始状态Robotabalcove

box机器人问题的初始状态和目标状态问题的初始状态是下列问题的合取:AT(robot，alcove)EMPTYHANDED(robot)

ON(box，a)TABLE(a)TABLE(b)

问题的目标状态是下列问题的合取:AT(robot，alcove)EMPTYHANDED(robot)

ON(box，b)TABLE(a)TABLE(b)机器人的操作有三类①GOTO（x，y）：机器人从x处走到y处。条件：AT(robot，x)；动作:删除:AT(robot，x)；添加:AT(robot，y)。②PICKUPBOX(x):机器人在x处拿起盒子。条件:ON(box，x)，TABLE(x)，AT(robot，x)，EMPTYHANDED(robot)；动作:删除:EMPTYHANDED(robot)，ON(box，x)；添加:HOLDS(robot，box)。③SETDOWN(x):机器人在x处放下盒子。条件:AT(robot，x),TABLE(x)，HOLDS(robot，box)；动作:删除:HOLDS(robot，box)；添加:EMPTYHANDED(robot)，ON(box，x)。机器人行动规划问题的求解过程

状态1：AT(robot，alcove),EMPTYHANDED(robot),ON(box，a),TABLE(a),TABLE(b)状态2：AT(robot，a)，EMPTYHANDED(robot)，ON(box，a),TABLE(a),TABLE(b)状态3：AT(robot，a)，HOLDS(robot，box)，TABLE(a)，TABLE(b)状态4：AT(robot，b)，HOLDS(robot，box)，TABLE(a)，TABLE(b)状态5：AT(robot，b),EMPTYHANDED(robot),ON(box，b),TABLE(a),TABLE(b)状态6：AT(robot，alcove),EMPTYHANDED(robot),ON(box，b),TABLE(a),TABLE(b)图4-3机器人行动规划问题的求解过程目标状态初始状态GOTO(x，y)用alcove代换x，a代换y用a代换xPICKUPBOX(x)用a代换x，b代换yGOTO(x，y)用b代换xSETDOWN(x)用b代换x，GOTO(x，y)alcove代换y5.逻辑表示与推理例4-7已知下面事实：试问马科斯还活着吗？⑴马科斯是男人；⑵马科斯是庞贝人；⑶马科斯出生于公元40年；⑷所有的人都会死；⑸所有庞贝人都死于公元79年的火山爆发；⑹公元79年的火山爆发；⑺所有会死的人数不会超过150岁；⑻现在是2002年⑼活意即未死；⑽如果某人死了，那么他后来的任何时刻都死了。马科斯问题的逻辑表示⑴MAN(marcus)；⑵POMPEIAN(marcus)；⑶BORN(marcus，40)；⑷()[MAN(x)→MORTAL(x))；⑸ERUPTED(volcano，79)∧()[POMPEIAN(x)→DIED(x，79)]；⑹ERUPTED(volcano，79)；⑺[MORTAL(x)∧BORN(x,t1)∧GT(T2-t1,150)→DEAD(x,t2)]⑻NOW=2011；⑼ALIVE(x，t)～DEAD(x,t)；⑽[DEAD(x,t1)∧GT(t2，t1)→DEAD(x,t2)]马科斯问题的证明过程

图4-4证明马科斯已死的过程～ALIVE(marcus，now)用9代换DEAD(marcus，now)用10代换DEAD(marcus,t1)∧GT(now，t1)用5代换ERUPTED(volcano，79)∧POMPEIAN(marcus)∧GT(now，79)用6、2代换GT(now，79)用8代换GT(2011，79)计算GTnil4．3逻辑推理的技术与算法

4．3．1子句集及其化简1.子句与子句集定义1：不含有任何联接词以及量词的谓词称为原子谓词。定义2：文字是原子谓词及其否定形式的统称。例如：P(x)、～P(x)、Q(x，y)、～Q(x，y)等都是文字。定义3：若P是原子谓词，则称P与～P为互补文字。定义4：若干个文字的一个析取式称为一个子句，例如：P(x)∨(～Q(x))；P(x，f(x))∨Q(x，g(x))都是子句。定义5：由r个文字组成的子句叫r-文字子句。定义6：1-文字子句叫单元子句。定义7：不含任何文字的子句叫空子句，记为□或NIL，空子句是永假的，不可满足的。定义8：所谓子句集是由子句或空子句构成的一种集合。2.子句集的化简⑴消去联结词“→”、“”。⑵缩小否定词～的使用范围。⑶变元适当改名(标准化)。使量词间不含同名指导变元和约束变元。⑷化为前束范式。⑸消去存在量词。。①若存在量词左边没有全称量词，只要用新的个体常量替换该存在量词约束的变元，同时消去该存在量词。②若存在量词位于一个或多个全称量词的辖域内(存在量词在右边)，则用这些全称量词指导变元的一个函数代替该存在量词辖域中的相应约束变元。⑹化为Skolem标准形。⑺消去所有全称量词。⑻消去合取词，把母式用子句集的形式表示出来。⑼更换变元名称，使子句间无同名变元。2.子句集的化简（1/6）

在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则化成相应的子句集。其化简步骤如下：

(1)消去连接词“→”和“↔”反复使用如下等价公式：

P→Q⇔～P∨QP↔Q⇔(P∧Q)∨(～P∧～Q)即可消去谓词公式中的连接词“→”和“↔”。例如公式

(∀x)((∀y)P(x,y)→～(∀y)(Q(x,y)→R(x,y)))经等价变化后为

(∀x)(～(∀y)P(x,y)∨～(∀y)(～Q(x,y)∨R(x,y)))(2)减少否定符号的辖域反复使用双重否定率～(～P)⇔P摩根定律～(P∧Q)⇔～P∨～Q

～(P∨Q)⇔～P∧～Q量词转换率～(∀x)P(x)⇔(∃x)～P(x)

～(∃x)P(x)⇔(∀x)￢P(x)将每个否定符号“～”移到仅靠谓词的位置，使得每个否定符号最多只作用于一个谓词上。例如，上式经等价变换后为

(∀x)((∃y)～P(x，y)∨(∃y)(Q(x，y)∧～R(x，y)))2.子句集的化简（2/6）

(3)对变元标准化在一个量词的辖域内，把谓词公式中受该量词约束的变元全部用另外一个没有出现过的任意变元代替，使不同量词约束的变元有不同的名字。例如，上式经变换后为

(∀x)((∃y)～P(x，y)∨(∃z)(Q(x，z)∧～R(x，z)))(4)化为前束范式化为前束范式的方法:把所有量词都移到公式的左边，并且在移动时不能改变其相对顺序。由于第(3)步已对变元进行了标准化，每个量词都有自己的变元，这就消除了任何由变元引起冲突的可能，因此这种移动是可行的。例如，上式化为前束范式后为

(∀x)(∃y)(∃z)(～P(x，y)∨(Q(x，z)∧～R(x，z)))2.子句集的化简（3/6）

(5)消去存在量词消去存在量词时，需要区分以下两种情况：

若存在量词不出现在全称量词的辖域内（即它的左边没有全称量词），只要用一个新的个体常量替换受该存在量词约束的变元，就可消去该存在量词。

若存在量词位于一个或多个全称量词的辖域内，例如

(∀x1)…(∀xn)(∃y)P(x1，x2,…,xn,y)则需要用Skolem函数f(x1，x2,…,xn)替换受该存在量词约束的变元y，然后再消去该存在量词。例如，上步所得公式中存在量词(∃y)和(∃z)都位于(∀x)的辖域内，因此都需要用Skolem函数来替换。设替换y和z的Skolem函数分别是f(x)和g(x)，则替换后的式子为

(∀x)(～P(x,f(x))∨(Q(x,g(x))∧～R(x,g(x))))2.子句集的化简（4/6）

(6)化为Skolem标准形

Skolem标准形的一般形式为

(∀x1)…(∀xn)M(x1,x2,……,xn)其中，M(x1,x2,……,xn)是Skolem标准形的母式，它由子句的合取所构成。把谓词公式化为Skolem标准形需要使用以下等价关系

P∨(Q∧R)⇔(P∨Q)∧(P∨R)例如，前面的公式化为Skolem标准形后为

(∀x)((～P(x,f(x))∨Q(x,g(x))∧(～P(x,f(x))∨～R(x,g(x))))(7)消去全称量词由于母式中的全部变元均受全称量词的约束，并且全称量词的次序已无关紧要，因此可以省掉全称量词。但剩下的母式，仍假设其变元是被全称量词量化的。例如，上式消去全称量词后为

(～P(x,f(x))∨Q(x,g(x))∧(～P(x,f(x))∨～R(x,g(x)))2.子句集的化简（5/6）

(8)消去合取词在母式中消去所有合取词，把母式用子句集的形式表示出来。其中，子句集中的每一个元素都是一个子句。例如，上式的子句集中包含以下两个子句～P(x,f(x))∨Q(x,g(x))

～P(x,f(x))∨～R(x,g(x))(9)更换变量名称对子句集中的某些变量重新命名，使任意两个子句中不出现相同的变量名。由于每一个子句都对应着母式中的一个合取元，并且所有变元都是由全称量词量化的，因此任意两个不同子句的变量之间实际上不存在任何关系。这样，更换变量名是不会影响公式的真值的。例如，对前面的公式，可把第二个子句集中的变元名x更换为y，得到如下子句集～P(x,f(x))∨Q(x,g(x))

～P(y,f(y))∨～R(y,g(y))2.子句集的化简（6/6）将逻辑表达式化成子句集例4-8求下列谓词表达式的子句集。解：利用上述步骤，按以下步骤进行求解：⑴消去：⑵否定深入：⑶变元改名：⑷化为前束范式：⑸消去存在量词：将逻辑表达式化成子句集⑹化为Skolem标准形：⑺消去全称量词：⑻消去合取词：⑼更换变元名称：4．3．2置换与合一

1.置换置换是在一个谓词表达式中用置换项去替换变量，其一般形式为有限集合{t1/x1，t2/x2，…，tn/xn}。其中xi是变量，ti是不同于xi的项，可以是常量、函数，或者其他的变量。xi≠xj(i≠j│i，j∈1，2，…，n)，ti/xi表示用ti替换xi，xi不能循环地出现在另一个ti中。例如{a/x，b/y，f(c)/z}是一个置换，而{g(y)/x，f(x)/y}就不是一个置换，原因是它在x和y之间出现了循环置换现象。通常置换用希腊字母θ、σ、α、λ表示。置换的例示在谓词表达式W=P[x，f(y)，B]中，若用置换θ={t1/x1，t2/x2，…，tn/xn}，把W中所有的xi全部换成ti(i=1，2，…，n)，记为Wθ，所得结果称为W在置换θ下的例示。表4-4四种不同的例示序号置换置换的例示①θ1=｛z/x，w/y｝Wθ1=P[x，f(y)，B]θ1=P[z，f(w)，B]②θ2=｛A/y｝Wθ2=P[x，f(y)，B]θ2=P[x，f(A)，B]③θ3=｛g(z)/x，A/y｝Wθ3=P[x，f(y)，B]θ3=P[g(z)，f(A)，B]④θ4=｛c/x，A/y｝Wθ4=P[x，f(y)，B]θ4=P[c，f(A)，B]复合置换若有两个置换θ={t1/x1，t2/x2，…，tn/xn}，λ={u1/y1，u2/y2，…，um/ym}。①当tiλ=xi时，删去tiλ/xi(i=1，2，…，n)；②当yi∈{x1，x2，…，xn}时，删去uj/yj(i=1，2，…，m)；称集合{t1λ/x1，t2λ/x2，…，tnλ/xn，u1/y1，u2/y2，…，um/ym}最后所剩下的元素为置换θ与λ的复合置换，记为θ•λ。复合置换举例例4-9设θ={f(y)/x，z/y}，λ={a/x，b/y，y/z}，求θ•λ。解：∵θ•λ={t1λ/x1，t2λ/x2，u1/y1，u2/y2，…，u3/y3}={f(b/y)/x，(y/z)/y，a/x，b/y，y/z}={f(b)/x，y/y，a/x，b/y，y/z}其中y/y满足条件①，a/x、b/y满足条件②给予删除。从而得到：θ•λ={f(b)/x，y/z}一般情况下复合置换是不可交换的，即θ•λ≠λ•θ。2.合一合一是通过对项进行置换，使两个谓词表达式达到一致的过程，通过合一，可把若干表达式合为一个表达式。合一的一般定义为：设W={W1，W2，…，Wn}，若存在一个置换θ，可使W1θ=W2θ=…=Wnθ，则称θ是W的一个合一，称W是可以合一的。一般一个表达式集的合一不唯一。若σ是表达式集W的一个合一，如果对W的任意一个合一θ，都存在一个置换λ，使得θ=σ•λ，则称σ为W的最一般合一。一个表达式集的最一般合一是唯一的。例如

W={P(u，y，g(y))，p(x，f(u)，z)}有一个最一般合一：σ={u/x，f(u)/y，g(f(u))/z}；例如θ={a/x，f(a)/y，g(f(a))/z，a/u}，存在一个置换：λ={a/u}，使得θ=σ•λ。4．3．3鲁滨逊消解(归结)原理1.命题逻辑的消解原理命题逻辑的消解原理因为P→Q，Q→RP→R，即(～P∨Q)∧(～Q∨R)(～P∨R)，也就是说由C1∨L和～L∨C2可以推出C1∨C2来。基本思想注意以下两个关键第一，子句集中的子句之间是合取关系。因此，子句集中只要有一个子句为不可满足，则整个子句集就是不可满足的；第二，空子句是不可满足的。因此，一个子句集中如果包含有空子句，则此子句集就一定是不可满足的。鲁滨逊归结原理基本思想首先把欲证明问题的结论否定，并加入子句集，得到一个扩充的子句集S'。然后设法检验子句集S'是否含有空子句，若含有空子句，则表明S'是不可满足的；若不含有空子句，则继续使用归结法，在子句集中选择合适的子句进行归结，直至导出空子句或不能继续归结为止。鲁滨逊归结原理包括命题逻辑归结原理谓词逻辑归结原理定义设C1、C2是命题逻辑中的任意两个子句，如果C1中文字L1与C2中文字L2互补，那么可以从C1和C2中分别消去L1和L2，并将余下的两个子句析取构成一个新的子句C12，则称这一过程为消解(归结)，称C1和C2为C12的亲本子句，称C12为C1和C2的消解式。即：C12=(C1-{L1})∨(C2-{L2})。若C1=P∨R，C2=～P∨Q，则C12=R∨Q；若C1=～P∨Q∨R，C2=～Q∨S，则C12=～P∨R∨S；若C1=P∨Q，C2=P∨R，则C12

不存在；若C1=～P∨Q，C2=～Q，C3=P，则C12=～P，C123=NIL(□)；定理和推论定理消解式C12是其亲本子句C1和C2的逻辑结论。推论如果C1和C2是子句集S的两个子句，C12为C1和C2的消解式，则①若用C12代替C1和C2，所得的新子句集S1保持着原子句集S的不可满足性。即：

S1不可满足S不可满足②若把C12加入S中得到新的子句集S2，则S与S2的不可满足性是等价的。即：

S2不可满足S不可满足消解举例例4-10证明S={P∨Q,～P∨Q，P∨～Q，～P∨～Q}是不可满足的子句集。证明①P∨Q②～P∨Q③

P∨～Q④～P∨～Q⑤Q(由①，②式)⑥～Q(由③，④式)⑦□(由⑤，⑥式)所以S是不可满足的

QP∨Q～P∨QP∨～Q～P∨～Q图4-5消解演绎树～Q□消解过程已知子句集E，证明G为真的过程如下：①否定结论G为～G；②把～G并入到E中，得到{E，～G}；③把{E，～G}化为子句集S；④对S中的子句进行消解，并把每次得到的消解式并入S中，力图推导出一个表示矛盾的空子句NIL。如此反复进行，若出现空子句，则停止消解，这样就证明了G为真。求证结论为真示例例4-11若已知子句集为{P，(P∧Q)→R，T→Q，T}，求证结论为R。证明：否定结论R为～R，将～R加入子句集，并化为新子句集：S={P，～P∨～Q∨R，～T∨Q，T，～R}出现空子句，因此命题R得证。～R～P∨～Q∨R□～P∨～Q～Q～T图4-6消解反演树P～T∨QT2.谓词逻辑中的消解谓词逻辑子句集中的谓词一般都含有变元，因而需要先用一个最一般合一对变元进行替换，然后才能进行消解。定义设C1和C2是两个没有公共变元的子句，L1、L2

分别是C1、C2中的两个文字，如果L1和～L2存在一个最一般合一σ，则称

C12=(C1σ—{L1σ})∪(C2σ—{L2σ})为C1和C2的二元消解式，而L1和L2为消解式上的文字。二元消解式举例例4-12设C1=P(x)∨Q(x)，C2=～P(a)∨R(x)，求C12。选L1=P(x)，L2=～P(a)，可得L1、L2的最一般合一为：σ={a/x}。从而C12=(C1σ—{L1σ})∪(C2σ—{L2σ})=({P(a),Q(a)}—{P(a)})∪({～P(a),R(y)}—{～P(a)}={Q(a)}∪{R(y)}=Q(a)∨R(y)

二元消解式的几种情况定义若C1和C2是无公共变元的子句，C1、C2的消解式C12是下列二元消解式之一。C1和C2的二元消解式；C1和C2的因子C2σ的二元消解式；C1的因子C1σ和C2的二元消解式；C1的因子C1σ和C2的因子C2σ的二元消解式。定理与举例定理谓词逻辑中的消解式C12是其亲本子句C1和C2的逻辑结论。例4-13如果有C1=P(x)∨P(f(y))∨R(g(y))，C2=～P(f(g(a)))∨Q(b)，求C12。解：对C1取最一般合一σ={f(y)/x}，得C1的因子C1σ=P(f(y))∨R(g(y))；P(f(y))和～P(f(g(a)))的最一般合一是θ={g(a)/y}，所以得到C1和C2的二元消解式：C12=R(g(g(a)))∨Q(b)证明逻辑结论成立举例例4-14求证G是F1和F2的逻辑结论。

F1：(x)(P(x)→(x)(Q(y)→～L(x，y)))F2：(x)(P(x)∧(y)(R(y)→L(x，y)))

G：(x)(R(x)→～Q(x))证明：首先将F1、F2和～G化成Skolem范式，利用量词消去规则，并改名得：①～P(x)∨～Q(y)∨～L(x，y)(由F1)②P(a)③～R(z)∨L(a，z)④R(b)⑤Q(b)⑥L(a，b)(由③，④式，取σ1={b/z})⑦～Q(y)∨～L(a，y)(由①，②式，取σ2={a/x})⑧～Q(b)(由⑥，⑦式，取σ3={b/y})⑨□(由⑤，⑧式)因此,G是F1和F2的逻辑结论。(由F2)(～G)经典的消解问题1例4-14“快乐学生”问题。现假设：任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可通过所有考试，张三不肯学习但他是幸运的，任何幸运的人都能获奖。试证明张三是快乐的。解：先定义谓词：①PASS(x,y)：x可以通过y考试；②WIN(x,award)：x能获得奖励；③STUDY(x)：x肯学习；④ENJOYMENT(x)：x是快乐的；⑤LUCKY(x)：x是幸运的。经典的消解问题1⑴任何通过计算机考试并获奖的人都是快乐的；(x)((PASS(x，computer)∧WIN(x，award))→ENJOYMENT(x))⑵任何肯学习或幸运的人都可通过