1、 第六章 逻辑式程序设计语言逻辑式语言基本形式:用一种符号逻辑作为程序设计语言来进行程序设计,通常称为逻辑程序设计语言,或声明性语言第1页,共47页。第六章 逻辑式程序设计语言程序要对数据结构实施某个算法过程,算法实现计算逻辑 算法=逻辑+控制逻辑程序设计的基本观点是程序描述的是数据对象之间的关系。关系也是联系对象和对象、对象和属性的联系就是我们所说的事实。事实之间的关系以规则表述,根据规则找出合乎逻辑的事实就是推理逻辑程序设计范型是陈述事实、制定规则,程序设计就是构造证明。程序的执行就在推理第2页,共47页。6.1谓词演算谓词演算 谓词演算是符号化事实的形式逻辑系统,它也是逻辑程序设计语言的
2、模型 表示命题 表示命题之间的关系 描述如何根据假设为真的命题推断出新命题 谓词演算诸元素谓词演算诸元素 用形式方法研究论域上的对象需要一种语言,它能表达该域对象具有什么性质(properties),以及对象间有些什么关系(relations)描述以公式(Formulas)表达。谓词公式中各元素按一定逻辑规则变换,即谓词演算(predicate calculus)第3页,共47页。(1)公式 由一组约定的符号组成的序列,它包括常量、变量、逻辑连接、命题函数、谓词、量词(2)常量 指明论域上的对象(3)变量 可束定到特定域上某个范围的对象上(4)函数 表征对象具有的映射关系(5)谓词 表征对象某
3、种性质的符号(6)量词 量词限定的变量名作用域是整个公式(7)逻辑操作 and,or,not,(蕴含)(全等)当谓词应用到的变元是常量或已被束定的变量上时,就叫做句子(sentence)或命题(proposition)第4页,共47页。谓词变元的个数称作目(arity),有单目、N目谓词之称 N-目谓词的例子。谓词 目 含义 odd(X)1 X是奇数 father(F,S)2 F是S的父亲 divide(N,D,Q,R)4 N除D得商Q和余数R 谓词例化 结果值 odd(2)False divide(23,7,3,2)Ture father(changshan,changping)True d
4、ivide(23,7,3,N)N未例化,不知真假第5页,共47页。谓词的量化量化谓词 结果值 Xodd(X)False Xodd(X)True X(X=2*Y+1odd(X)True XYdivide(X,3,Y,0)True,如X=3,Y=1XYdivide(X,3,Y,0)FalseXYdivide(X,3,Y,0)False,但很难证明第6页,共47页。第7页,共47页。谓词演算的等价变换谓词演算的等价变换1以,消除、符号2化为前束范式,消除最外的符号,否定符号内移(XP(X)X(p(X)3用斯柯林变换消去存在量词 X(a(X)b(X)Y c(X,Y)X(a(X)b(X)c(X,g(X)
5、4 消除前束范式的全称量词 a(X)b(X)c(X,g(X)一般谓词公式变换为子句的实例。一般谓词公式变换为子句的实例。号为号为“可推可推出出”第8页,共47页。5用分配率P(QR)=(PQ)(PR)化成合取范式 (a(X)c(X,g(X)(b(X)c(X,g(X)经过以上变换,任何一复合公式均可成为如下形式:F=C1C2 Cn 且其中Ci称为子句 若以;代则有:Ci=L1 L2 Lv=L1;L2;Lv 因此,任一公式均可化为连接的子句的集合第9页,共47页。6.2 自动定理证明自动定理证明 证明系统证明系统 事实即证明系统中的公理(axioms)证明系统(proof system)是应用公理
6、演绎出定理 (theorems)的合法演绎规则的集合 演绎也叫归约(deduction),是对证明系统中合法 推理规则的一次应用 演绎从公理导出结论(conclusion),中间可利用以 这些规则演绎出的定理证明证明(proof)是个语句序列,以每个语句得到证明而结束,即每个句子要么演绎成公理,要么演绎成前此导出的定理第10页,共47页。一个证明若有一个证明若有N个语句个语句(命题命题)则称则称N步证明步证明反驳反驳(refutation)是一个语句的反向证明。是一个语句的反向证明。它证明它证明 一个语一个语句是矛盾的,句是矛盾的,即不合乎给定的公理即不合乎给定的公理一个语句若能从公理出发推演
7、出来,一个语句若能从公理出发推演出来,则称则称合法语句合法语句,任何合法语句也叫做任何合法语句也叫做定理定理(theorem)从某一公理集合导出的所有定理集合称为从某一公理集合导出的所有定理集合称为理论理论(theory)第11页,共47页。模型模型 从公理集合中导出定理集称之为从公理集合中导出定理集称之为理论理论,有了理论我们,有了理论我们要解释它的语义必须借助某个要解释它的语义必须借助某个模型模型(model)。因为形式系因为形式系统只是符号抽象,借助模型我们可为每个常量、函数、谓词统只是符号抽象,借助模型我们可为每个常量、函数、谓词符号找到真理性的解释。即定义每个论域,并表明域上成员符号
8、找到真理性的解释。即定义每个论域,并表明域上成员和常量公理之间的关系。和常量公理之间的关系。公理的谓词符号必须派定为域中对象的性质,公理的谓词符号必须派定为域中对象的性质,函函数派定为对域中对象的操作。数派定为对域中对象的操作。公理集合一般情况下只是定义的部分公理集合一般情况下只是定义的部分(偏偏)函数和谓词,函数和谓词,是问题域的一个侧面。是问题域的一个侧面。所以能满足该理论的模型往往不止所以能满足该理论的模型往往不止一个。一个。第12页,共47页。例例 一个最简单的理论一个最简单的理论 公理集公理集:Xinterval(X)not interval(X+1)(a1)Xnot interva
9、l(X+1)interval(X)(a2)2=1+1 (a3)从间隔数公理可导出定理从间隔数公理可导出定理:Xinterval(X)interval(X+2)(t1)Xinterval(X+2)interval(X)(t2)谓词谓词interval(间隔数间隔数)在整数域上有两个子域在整数域上有两个子域odd、even都能够满足间隔数都能够满足间隔数理论不能证明理论不能证明interval(3),也不能证明,也不能证明not interval(3)为真命题。这就是为真命题。这就是Hilbert讨论过的讨论过的可判定可判定(decidability)问题。问题。1936年年Church和和Tur
10、ing证实谓词演算可判定性问题是没有解的证实谓词演算可判定性问题是没有解的一旦我们断言一旦我们断言interval(3)或或interval(2)是真命题是真命题,我们立刻可通过演绎证明我们立刻可通过演绎证明按这个理论写出的每一个谓词为真。这就是按这个理论写出的每一个谓词为真。这就是Godel和和Herbrand1930年证实年证实的谓词演算具备的完整性的谓词演算具备的完整性(completeness)第13页,共47页。证明技术证明技术 从谓词演算具有完整性,从谓词演算具有完整性,理论上可证明按公理集理论上可证明按公理集合建立的任何理论。关键是效率。合建立的任何理论。关键是效率。如果我们从公
11、理出发做出每一个步骤,如果我们从公理出发做出每一个步骤,在新的步骤上在新的步骤上仍然要查找每一个公理,找出可能的推理。如此下去就形仍然要查找每一个公理,找出可能的推理。如此下去就形成一个庞大的树行公理集,成一个庞大的树行公理集,每层的结点表示一个公理的语每层的结点表示一个公理的语句,句,其深度和宽度随问题和最初给出的公理而定,其深度和宽度随问题和最初给出的公理而定,一层一层一步骤,一步骤,N层的树就是层的树就是N步推理。步推理。对于自动定理证明程序,对于自动定理证明程序,只有穷举每条可能的证明步只有穷举每条可能的证明步骤才能说它是完全的。骤才能说它是完全的。穷举完所有路径马上遇到组合爆炸穷举完
12、所有路径马上遇到组合爆炸问题,无论是深度优先还是广度优先,百步演绎可能的路问题,无论是深度优先还是广度优先,百步演绎可能的路径数都是天文数字。径数都是天文数字。第14页,共47页。归结定理证明归结定理证明 J.A.Robinson1965年提出的年提出的归结法归结法(resolution),是命题演,是命题演算中对合适公式的一种证明方法。算中对合适公式的一种证明方法。为了证明合适公式为了证明合适公式F为真,为真,归结法证明归结法证明 F恒假来代替恒假来代替F永真。永真。把两子句合一把两子句合一(unification)并消去一对正逆命题,故归结并消去一对正逆命题,故归结也译作也译作消解消解。归
13、结证明的过程并称之归结演绎,归结证明的过程并称之归结演绎,其步骤如下其步骤如下:第15页,共47页。1把前题中所有命题换成子句形式。把前题中所有命题换成子句形式。2取结论的反取结论的反,并转换成子句形式并转换成子句形式,加入加入1中的子句集中的子句集.3在子句集中选择含有互逆命题的命题归结。用合一算法得在子句集中选择含有互逆命题的命题归结。用合一算法得出新子句出新子句(归结式归结式),再加入到子句集。,再加入到子句集。4重复重复3,若归结式为空则表示此次证明的逻辑结论是,若归结式为空则表示此次证明的逻辑结论是矛盾,原待证结论若不取反则恒真。命题得证。矛盾,原待证结论若不取反则恒真。命题得证。否
14、则继否则继续重复续重复3。第16页,共47页。例:归结证明例:归结证明 若有前题若有前题 待证命题待证命题 取反得新子句取反得新子句 p1 Q P P U p5 P p2 R Q p6 U p3 S R p4 U S 取待证命题的反,取待证命题的反,得得PU,它是它是连接的两个子句连接的两个子句P、U,把它们加到前题子句集,把它们加到前题子句集,为为p5,p6。第17页,共47页。归结演绎如下图归结演绎如下图:Q P P p1-p5归结归结 Q R Q 再与再与p2归结归结 S R R 再与再与p3归结归结 S U S 再与再与p4归结归结 U U 再与再与p6归结归结 矛盾矛盾第18页,共4
15、7页。由本例可以看出两个问题:由本例可以看出两个问题:第一,归结法是由合一算法实现的。所谓第一,归结法是由合一算法实现的。所谓合一合一是找出型式匹是找出型式匹配的两子句,配的两子句,将它们合一为归结式,将它们合一为归结式,相当于代数中的化相当于代数中的化简。简。第二,如果得不出矛盾,那么归结法要无休止地做下去,第二,如果得不出矛盾,那么归结法要无休止地做下去,中间归结式出得越多,中间归结式出得越多,匹配查找次数越多,匹配查找次数越多,每一步都做每一步都做长时间计算。长时间计算。Solution:利用切断利用切断(cut)操作,操作,并利用对子句形式进一步并利用对子句形式进一步限制的限制的超级归
16、结法超级归结法(Hyperresolution)。第19页,共47页。Horn子句实现超归结子句实现超归结 Horn子句是至多只有一个非负谓词符号的子句子句是至多只有一个非负谓词符号的子句 Horn子句形式示例如下子句形式示例如下:P QS R T 其中只有一个非负谓词其中只有一个非负谓词S,可作以下演算:可作以下演算:先将先将S移向右方移向右方 S P Q R T 按德按德摩根定律摩根定律 S (PQRT)即即,则则 S(P Q R T)此条件此条件Horn子句的意义是子句的意义是 if S then(PQRT)。若若S为空,为空,则为无条件则为无条件Horn子句子句,是一个断言是一个断言(
17、事实事实)第20页,共47页。6.3 逻辑程序的风格逻辑程序的风格第一第一个特点是它不描述计算过程而是描述证明过程个特点是它不描述计算过程而是描述证明过程第二个特点是描述性第二个特点是描述性第三个特点是大量用表和递归实现重复操作第三个特点是大量用表和递归实现重复操作sort(old_list,new_list)permute(old_list,new_list)sorted(new_list)sorted(list)j 使得 1 j n,list(j)list(j+1)*permute是一个谓词,如果第二个参数组是第一个参数组的一个排列,就返回真第21页,共47页。Prolog语言 Prolo
18、g是一种基于一阶谓词的逻辑式语言 Prolog是基于Horn子句的,使用归结推理,具有很强的逻辑描述能力和推理能力 Prolog语言特点:一阶逻辑的语言形式是形式化地严格定义的 一阶逻辑的语法简易易懂 逻辑公式不需要重复表达,与不同应用无关 事实、假设、推理、查询、视图和完整性规约条件都能以基于一阶逻辑的prolog语言表达 逻辑语言Prolog可作为定义和比较其它知识表示模型的共同模型第22页,共47页。例例 求平均成绩的逻辑程序,打开一分数文件求平均成绩的逻辑程序,打开一分数文件scores,读读入分数求和并用的数入分数求和并用的数N除之得平均成绩除之得平均成绩 average:-see(
19、scores),getinput(Sum,N),seen(scores),Av is Sum/N,print(Average=,Av)getinput(Sum,N):-ratom(X),not(eof),getinput(Sum1,N1),Sum is Sum1+X,N is N11.getinput(0,0):-eof.第23页,共47页。6.4 典型逻辑程序设计语言典型逻辑程序设计语言Prolog Prolog要环境支持要环境支持,即管理事实和规则的数据库即管理事实和规则的数据库 Prolog的基本成分是对象的基本成分是对象(常量、变量、结构、表常量、变量、结构、表)、谓词、运算、谓词、运
20、算符、函数、规则符、函数、规则 从从纯语法纯语法意义上意义上Prolog的项什么都可以表示的项什么都可以表示:=|()|第24页,共47页。从从语义语义角度,角度,以下语法描述提供了处理时的语义概念以下语法描述提供了处理时的语义概念:(|):-,/*形如形如p或或q(T,)的字面量的字面量*/第25页,共47页。与Prolog交互?-(在每轮交互开始时系统都会给出“提示符号”)表示希望得到一个查询?-consult(links).Consult结构读入包含事实和规则的文件,并将这些内容添加到当前规则数据库末尾。?-link(algol60,L),link(L,M).L=cplM=bcpl表示:
21、是否存在L和M,使link(algol60,L)and link(L,M)?输入“;”并回车,Prolog将用另一个解作为响应,或者用“no”说明已经无法在找到解。规则的表示规则就是horn子句:-1,2,k.:-左边的项称为头部,在:-右边的那些项称为条件。事实是规则的特殊形式,只有头部而没有条件。Path(L,L).Path(L,M):-link(L,X),path(X,M).其中变量X,出现在条件里面,而不在头部,表示某个满足条件的对象第26页,共47页。与Prolog交互合一?-f(X,b)=f(a,Y).X=aY=b得到项T的实例方法:用一些项去替换T中的一个或几个变量。同一个变量的
22、所有出现必须用同一个项去替换。f(a,b)是f(X,b)的实例,同理f(a,b)是f(a,Y)的实例。共同的实例是f(a,b)。g(a,b)不是g(X,X)的实例合一是在规则应用时隐含发生的。算术:“=”运算符表示合一?-X=2+3 X=2+3中缀运算符“is”对表达式求值:?-X is 2+3 X=5第27页,共47页。Prolog程序结构程序结构 Prolog程序由子句组成,程序由子句组成,子句模型是子句模型是Horn子句。子句。(1)事实与规则事实与规则 Prolog程序先定义公理集程序先定义公理集例:例:Prolog的规则和事实的规则和事实 条件子句条件子句(规则规则)pretty(X
23、):-artwork(X)pretty(X):-color(X,red),flower(X).watchout(X):-sharp(X,_).无条件子句无条件子句(事实事实)color(rose,red).sharp(rose,stem).sharp(holly,leaf).flower(rose).flower(violet)artwork(painting(Monet,haystack_at_Giverny).第28页,共47页。(2)查询查询 Prolog中查询中查询(query)是要求是要求Prolog证明定理。证明定理。因为提出的问因为提出的问题就是证明过程的目标题就是证明过程的目标
24、,所以查询也叫目标所以查询也叫目标(goal)。例例:Prolog的查询的查询?-pretty(rose).yes?-pretty(Y).Y=painting(Monet,haystack_at_Giverny).Y=rose.no?-pretty(W),sharp(W,Z)W=rose Z=stem no 第29页,共47页。例例:最大公约数的欧基里得算法最大公约数的欧基里得算法 最大公约数欧基里得算法可用三条规则描述最大公约数欧基里得算法可用三条规则描述:gcd(A,0,A).gcd(A,B,D):-(AB),(B0),R is A mod B,gcd(B,R,D).gcd(A,B,D):
25、-(AB),gcd(B,A,D).第30页,共47页。封闭世界内的假设封闭世界内的假设 如果有某个子目标查遍数据库也找不到能满足的如果有某个子目标查遍数据库也找不到能满足的事实,事实,该子目标失败,该子目标失败,但不等于整个目标的失败。但不等于整个目标的失败。即使是整个目标最后失败,即使是整个目标最后失败,也不等于这个目标追求的命也不等于这个目标追求的命题是否定的,题是否定的,因为限于数据库存放的规则和事实有限,因为限于数据库存放的规则和事实有限,它是它是“封闭世界假说封闭世界假说”之下的失败。之下的失败。第31页,共47页。函数和计算函数和计算(1)函子完成逻辑设计中的计算函子完成逻辑设计中
26、的计算 函子以结构形式出现,函子以结构形式出现,如如:中缀表示中缀表示 前缀表示前缀表示 X+Y*Z +(X,*(Y,Z)A-B/C -(A,/(B,C)故它不是谓词,仅仅是一特殊的结构:故它不是谓词,仅仅是一特殊的结构:(,)函数求值的的结果一般通过谓词函数求值的的结果一般通过谓词is(,)束束定到变元上定到变元上gcd(A,B,D);-(AB),(B0),R is A mod B,gcd(B,R,D).把把函数改写为约束,很容易写出函数改写为约束,很容易写出prolog程序程序第32页,共47页。第33页,共47页。(2)逻辑程序的算法表达逻辑程序的算法表达 算法怎样用公理表达呢?拿一个最
27、典型的算法怎样用公理表达呢?拿一个最典型的Quicksort分类程分类程序讨论。序讨论。quicksort(未分类表,分类完的表未分类表,分类完的表):-(从未分类表拿出第一元素从未分类表拿出第一元素,以它为基准以它为基准,分成两个表分成两个表),1 quicksort(小表,分类完小表小表,分类完小表),2 quicksort(大表,分类完大表大表,分类完大表),3 append(分类完小表,分类完小表,基准元素和分类完大表,分类完总表基准元素和分类完大表,分类完总表)4这样把快速分类的总目标变成了四个子目标这样把快速分类的总目标变成了四个子目标第34页,共47页。例例 快速分类的快速分类的
28、Prolog代码代码 r1 split(_,).r2 split(Pivot,Head|Tail,Head|Sm,Lg):-Head Pivot,split(Pivot,Tail,Sm,Lg).r3 split(Pivot,Head|Tail,Sm Head|Lg):-Pivot Head,split(Pivot,Tail,Sm,Lg).r4 quicksort(,).r5 quicksort(Head ,Head).r6 quicksort(Pivot|Unsorted AllSorted):-split(Pivot,Unsorted,Small,Large),quicksort(Small
29、,SmSorted),quicksort(Large,Lgsorted),append(SmSorted,Pivot|LgSorted,AllSorted).第35页,共47页。(3)逻辑和控制分离逻辑和控制分离 Prolog无通常意义的控制结构,也就是无通常意义的控制结构,也就是该程序动作次序(显然也有)和计算的子句该程序动作次序(显然也有)和计算的子句逻辑没有必然的关系。例如逻辑没有必然的关系。例如:把上例中把上例中r4,r5,r6写在写在r1,r2,r3前面并不影响本程序的前面并不影响本程序的执行结果。执行结果。第36页,共47页。cut和和not谓词谓词 因为因为Prolog的归结模型
30、只能完整地证明正命题,的归结模型只能完整地证明正命题,是是否有解无法判定否有解无法判定 如果明知再作没有意义,可人为截断如果明知再作没有意义,可人为截断cut(1)安全安全cut 非形式解释非形式解释cut,它如同一篱笆,它如同一篱笆,由程序员任意置放由程序员任意置放在规则之中,在规则之中,以停止无意义的回溯。以停止无意义的回溯。第37页,共47页。例例 安全安全cut示例:示例:求求1到到N的整数之和的整数之和 r1 sum_to(N,1):-N=1,!,!.r2 sum_to(N,R):-N1 is N-1,sum_to(N1,R1),R is R1+N.当有查询当有查询:?-sum_to
31、(1,X)/匹配匹配r1 X=1;/打打;号由于有!不致无限号由于有!不致无限 查找第查找第2个个 no?-sum_to(6,X)/匹配匹配r1失败,失败,匹配匹配r2连续连续r2 X=21;/直至成功,直至成功,打打;号也不再找号也不再找 no r1 可用可用sum_to(1,1).事实代事实代第38页,共47页。(2)cut 实现实现not操作操作 r1 not(X):-X,!,!,fail.r2 not(_).其推理过程是其推理过程是:若若X为假,匹配为假,匹配r1,在未达到!时已失败,则匹配规则在未达到!时已失败,则匹配规则r2,由于由于r2什么变元都可以且总为成功,所以,什么变元都可
32、以且总为成功,所以,not(X)是成是成功的。功的。若若X为真,匹配为真,匹配r1后,后,X为真,控制通过!传到为真,控制通过!传到fail,则则r1失败。失败。于是回溯到!过不去,只好失败。由于用了于是回溯到!过不去,只好失败。由于用了!就地失就地失败,它不再匹配败,它不再匹配r2,故故not(X)为失败。为失败。正是由于这个原因,正是由于这个原因,谓词谓词p和和not(not(p)求值结果不能保证求值结果不能保证一样,一样,有时有时not(p)和和not(not(p)求值结果倒是一样的,求值结果倒是一样的,以下以下是是not谓词出毛病的例子谓词出毛病的例子:第39页,共47页。例例 不可靠
33、的不可靠的not谓词谓词 假定一规则假定一规则test有以下定义有以下定义:test(S,T):-S=T.运行以下查询时有运行以下查询时有:?-test(3,5).no?-test(5,5)yes?-not(test(5,5)no?-test(X,3),R is X+2.X=3 R=5?-not(not test(X,3),R is X+2.!error in arithmetic expression:not a numberr1 not(X):-X,!,!,fail.r2 not(_).由于第二次由于第二次not(外部的外部的)求值时求值时用到上例规则用到上例规则r1,其中其中X是是not
34、(test(X,3)的结果值,故的结果值,故X+2不是数加不是数加2。这个问题原这个问题原因在于子句逻辑的不可判定因在于子句逻辑的不可判定性性第40页,共47页。(3)不安全的不安全的cut cut使我们处于两难的境地,使我们处于两难的境地,它的高效是以风它的高效是以风险为代价得到的,如同险为代价得到的,如同60年代年代goto技巧对非结构化技巧对非结构化程序的影响。只要模型是超级归结,程序的影响。只要模型是超级归结,cut的两面性是不的两面性是不可以解决的。可以解决的。第41页,共47页。6.5 Prolog评价评价 Prolog提供一种证明风格的声明式程序设计,提供一种证明风格的声明式程序
35、设计,推理清晰,推理清晰,概括能力强,概括能力强,程序和数据没有明显分离。程序和数据没有明显分离。Prolog程序具有自文档性程序具有自文档性 由于非过程性,它也成为潜在的并行程序设计语言的候选者由于非过程性,它也成为潜在的并行程序设计语言的候选者 它的效率仍不及传统过程语言。由于它的声明性质,它的效率仍不及传统过程语言。由于它的声明性质,程程序员在优化算法时作用有限序员在优化算法时作用有限 复杂的大型系统一开始很难按照证明系统开发,复杂的大型系统一开始很难按照证明系统开发,程序不大运算程序不大运算量惊人量惊人,而而Prolog本身也只有局部量,本身也只有局部量,天生来也不是大天生来也不是大型
36、软件开发的工具。型软件开发的工具。因此,因此,Prolog只能作为逻辑程序设只能作为逻辑程序设计的独枝存在,计的独枝存在,解决大型应用多范型语言是个出路解决大型应用多范型语言是个出路第42页,共47页。归结练习已知:某些病人喜欢所有的医生(A1)没有一个病人喜欢任意一个骗子(A2)欲证明:任意一个医生都不是骗子(B)证明:事实表示:令P(x):x是病人D(x):x是医生Q(x):x是骗子L(x,y):x喜欢yA1:x(P(x)y(D(y)L(x,y)A2:?B:?第43页,共47页。归结练习P(x):x是病人D(x):x是医生Q(x):x是骗子L(x,y):x喜欢yA1:x(P(x)y(D(y
37、)L(x,y)A2:x(P(x)y(Q(y)L(x,y)B:x(D(x)Q(x)要证明B是A1和A2的逻辑结果,即公式A1 A2 B是不可满足的第44页,共47页。归结练习A1=x(P(x)y(D(y)L(x,y)A2:x(P(x)y(Q(y)L(x,y)B:x(D(x)Q(x)A1=x(P(x)y(D(y)L(x,y)=x y(P(x)(D(y)L(x,y)-y(P(a)(D(y)L(a,y)A2=B=A1 A2 B的子句集是什么S=第45页,共47页。归结练习A1=x(P(x)y(D(y)L(x,y)=x y(P(x)(D(y)L(x,y)-y(P(a)(D(y)L(a,y)A2=x(P(x)y(Q(y)L(x,y)=x(P(x)y(Q(y)L(x,y)=x y(P(x)Q(y)L(x,y)B=(x(D(x)Q(x)=x(D(x)Q(x)-(D(b)Q(b)S=P(a),D(y)L(a,y),P(x)Q(y)L(x,y),D(b),Q(b)第46页,共47页。归结练习第47页,共47页。