第4讲归结原理不讲

《第4讲归结原理不讲》由会员分享，可在线阅读，更多相关《第4讲归结原理不讲（116页珍藏版）》请在金锄头文库上搜索。

1、人工智能原理人工智能原理第第 四四 讲讲 归结原理归结原理1归结原理归结原理n4.1 4.1 引言引言n4.2 4.2 一阶逻辑一阶逻辑n4.3 4.3 子句形子句形n4.4 Herbrand4.4 Herbrand定理定理n4.5 4.5 置换与合一置换与合一n4.6 4.6 归结原理归结原理n4.7 4.7 归结法的完备性归结法的完备性n4.8 4.8 归结策略归结策略2 4.1 引言引言n自动定理证明n历史n四色定理n三类方法3自动定理证明自动定理证明nAutomated Theorem Proving(ATP)n定理机器证明(Mechanical Theorem Proving)n为什

2、么？n定理证明是一种智能行为；n体现了人类的逻辑推理能力；n推理用计算来实现nLeibniz的梦想：nLeibniz imagined a universal formal calculus which could express reasoning in any subject, and an algorithmic procedure which could be applied to decide truth of statements in this calculus.4n1930年，Herbrand定理。n半可判定问题。n一阶逻辑的判定问题。n在一阶逻辑中，有没有方法可以判断任何一个

3、命题是否定理？(有没有方法可以判断任何一个公式能不能从公理及推理规则推导出来)。n数理逻辑的基本问题。n1936年，证明基本问题是不可解的。n在一阶逻辑中，如果一个定理是正确的，则有一个机械的方法在有限步内证明它。n一阶谓词逻辑有很强的表达能力，凡可计算的函数就可由一阶谓词表达。5历史历史nNewell，Shaw，Simonn1956年，The logic theory machine(逻辑理论机).n数学定理证明程序(Logic Theorist)nmimic human reasoningn数学原理第二章中的38个定理n1963年，经过改进的LT程序在一部更大的电脑上，最终完成了第二章全部

4、52条数学定理的证明。6n王浩n1958年，IBM704电脑，3-5分钟，证明了数学原理中有关命题演算的全部220条定理。n1959年，8.4分钟，证明了数学原理中全部（350条以上）定理。n罗素：“我真希望，在怀特海和我浪费了10年的时间用手算来证明这些定理之前，就知道有这种可能。” n1983年获得首届自动定理证明里程碑奖。7四色定理四色定理n1852年，一位21岁的大学生提出来的数学难题：任何地图都可以用最多四种颜色着色，就能区分任何两相邻的国家或区域。8四色定理四色定理 1976年7月，美国的阿佩尔(K.Appel)等人合作解决了长达124年之久的难题-四色定理。他们用三台大型计算机，

5、花去1200小时CPU时间，并对中间结果进行人为反复修改500多处。四色定理的成功证明曾轰动计算机界。 伊利诺斯数学杂志第21卷刊载的检验表(460p)9三类方法三类方法n基于归结的方法n类人的方法(human simulation)n判定方法10基于归结的方法基于归结的方法n1960年，Gilmore在计算机上实现了Herbrand算法。n1960年，M.Davis和H.Putnam的改进：nTautology Rule, One-literal Rule, Pure-literal Rule, Splitting Rule。n技巧而非本质：枚举基替换。n1960年，D.Prawitzn直接

6、寻找替换，避免组合爆炸。n思想深刻，效果不理想。n1965年，J.A.Robinson提出归结原理nOne-literal Rule的扩展。11n效率的提高n1965： Wos, G.A.Robinson, Curson, 支持集归结；n1967：Slagle，语义归结；n1970：Loveland，Luckham，线性归结；n1971：Boyer，锁归结；n1978：刘叙华，锁语义归结；n1979：王湘浩，刘叙华，广义归结；12类人的方法类人的方法( (human human simulation)simulation)n1956年，Newell，Shaw，Simon The logic t

7、heory machine(逻辑理论机)n1966年，MIT的L.M.Norton建造了ADEPT系统n群论的定理证明系统；n启发式；n1972年，R.Boyer和J.Mooren启发式策略和人机交互；n质因子分解唯一定理，验证编译程序的正确性；n1977年，Bledsoe：nNon-Resolution Theorem Proving(非归结定理证明)13判定方法判定方法n在较小的范围内找到一个有效的判定方法；n早期工作： A.Tarski的初等代数和初等几何的方法。n王浩：命题逻辑的一个有效的判定方法。n吴文俊：吴方法(1977)。14吴方法吴方法n平面几何定理n几何问题-代数问题n195

8、9年，Gelernter提出几何定理证明机(Geometry Theorem Proving Machine, GTM)n反向推理；n直线图形中大部分高中考试的问题；n运行时间与高中学生做题时间差不多；n获国际Herbrand自动推理杰出成就奖n“吴的工作将几何定理证明从一个不太成功的领域变为最成功的领域之一。在很少的领域中，我们可以将定理机器证明归于一个人的工作。几何定理证明就是这样的一个领域 ” (中国)15 4.2 一阶逻辑一阶逻辑n基本概念n合适公式n公式的解释n前束范式n合取范式与析取范式n逻辑结论16一一. 基本概念基本概念n定义(谓词)：n设D是非空个体名称集合，定义在Dn上，取

9、值于T，F上的n元函数，称为n元谓词。nDn表示集合D上的n次笛卡儿乘积。n例子：nMan(x)nGreater(x，y)171. 函数函数n函数(函词)n是一个映射： f: D D D Dn例子：nfather(x）182. 符号符号n常数：3，20.5，John，Confuciusn变量：x，y，zn函数：g，f，h，father，plusn谓词：Q，P，GREATER 193. 项项n定义定义(项项)：n常数是项；n变量是项；n如果f是一个n元函数符号，且t1，t2，. ，tn是项，则f(t1，t2，. ，tn)也是项；n所有项均是应用上述规则产生；n谓词不能是项。20二二. . 合适公

10、式合适公式( (wff, well-formed wff, well-formed formula)formula)n： 全称量词nx： 所有x，每个x；n：存在量词nx：存在一个x；211. 举例举例1.每个有理数是实数。2.存在一个数，它是素数。3.对每个数x，存在一个数y，使得xy。n令：nQ(x)：x是有理数； P(x)：x是素数；nR(x)：x是实数； LESS(x, y)；x1 的形式，其中Gi文字的析取式。n例子: (AB)(CD)(FG)n析取范式531. 1. 变换公式变换公式nFG = (FG) (GF)nFG = F GnFG = GF, FG = GF (交换律)n(F

11、G)H = F(GH) (结合律) (FG)H = F(GH)nF(GH) = (FG)(FH) (分配律) F(GH) = (FG)(FH)54n(F) = F (否定之否定)n(FG) = FG (狄摩根定律) (FG) = FGnF G = G； F G = F T G = T ； T G = G552. 2. 化公式为合取范式化公式为合取范式( (析取范式析取范式) )n消去和nFG = (FG) (GF)nFG = F Gn将代入每个原子前面n(F) = Fn(FG) = FG n(FG) = FGn使用:nF(GH) = (FG)(FH)nF(GH) = (FG)(FH)56例子例

12、子: :n(P(QG)S=(P(QG)S=(P(QG)S=P(QG)S=(PS)(QG)=(PSQ)(PSG)57六六. . 逻辑结论逻辑结论n定义(逻辑结论)n给定公式F1，F2， ，Fn和G，G是公式F1， F2， ，Fn的逻辑结论，当且仅当使F1，F2， Fn为真的任一个解释，使G为真。公式F1，F2， ，Fn称为G的公理。58定理定理1 1n定理1n给定公式F1，F2， ，Fn和G，G是公式F1， F2， ，Fn的逻辑结论，当且仅当公式 (F1F2Fn)G 为永真式。n证明：(F1F2Fn)G = (F1F2Fn)G= F1F2FnG59n(F1F2Fn)G = F1F2FnGn设G是

13、公式F1，F2， ，Fn的逻辑结论n要证：(F1F2FnG)是永真式nF1，F2，Fn均为真 nF1，F2，Fn中至少有一个为假n设公式(F1F2Fn)G为永真式n要证：G是公式F1，F2， ，Fn的逻辑结论n要证：当F1，F2，Fn为真，G为真n(F1F2FnG)是永真式60定理定理2 2n定理2n给定公式F1，F2，Fn和G，G是公式F1，F2， ，Fn的逻辑结论，当且仅当公式 F1F2FnG 不相容 (是永假式)n证明：n(定理1)给定公式F1, F2, Fn和G, G是公式F1, F2, Fn的逻辑结论, 当且仅当公式 (F1F2Fn)G 为永真式n(F1F2Fn)G)为永假式nF1F

14、2FnG61定理的定义定理的定义n定义(定理)n如果G是公式F1，F2，Fn的逻辑结论，则公式 (F1F2Fn)G 称为定理， G称为定理的结论。62 4.3 4.3 子句形子句形 设有由一阶谓词逻辑描述的公式A1,A2,A3和B，证明在A1A2A3成立的条件下有B成立。采用反演法来证明： A1A2A3B是不可满足的。和命题逻辑不同，首先遇到了量词问题，为此要将A1A2A3B化成SKOLEM标准形，进而建立子句集，方可使用 Herbrand 定理和归结原理来证明A1A2A3B成立。 63一一. . SKOLEM SKOLEM 标准形标准形 对给定的一阶谓词逻辑公式：G A1A2A3B首先化成与

15、其等值的前束范式：(Q1x1)(Q1xn)M(x1, xn)其中Qi(i=1,n)是存在量词或全称量词，而母式M(x1, xn)中不再含有量词。进而可将M(x1, xn)化成等值的合取范式。最后将所有存在量词消去，便得公式G的SKOLEM标准形了。 64二二. . 化化SKOLEM SKOLEM 标准形标准形的方法的方法消存在量词的过程如下：设(Qixi) 1in是第一个出现于(Q1x1) (Qixi) (Qnxn) M(x1,xn)中的存在量词，即Qi, Qi-1均为全称量词。* 若i1，则将M(x1,xn)中的所有变量x1均以某个常量C代之，但要求C不同于已出现在M(x1,xn)中的任一常

16、量。然后便可消去这个存在量词(Q1x1)即(x1)。* 若1in，(QiXi)的左边有全称量词(Qs1xs1), ,(Qsmxsm) 而1s1s2smi 则将M(x1,xi,xn)中的所有变量xi均以变量xs1, ,xsm的某个函数如f(xs1, ,xsm)代之，但要求f不同于已出现在M(x1,xn)中的任一函数，而对f的具体形式没有要求。然后消去这个存在量词(QiXi)。反复使用这种方法于(Q1x1)(Qnxn) M(x1,xn)，便可消去其中所有的存在量词，所得之公式称作公式G的 SKOLEM 标准形。 65 例例1 1 G( x)( y)( z)(P(x,y) Q(x ,z) R(x,y

17、,z),G已是前束形了，已是前束形了，需将需将M(x,y,z)化成合取范式。化成合取范式。 M(x,y,z)=(P(x,y)Q(x,z)R(x,y,z) =(P(x ,y)R(x ,y ,z)(Q(x ,y)R(x ,y ,z)于是G(x)(y)(z)(P(x,y)R(x,y,z)(Q(x,z)R(x,y,z) 先消去(y)，因其左边只有全称量词(x)，于是引入f(x)代入M(x ,y ,z)中的所有变量y。再消去(z)，它左边也只有(x)，也引入一个不同于f(x)的g(x)代入M(x,y,z)中的所有变量z。最后得： (x)(P(x,f(x)R(x ,f(x),g(x)(Q,x,g(x)R(

18、x,f(x),g(x) 便是G的 SKOLEM 标准形，其中f(x),g(x)称作 SKOLEM 函数。 66 例例2 2化公式化公式G G( ( x)(x)( y)(y)( z)(z)( u)(P(x ,y ,z ,u)u)(P(x ,y ,z ,u)为为SKOLEM SKOLEM 标标准形准形G已是前束形，M(x,y,z,u)=P(x,y,z,u)也已是合取范式。先消去(x)，因其左边没有全称量词，于是引入常量c代入P(x ,y ,z ,u)中的所有变量x。再消去(u)，它左边有全称量词(y)(z)，于是需引入一个二元函数f(y,z)代入P(x,y,z,u)中的变量u得G的 SKOLEM标

19、准形：(y)(z)P(c ,y ,z ,f(y ,z) 67三三. . 子句与子句集子句与子句集 定义（子句）： 将文字的析取称为子句。例如： P(x,f(x)R(x ,f(x),g(x)） P(x,y,z)Q(x,z)R(x) 将一个公式化为Skolem范式后，可将其进一步化为子句集形式。68 子句集子句集nSkolem化以后，将公式表示为子句集合。n(x)(y)(P(x)Q(y) (Q(x)S(f(y)nS = P(x)Q(y)，Q(x)S(f(y)n子句（clause）：n例：n（1） P S R （2） P(x) Q(y, z) R(y, y)n空子句(nil，永假)nn文字子句n子句

20、集合：n子句内部的关系是析取；n子句间的关系是和取n所有子句受全程量词约束；69 定理定理n定理n设S是公式G的子句集， G不相容 S不相容nS不相容：对任一个解释，S中至少有一个子句为假。nS相容：存在一个解释，使S中所有子句为真。70n推论n如果G=G1Gn, Si是Gi的子句集， 其中i=1，n； 令S=S1Sn。 G不相容 S不相容71n要证明定理: (A1A2A3A4)Bn证明: (A1A2A3A4B)是永假式; n证明: (A1A2A3A4B)的子句集不相容;n根据推论, 只要分别求出A1, A2, A3, A4, B的子句集;72nA1: (x)(y)(z)P(x,y,z)nSA

21、1: P(x,y,f(x,y)nA2: (x)(y)(z)(u)(v)(w) (P(x,y,u)P(y,z,v)P(u,z,w)P(x,v,w) (P(x,y,u)P(y,z,v)P(x,v,w)P(u,z,w)nSA2: P(x,y,u)P(y,z,v)P(u,z,w)P(z,v,w), P(x,y,u)P(y,z,v)P(x,v,w)P(u,z,w)nA3: (x)(P(x,e,x) P(e,x,x)nSA3: P(x,e,x), P(e,x,x)nA4: (x)(P(x,i(x),e)P(i(x),x,e) nSA4: P(x,i(x),e), P(i(x),x,e)73nB: (x)P

22、(x,x,e)(u)(v)(w)(P(u,v,w)P(v,u,w)nSB: P(x,x,e), P(a,b,c), P(b,a,c)nSA1SA2SA3SA4SB共含有10个子句:nP(x,y,f(x,y), P(x,y,u)P(y,z,v)P(u,z,w)P(z,v,w), P(x,y,u)P(y,z,v)P(x,v,w)P(u,z,w), P(b,a,c)74nSkolem范式nHerbrand域n语义树nHerbrand定理nDavis的工作 4.4 Herbrand 4.4 Herbrand定理定理75动机动机n命题逻辑下验证定理是直观的;n公式G含有n个原子, 有2n个解释;nG1

23、= P (Q R)nG2 = (PQ) P) QPQRG100000010010001111001101111011111PQG200101110111176n一阶逻辑下验证定理是困难的:n个体变量论城D的任意性.nD中元素的任意性.n解释的个数的无限性.n是否能找到一个比较简单的、特殊的论域，使得只要在这个论域上该公式是不可满足的，便能保证该公式在任一论域上也是不可满足的? Herbrand域(简称H域)就具有这样的性质。77 一、一、 HerbrandHerbrand域（域（H H域域）n令H0是子句集S中出现的常量的集合。若S中没有常量出现, 则H0由单个常量a组成(即H0=a). 对于

24、i=1,2, Hi=Hi-1所有形如f(t1,.,tn)的项的集合 其中f(t1,.,tn)是出现于S中的任一函数符号， t1,.,tnHi-1.n规定H为S的Herbrand域. （Herbrand universe of S, 简称H域）. 78例例1 1nS=P(z), P(x)Q(y)nH0=aH1= H0H2= H1.H=a 79例例2 2nS=P(a), P(x)P(f(x)nH0=aH1=af(a) = a, f(a)H2=H1f(a), f(f(a) = a, f(a), f(f(a).H=a, f(a), f(f(a),.80例例3 3nS=P(f(x)，a，g(y)，b)n

25、H0=a，bH1=a，b，f(a)，g(a)，f(b)，g(b)H2=a，b，f(a)，g(a)，f(b)，g(b)， f(f(a)，f(g(a)，f(f(b)，f(g(b)， g(f(a)，g(g(a)，g(f(b)，g(g(b).81 二、基本概念二、基本概念n基础(ground)n没有变量的项称为基础项(ground term).nf(a,b)n没有变量的原子称为基础原子(ground atom).nP(a,f(b)n没有变量的文字称为基础文字(ground literal).nP(a,f(b), P(a,f(b)n没有变量的子句称为基础子句(ground clause).nP(b,f(

26、b) Q(f(f(b)82原子集（原子集（ HerbrandHerbrand 基，基，H H基）基）n令S是一个子句集合, 形如P(t1,.,tn)的基础原子集合, 称为S的原子集或Herbrand基(atom set, or the Herbrand base of S). 记为A. 其中, P(t1,.,tn)是出现在S中的任一谓词符号, 而t1,.,tn是S的H域的任意元素。83例子例子nS=P(z), P(x)Q(y)nH=a nA=P(a), Q(a) nS=P(a), P(x)P(f(x)nH=a, f(a), f(f(a),.nA=P(a), P(f(a), P(f(f(a),.

27、nS=P(f(x), a, g(y), b)nH=a, b, f(a), g(a), f(b), g(b),nA=P(a,a,a,a), P(a,a,a,b), P(a,a,b,b),.84基础实例（基例）基础实例（基例）n定义(基础实例，基例)n当S中的某子句C中所有变量符号均以S的H域的元素代入时，所得的基子句C称作C的一个基础实例(基例, a ground instance of a clause C)。n例 S=P(x), Q(f(y)R(y), Z(f(y)nH=a,f(a),f(f(a),.nP(a), P(f(a)都称作子句C=P(x)的基例。同样, Q(f(a)R(a), Q(

28、f(f(a)R(f(a)都是Q(f(y)R(y)的基例。 nQ(a)R(a)不是Q(f(y)R(y)的基例。n对于任一bD,子句P(b), Q(f(b)R(b)都叫基子句。85注意注意n原子集和基础实例不同：n原子集考虑单个原子，基础实例考虑子句。nQ(f(a)R(a)是基例,但不属于S的原子集。n原子集是将某个谓词中的项改为H域中的元素，而基例是改变量。nH=a,f(a),f(f(a),.nQ(a)不是Q(f(y)的基例, 但是属于S的原子集。nQ(f(a)既是Q(f(y)的基例, 又属于S的原子集。86 三、Herbrand解释（H解释）n起因n由子句集S建立H域、原子集A;n一般论域D上

29、对S的解释I H域上的解释I*;nS在D上为真 S在H上为真;nS在D上不可满足 S在H上不可满足; 87H H解释的表示解释的表示n令A=A1,An ,是S的原子集, 一个H解释可被表示为: I=m1,mn , 其中mj或者是Aj或者是Aj. 如果mj是Aj, 则Aj为真, 否则, Aj为假.88例例1 1nS=P(x)Q(x), R(f(y)nH=a, f(a), f(f(a), .nA=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),.n凡对A中各元素真假值的一个具体设定，都是S的一个H解释。 I1*=P(a),Q(a),R(a),P(f(a),Q(f(a),R(

30、f(a),. I2*=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),. I3*=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),. S|I1*=T, S|I2*=F , S|I3*=F89n对S的任一个解释I均可找到一个H解释I*与其对应.n例子: S=P(x)，Q(y，f(y，a) n设D=1,2,解释I作如下设定a f(1,1) f(1,2) f(2,1) f(2,2)2 -1- 2 -2 - 1P(1) P(2) Q(1,1) Q(1,2) Q(2,1) Q(2,2) T -T -F -T -T- Fn对x=1,y=1: P(1)Q(1,

31、f(1,2)=T 对x=1,y=2: P(1)Q(2,f(2,2)=T 对x=2,y=1: P(2)Q(1,f(1,2)=T 对x=2,y=2: P(2)Q(2,f(2,2)=Tn在解释I下, S为真;90n找I*;nH=a, f(a,a), f(a,f(a,a), f(f(a,a),a), f(f(a,a), f(a,a),.nA=P(a),Q(a,a),P(f(a,a),Q(a,f(a,a),Q(f(a,a) ,a), Q(f(a,a),f(a,a), .na2f(a,a) f(2,2) 1f(a,f(a,a) f(2,1) 2f(f(a,a),a) f(1,2) 2f(f(a,a),f(

32、a,a) f(2,2) 1.P(a) P(2) TQ(a,a) Q(2,2) FP(f(a,a) P(1) TQ(a,f(a,a) Q(2,1) TQ(f(a,a),a) Q(1,2) TQ(f(a,a),f(a,a) Q(1,1) F.nI*=P(a),Q(a,a),P(f(a,a),Q(a,f(a,a),Q(f(a,a),a),Q(f(a,a),f(a,a), .91nS=P(x)，Q(y，f(y，a)nH=a, f(a,a), f(a,f(a,a), f(f(a,a),a), f(f(a,a), f(a,a),.n在I*下的S的真值S|I*=P(a) Q(a,f(a,a)(x=a,y=a

33、对应于x=2,y=2)P(a) Q(f(a,a),f(f(a,a),a)(x=a,y=f(a,a) 对应于x=2,y=1)P(f(a,a) Q(a,f(a,a)(x=f(a,a),y=a 对应于x=1,y=2)P(f(a,a) Q(f(a,a),f(f(a,a),a)(x=f(a,a),y=f(a,a) 对应于x=1,y=1)P(a) Q(f(a,f(a,a),f(f(a,f(a,a),a)(x=a,y=f(a,f(a,a) 对应于x=2,y=2).=T. 92例例2 2nS=P(x)Q(x), R(f(y) n设D=1,2,解释I作如下设定nf(1) f(2) P(1) P(2) Q(1)

34、Q(2) R(1) R(2)-2 -2-T- -F -F- - T -F -T于是有 S|I=T93n由于I对常量符号a没有设定, 这时a设定1或2(D中元素), 便有相应于I的H解释I1*和I2*: nI1*=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),P(f(f(a),Q(f(f(a),R(f(f(a),. nI2*=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),P(f(f(a),Q(f(f(a),R(f(f(a),.n有S|I1*=T，S|I2*=T。94 四、四、H H解释的性质解释的性质n引理n如果在论域D上的一个解释I满足S，则

35、任一个对应于I的H解释I*，也满足S。n定理n子句集S是不可满足的，当且仅当S的所有的H解释使S为假。95n定理定理n子句集S是不可满足的，当且仅当S的所有的H解释使S为假。n证明: n()设S是不可满足的.n则在任一个论域上的任一解释使S为假;nH是一个论域;n()设S的所有的H解释使S为假.n假设子句集S可满足.n在某个论域上的某个解释I使S为真;nI在H域上对应解释I*;n根据引理，I*满足S.96几个性质几个性质n(性质1)一个子句C的基础实例C对解释I为满足的, iff存在一个C的基础文字L, 使得L在I中, 即C I。nC: P(x) Q(f(x)nH: a, f(a), f(f(

36、a)nC:P(a) Q(f(a)nI1: P(a), Q(a), P(f(a), Q(f(a), n(性质2)一个子句C在解释I下为真，iff这个子句C的每个基础实例被I所满足。nI2: P(a), Q(a), P(f(a), Q(f(a), 97n(性质3)一个子句C在解释I下为假，iff至少存在一个C的基础实例C，使得C 不被I所满足。nC: P(x) Q(f(x)nH: a, f(a), f(f(a)nC:P(a) Q(f(a)nI3: P(a), Q(a), P(f(a), Q(f(a), n(性质4)子句集S是不可满足的, iff对每个解释I下，至少有S的某个子句的某个基例不被I所满

37、足。 98 五、语义树五、语义树( (Semantic tree)Semantic tree)nExample 1nG = P Q RnS = P, Q, RnA = P, Q, RPPQQQQRRRRRRRR99nExample 2nS=P(x)Q(x), P(f(y), Q(f(y)nH=a, f(a), f(f(a), .nA=P(a), Q(a), P(f(a), Q(f(a), . P(a)P(a)Q(a)Q(a)Q(a)Q(a)P(f(a) P(f(a)P(f(a) P(f(a)P(f(a) P(f(a). 100注意注意n颠倒原子的顺序是可以的. 例如Q(a)为第一个顶点.n如果

38、原子集是无限的，则对应的语义树必定是无限的.n从任一个叶节点向根节点看, 代表S的一个解释.n从任一个中间节点向根节点看, 代表S的一个部分解释.101n证明一个定理就是寻找一棵封闭语义树.nS不可满足S在所有解释下为假 S在所有H解释下为假;n完备语义树包含所有H解释;每一枝是一个H解释;nS在I下为假, 则使某个基础实例为假;n这个节点称为假节点, 不用再扩展;n所有枝上都有假节点, 则为封闭语义树;102 六、六、HerbrandHerbrand定理定理nHerbrand定理(Version 1)n子句集S是不可满足的，当且仅当对应于S的任一棵完备语义树, 都存在一棵有限的封闭语义树。

39、103证明n设子句集S不可满足.n要证:对应于S的任一棵完备语义树, 都存在一棵有限的封闭语义树。n设T是S的完备语义树.n任选T的一个分支B, I(B)是B上所有连线上的文字的集合的并. I(B)是S的一个解释.nS不可满足, 则I(B)一定使S中的一个子句C为假;nI(B)一定使C的某个基础实例C为假(性质3); nC的每个原子一定都在原子集A中. 因为C的文字数目是有限的, 所以在B上一定存在一个假节点.n因为B的任意性, T的每个分支都有假节点. T是封闭的.104nT是有限的.nT是有限的封闭语义树.n设对应于S的任一棵完备语义树, 都存在一棵有限的封闭语义树.n要证: 子句集S不可

40、满足。n完备语义树包含S的所有解释,每一枝对应一个解释;n封闭语义树: 每一枝都终止在假节点上: 每一枝都使S的某个子句的某个基例为假.n(性质4)子句集S是不可满足的, iff对每个解释I下，至少有S的某个子句的某个基例为假。 105HerbrandHerbrand定理定理2 2nHerbrand定理(Version 2)n子句集S是不可满足的，当且仅当存在一个有限不可满足的S的基础实例集合S。 n例子:nS=P(x), P(a)P(b), Q(f(x)nH=a, b, f(a), f(b), f(f(a), f(f(b)nA=P(a), P(b), Q(a), Q(b),nS=P(a),

41、P(b), P(a)P(b)P(a)P(b)P(a)P(b)106n证明n设子句集S是不可满足的;n要证: 存在一个有限不可满足的S的基础实例集合S.n根据Version 1, 有一棵有限的封闭语义树;n每一枝都终止在假节点上: 每一枝都使S的某个子句的某些基例为假: 构成S.nS不可满足.n有限的封闭语义树: 节点有限:假节点有限: S有限.107n设存在一个有限不可满足的S的基础实例集合S。nS的任一个解释I都是一个对所有基础实例的解释;它包含一个对S的解释I.n因为S不可满足, 所以I使S为假;nII, 所以I使S为假; (I使某个子句的某个基础实例为假)n由于解释I的任意性, S不可满

42、足.108GilmoreGilmore的方法的方法(1960)(1960)n子句集S是有限的;n基础实例的数目是可数的;n枚举;109Davis-PutnamDavis-Putnam的工作的工作nGilmore的方法是指数复杂性的;nDavis-Putnam: 提高效率(启发式方法);n四条规则: n其应用不改变子句集的不相容性;110规则一规则一n重言式规则(tautology rule)nS中的重言式子句，不会为S的不可满足提供任何信息，应该删除。nS=PP，Q，RPS的逻辑含义是（PP）Q(RP)= Q(RP)，从而删去重言式PP，不影响S的真值。nS=Q，RPnDelete all t

43、he ground clauses from S that are tautologies. The remaining set S is unsatisfiable if and only if S is.111规则二规则二n单文字规则(one-literal rule) n单文字: 在S中存在只有一个文字的基础子句L.n例子: S=L，LP，LQ，SR n如果在S中存在只有一个文字的基础子句L, 消去在S中带有这个文字L的所有子句得到S, 如果S为空, 则S是相容的; 否则, 从S中删去L, 得到S. S不可满足当且仅当S不可满足.nS = LQ，SRnS= Q，SRnS不可满足, 则在所

44、有解释下S都为假;nL=0;nL=1;nL=0.112规则三规则三n纯文字规则(pure-literal rule) n纯文字: 如果文字L出现于S中，而L不出现于S中，L称为S的纯文字. n例子: S=AB, AB, B, BnL是S的纯文字. 从S中删除含L的子句得S，如果S为空集，那么S是可满足的。否则, S不可满足当且仅当S不可满足.nS= B, B;nS不可满足, 在A为真下不可满足;nA=1: AB=1, AB=1;nS不可满足, 当然S不可满足;113规则四规则四n分裂规则(splitting rule)nS=(L A1). (L Am) (LB1). (LBn)RAi, Bi, R中不含L和L。令S =A1.AmR， S=B1.BnR则S不可满足当且仅当S和S同时是不可满足的。nL=1(S)nL=0(S)114例例1 1nS=PQR, PQ, P, R, Un对U使用纯文字: PQR, PQ, P, Rn对P使用单文字: QR, Q, Rn对Q使用单文字: R, Rn对R使用单文字: nS不可满足;115例例2 2nS=PQ, Q, PQRn对Q使用单文字: P, PRn对P使用单文字: Rn对R使用纯文字: nS可满足;116