《归结原理不讲》PPT课件.ppt

1,人工智能原理 第 四 讲 归结原理,周日贵 华东交通大学信息工程学院,2,归结原理,4.1 引言 4.2 一阶逻辑 4.3 子句形 4.4 Herbrand定理 4.5 置换与合一 4.6 归结原理 4.7 归结法的完备性 4.8 归结策略,3,4.1 引言,自动定理证明 历史 四色定理 三类方法,4,自动定理证明,Automated Theorem Proving(ATP) 定理机器证明(Mechanical Theorem Proving) 为什么？ 定理证明是一种智能行为； 体现了人类的逻辑推理能力； 推理用计算来实现 Leibniz的梦想： Leibniz 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.,5,1930年，Herbrand定理。 半可判定问题。 一阶逻辑的判定问题。 在一阶逻辑中，有没有方法可以判断任何一个命题是否定理？(有没有方法可以判断任何一个公式能不能从公理及推理规则推导出来)。 数理逻辑的基本问题。 1936年，证明基本问题是不可解的。 在一阶逻辑中，如果一个定理是正确的，则有一个机械的方法在有限步内证明它。 一阶谓词逻辑有很强的表达能力，凡可计算的函数就可由一阶谓词表达。,6,历史,Newell，Shaw，Simon 1956年，The logic theory machine(逻辑理论机). 数学定理证明程序(Logic Theorist) mimic human reasoning 数学原理第二章中的38个定理 1963年，经过改进的LT程序在一部更大的电脑上，最终完成了第二章全部52条数学定理的证明。,7,王浩 1958年，IBM704电脑，3-5分钟，证明了数学原理中有关命题演算的全部220条定理。 1959年，8.4分钟，证明了数学原理中全部（350条以上）定理。 罗素：“我真希望，在怀特海和我浪费了10年的时间用手算来证明这些定理之前，就知道有这种可能。” 1983年获得首届自动定理证明里程碑奖。,8,四色定理,1852年，一位21岁的大学生提出来的数学难题：任何地图都可以用最多四种颜色着色，就能区分任何两相邻的国家或区域。,9,四色定理,1976年7月，美国的阿佩尔(K.Appel)等人合作解决了长达124年之久的难题-四色定理。他们用三台大型计算机，花去1200小时CPU时间，并对中间结果进行人为反复修改500多处。四色定理的成功证明曾轰动计算机界。 伊利诺斯数学杂志第21卷刊载的检验表(460p),10,三类方法,基于归结的方法 类人的方法(human simulation) 判定方法,11,基于归结的方法,1960年，Gilmore在计算机上实现了Herbrand算法。 1960年，M.Davis和H.Putnam的改进： Tautology Rule, One-literal Rule, Pure-literal Rule, Splitting Rule。 技巧而非本质：枚举基替换。 1960年，D.Prawitz 直接寻找替换，避免组合爆炸。 思想深刻，效果不理想。 1965年，J.A.Robinson提出归结原理 One-literal Rule的扩展。,12,效率的提高 1965： Wos, G.A.Robinson, Curson, 支持集归结； 1967：Slagle，语义归结； 1970：Loveland，Luckham，线性归结； 1971：Boyer，锁归结； 1978：刘叙华，锁语义归结； 1979：王湘浩，刘叙华，广义归结；,13,类人的方法(human simulation),1956年，Newell，Shaw，Simon The logic theory machine(逻辑理论机) 1966年，MIT的L.M.Norton建造了ADEPT系统 群论的定理证明系统； 启发式； 1972年，R.Boyer和J.Moore 启发式策略和人机交互； 质因子分解唯一定理，验证编译程序的正确性； 1977年，Bledsoe： Non-Resolution Theorem Proving(非归结定理证明),14,判定方法,在较小的范围内找到一个有效的判定方法； 早期工作： A.Tarski的初等代数和初等几何的方法。 王浩：命题逻辑的一个有效的判定方法。 吴文俊：吴方法(1977)。,15,吴方法,平面几何定理 几何问题-代数问题 1959年，Gelernter提出几何定理证明机(Geometry Theorem Proving Machine, GTM) 反向推理； 直线图形中大部分高中考试的问题； 运行时间与高中学生做题时间差不多； 获国际Herbrand自动推理杰出成就奖 “吴的工作将几何定理证明从一个不太成功的领域变为最成功的领域之一。在很少的领域中，我们可以将定理机器证明归于一个人的工作。几何定理证明就是这样的一个领域 ” (中国),16,4.2 一阶逻辑,基本概念 合适公式 公式的解释 前束范式 合取范式与析取范式 逻辑结论,17,一. 基本概念,定义(谓词)： 设D是非空个体名称集合，定义在Dn上，取值于T，F上的n元函数，称为n元谓词。 Dn表示集合D上的n次笛卡儿乘积。 例子： Man(x) Greater(x，y),18,1. 函数,函数(函词) 是一个映射： f: D D D D 例子： father(x）,19,2. 符号,常数：3，20.5，John，Confucius 变量：x，y，z 函数：g，f，h，father，plus 谓词：Q，P，GREATER,20,3. 项,定义(项)： 常数是项； 变量是项； 如果f是一个n元函数符号，且t1，t2，. ，tn是项，则f(t1，t2，. ，tn)也是项； 所有项均是应用上述规则产生； 谓词不能是项。,21,二. 合适公式(wff, well-formed formula),： 全称量词 x： 所有x，每个x； ：存在量词 x：存在一个x；,22,1. 举例,每个有理数是实数。 存在一个数，它是素数。 对每个数x，存在一个数y，使得xy。 令： Q(x)：x是有理数； P(x)：x是素数； R(x)：x是实数； LESS(x, y)；xy； (x)(Q(x) R(x) (x)P(x) (x)(y)LESS(x, y),23,2. 约束变量与自由变量,变量的出现是约束的，当且仅当变量出现在使用它的量词范围之内；变量的出现是自由的， 当且仅当它的出现不是约束的。 (x)(P(x, y) Q(x, z) R(x) 变量是约束的，如果至少一次它的出现是约束的；变量是自由的，如果至少一次它的出现是自由的。 一个变量可以既是约束变量又是自由变量。 (x)(P(x, y) Q(x, z) R(x),24,3. 变量改名,(x)G(x) = (y)G(y) (x)G(x) = (y)G(y) (x)(P(x, y) Q(x) (z)(P(z, y) Q(x) (x)P(x, y) (y)P(y, y) (x)(P(x, y) Q(x, z) R(x) (x)(P(x, y) Q(x, z) R(u),25,定义(原子)： 如果P是n元谓词，t1，t2，. ，tn是项，则 P（t1，t2，. ，tn）是一个原子。,4. 原子,26,5. 合适公式（Wff),定义(合适公式) 原子是公式； 如果G，H是公式，则G，(GH)，(GH)，(GH)，(GH)是公式； 如果G是公式，且x是G中的自由变量，则(x)G和(x)G是公式； 所有公式均是由上述规则产生。,27,6. 五个联结符,（读做“非”）(名称：否定符号) （与，并且）(合取符号) （或，或者）(析取符号) （蕴涵，隐含）(蕴涵符号) （充要，等价）(等值符号),28,7. 举例,每个人都是要死的。 (x)(MAN(x)MORTAL(x) 孔子是人。 MAN(Confucius) 孔子是要死的。 MORTAL(Confucius) 对每个数，存在一个且仅仅一个直接后继； (x)(y)(E(f(x), y) (z)(E(z, f(x)E(y, z) 没有一个数，它的直接后继是0； (x)E(f(x), 0) (令f(x)表示x的直接后继；E(x, y)： x=y),29,三. 一阶谓词逻辑的公式解释,定义(公式的解释) 公式的解释是由一个非空域D，以及下列对公式G中的常量、变量、函数及谓词符号的指派组成，并且它的指派遵守下述规则： 对每个常量，均是D中的一个元素； 对每个变量，指派一个D中的元素作为它的值； 对每个n元函数符号，指派一个从Dn到D的映射； 对每个n元谓词符号，指派一个从Dn到T，F的映射。,30,1. 对D域内计算公式的规则,如果公式G，H的真值已被计算, 则 H，(GH)，(GH)，(GH)，(GH) 的真值可按命题的计算定义来求出。,31,2. 真值表,32,3. 联结符的一些重要性质, A=A （A B）= A B （A B）= A B A B = AB A B = （A B） （B A） （(x)A(x)）= (x)（ A(x)） （(x)A(x)）= (x)（ A(x)）,33,例1,G=(x)(P(x) Q(f(x),a) 一个解释I： 域：D=1，2 对常数指派：a:1 对函数指派：f(1)=2, f(2)=1 对谓词指派：P(1)=F，P(2)=T，Q(1,1)=T， Q(1,2)=T，Q(2,1)=F，Q(2,2)=T G？,34,x=1： P(x) Q(f(x),a) =P(1) Q(f(1), 1) =P(1) Q(2, 1) =F F =T x=2： P(x) Q(f(x),a) =P(2) Q(f(2), 1) =P(2) Q(1, 1) =T T =T 公式G在解释I下为真；,35,例2,(a) G=(x)(P(f(x) Q(x, f(a) (b) G=(x)(P(x) Q(x, a) (c) G=(x)(y)(P(x) Q(x, y) 一个解释I： 域：D=1, 2 对常数指派：a=1 对函数指派：f(1)=2，f(2)=1 对谓词指派：P(1)=F，P(2)=T，Q(1,1)=T，Q(1,2)=T， Q(2,1)=F，Q(2,2)=T G？,36,(a) G=(x)(P(f(x) Q(x, f(a) x=1 P(f(1) Q(1, f(1) =P(2) Q(1, 2) =T T =T G在解释I下为真。,37,(b) G=(x)(P(x) Q(x, a) x=1 P(1) Q(1, 1) =F T =F x=2 P(2) Q(2, 1) =T F =F G在解释I下为假。,38,(c) G=(x)(y)(P(x) Q(x, y) x=1，y=1 P(x) Q(x, y) = P(1) Q(1, 1) = F T = F x=1，y=2 P(x) Q(x, y) = P(1) Q(1, 2) = F T = F G在解释I下为假。,39,4. 一些定义,一个公式G是相容的(满足的)，当且仅当存在一个解释I，使公式G在解释I下为真，称I是G的一个模型且I满足G。 一个公式G是不相容的(不满足)，当且仅当不存在解释满足G。 一个公式G是永真的，当且仅当每一个论域的每一个解释都满足G。 一个公式G是公式F1，F2， ，Fn的逻辑结论， 当且仅当对任一个解释I，如果F1，F2， ，Fn在I下为真，则G在I下也为真。,40,例1,证明H=(x)(P(x) (y)(P(y)不相容。,证明： 如果任一个aD使得P(a)=T 则P(a)=F，(y)(P(y)为假。 如果存在一个aD使得P(a)=F 则(x)(P(x)为假。 所以H不相容。,41,例2,证明Q(a)是F1，F2的逻辑结论。 F1= (x)(P(x) Q(x) F2= P(a),证明： 假设F1，F2为真，Q(a)为假； 则P(a)Q(a)为假； P(a)Q(a)为假； (x)(P(x) Q(x)为假。,42,四. 前束范式,定义(前束范式，prenex normal form)： 一个公式H称为前束范式，当且仅当公式H有如下形式： (Q1x1)(Qnxn)(M) 其中Qi或是或是，i=1，n；M是不含量词的公式。 其中(Q1x1)(Qnxn)称为前缀，M称为母式。 (x)(y)(P(x, y)，(x)(y)(P(x, y)Q(y)均是 (x)(P(x, y)(y)(Q(y)不是,43,1. 公式的等价,等价公式 H=G: H和G的值对所有域的所有解释都相同; 设H(x)是仅含有自由变量x的公式，G是不含变量x的公式。 (x)H(x) G = (x)(H(x) G) (x)H(x) G = (x)(H(x) G) (x)H(x) G = (x)(H(x) G) (x)H(x) G = (x)(H(x) G),44,(x)H(x) = (x)(H(x) (x)H(x) = (x)(H(x) 设H(x)，G(x)是仅含有自由变量x的公式： (x)G(x) (x)H(x) = (x)(G(x) H(x) (x)G(x) (x)H(x) = (x)(G(x) H(x) (x)G(x) (x)H(x) = (x)(y)(G(x) H(y) (x)G(x) (x)H(x) = (x)(y)(G(x) H(y),45,证明： 设(x)H(x)=T (x)H(x)=F 存在eD，H(e)=F， H(e)=T 设(x)H(x)=F (x)H(x)=T 对任一个eD，H(e)=T， H(e)=F,证明(x)H(x) = (x)(H(x).,46,证明： 设(x)G(x) (x)H(x)=T (x)G(x)=T，(x)H(x)=T 对任一个eD，G(x)=T并且H(x)=T 对任一个eD，G(x)=T H(x)=T 设(x)G(x) (x)H(x)=F 对任一解释，(x)G(x)=F或者(x)H(x)=F 设(x)G(x)=F 存在eD，G(e)=F G(e) H(e)=F,证明(x)G(x) (x)H(x) = (x)(G(x) H(x),47,注意：,(x)G(x) (x)H(x) (x)(G(x) H(x) (x)G(x) (x)H(x) (x)(G(x) H(x),48,证明(x)G(x) (x)H(x) (x)(G(x) H(x) (x)G(x) (x)H(x) = T, 则(x)(G(x) H(x)=T 设(x)G(x) (x)H(x)=F (x)G(x)=F 且 (x)H(x)=F 存在aD，使G(a)=F。存在bD，使H(b)=F.。 反例： 对任意eD，ea，G(e)=T。 对任意eD，eb，H(e)=T。 ab 对任意eD，G(e) H(e)=T。 (x)(G(x) H(x)=T。,49,2. 化公式为前束范式步骤,消去和 FG = (FG) (GF) FG = F G 将代入每个原子前面 (F) = F (FG) = FG (FG) = FG (x)H(x) = (x)(H(x) (x)H(x) = (x)(H(x),50,如果必要的话，将约束变量改名。 (x)G(x) (x)H(x) = (x)(y)(G(x) H(y) 利用等价公式将量词移到公式的最左边。,51,例1,化(x)P(x) (x)Q(x)为前束范式。,(x)P(x) (x)Q(x)= (x)P(x) (x)Q(x),= (x)P(x) (x)Q(x),= (x)(P(x) Q(x),52,例2,化下式为前束范式。 (x)(y)(z)(P(x,z) P(y,z) (u)Q(x,y,u),=(x)(y)(z)(P(x,z) P(y,z) (u)Q(x,y,u),=(x)(y)(z)(P(x,z)P(y,z) (u)Q(x,y,u),=(x)(y)(z)(u)(P(x,z) P(y,z) Q(x,y,u),53,五. 合取范式与析取范式,定义(等价)： 两个公式等价(F=G)，当且仅当对任一个解释，F和G的值都相同。 定义(文字)： 文字是一个原子或一个原子的非； 定义(合取范式)： 公式G是合取范式，当且仅当G有 G1G2 Gn，n1 的形式，其中Gi文字的析取式。 例子: (AB)(CD)(FG) 析取范式,54,1. 变换公式,FG = (FG) (GF) FG = F G FG = GF, FG = GF (交换律) (FG)H = F(GH) (结合律) (FG)H = F(GH) F(GH) = (FG)(FH) (分配律) F(GH) = (FG)(FH),55,(F) = F (否定之否定) (FG) = FG (狄摩根定律) (FG) = FG F G = G； F G = F T G = T ； T G = G,56,2. 化公式为合取范式(析取范式),消去和 FG = (FG) (GF) FG = F G 将代入每个原子前面 (F) = F (FG) = FG (FG) = FG 使用: F(GH) = (FG)(FH) F(GH) = (FG)(FH),57,例子:,(P(QG)S =(P(QG)S =(P(QG)S =P(QG)S =(PS)(QG) =(PSQ)(PSG),58,六. 逻辑结论,定义(逻辑结论) 给定公式F1，F2， ，Fn和G，G是公式F1， F2， ，Fn的逻辑结论，当且仅当使F1，F2， Fn为真的任一个解释，使G为真。公式F1，F2， ，Fn称为G的公理。,59,定理1,定理1 给定公式F1，F2， ，Fn和G，G是公式F1， F2， ，Fn的逻辑结论，当且仅当公式 (F1F2Fn)G 为永真式。,证明： (F1F2Fn)G = (F1F2Fn)G = F1F2FnG,60,(F1F2Fn)G = F1F2FnG 设G是公式F1，F2， ，Fn的逻辑结论 要证：(F1F2FnG)是永真式 F1，F2，Fn均为真 F1，F2，Fn中至少有一个为假 设公式(F1F2Fn)G为永真式 要证：G是公式F1，F2， ，Fn的逻辑结论 要证：当F1，F2，Fn为真，G为真 (F1F2FnG)是永真式,61,定理2,定理2 给定公式F1，F2，Fn和G，G是公式F1，F2， ，Fn的逻辑结论，当且仅当公式 F1F2FnG 不相容 (是永假式),证明： (定理1)给定公式F1, F2, Fn和G, G是公式F1, F2, Fn的逻辑结论, 当且仅当公式 (F1F2Fn)G 为永真式 (F1F2Fn)G)为永假式 F1F2FnG,62,定理的定义,定义(定理) 如果G是公式F1，F2，Fn的逻辑结论，则公式 (F1F2Fn)G 称为定理， G称为定理的结论。,63,4.3 子句形,设有由一阶谓词逻辑描述的公式A1,A2,A3和B，证明在A1A2A3成立的条件下有B成立。采用反演法来证明： A1A2A3B 是不可满足的。和命题逻辑不同，首先遇到了量词问题，为此要将A1A2A3B化成SKOLEM标准形，进而建立子句集，方可使用 Herbrand 定理和归结原理来证明A1A2A3B成立。,64,一. SKOLEM 标准形,对给定的一阶谓词逻辑公式： G A1A2A3B 首先化成与其等值的前束范式： (Q1x1)(Q1xn)M(x1, xn) 其中Qi(i=1,n)是存在量词或全称量词，而母式M(x1, xn)中不再含有量词。 进而可将M(x1, xn)化成等值的合取范式。 最后将所有存在量词消去，便得公式G的SKOLEM标准形了。,65,二. 化SKOLEM 标准形的方法,消存在量词的过程如下： 设(Qixi) 1in是第一个出现于(Q1x1) (Qixi) (Qnxn) M(x1,xn) 中的存在量词，即Qi, Qi-1均为全称量词。 * 若i1，则将M(x1,xn)中的所有变量x1均以某个常量C代之，但要求C不同于已出 现在M(x1,xn)中的任一常量。然后便可消去这个存在量词(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 标准形。,66,例1,G(x)(y)(z)(P(x,y)Q(x ,z)R(x,y,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(x,f(x),g(x) 便是G的 SKOLEM 标准形，其中f(x),g(x)称作 SKOLEM 函数。,67,例2,化公式G(x)(y)(z)(u)(P(x ,y ,z ,u)为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标准形： (y)(z)P(c ,y ,z ,f(y ,z),68,三. 子句与子句集,定义（子句）： 将文字的析取称为子句。 例如： P(x,f(x)R(x ,f(x),g(x)） P(x,y,z)Q(x,z)R(x) 将一个公式化为Skolem范式后，可将其进一 步化为子句集形式。,69,子句集,Skolem化以后，将公式表示为子句集合。 (x)(y)(P(x)Q(y) (Q(x)S(f(y) S = P(x)Q(y)，Q(x)S(f(y) 子句（clause）： 例： （1） P S R （2） P(x) Q(y, z) R(y, y) 空子句(nil，永假) n文字子句 子句集合： 子句内部的关系是析取； 子句间的关系是和取 所有子句受全程量词约束；,70,定理,定理 设S是公式G的子句集， G不相容 S不相容 S不相容：对任一个解释，S中至少有一个子句为假。 S相容：存在一个解释，使S中所有子句为真。,71,推论 如果G=G1Gn, Si是Gi的子句集， 其中i=1，n； 令S=S1Sn。 G不相容 S不相容,72,要证明定理: (A1A2A3A4)B 证明: (A1A2A3A4B)是永假式; 证明: (A1A2A3A4B)的子句集不相容; 根据推论, 只要分别求出A1, A2, A3, A4, B的子句集;,73,A1: (x)(y)(z)P(x,y,z) SA1: P(x,y,f(x,y) A2: (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) SA2: 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) A3: (x)(P(x,e,x) P(e,x,x) SA3: P(x,e,x), P(e,x,x) A4: (x)(P(x,i(x),e)P(i(x),x,e) SA4: P(x,i(x),e), P(i(x),x,e),74,B: (x)P(x,x,e)(u)(v)(w)(P(u,v,w)P(v,u,w) SB: P(x,x,e), P(a,b,c), P(b,a,c) SA1SA2SA3SA4SB共含有10个子句: P(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),75,Skolem范式 Herbrand域 语义树 Herbrand定理 Davis的工作,4.4 Herbrand定理,76,动机,命题逻辑下验证定理是直观的; 公式G含有n个原子, 有2n个解释; G1 = P (Q R) G2 = (PQ) P) Q,77,一阶逻辑下验证定理是困难的: 个体变量论城D的任意性. D中元素的任意性. 解释的个数的无限性. 是否能找到一个比较简单的、特殊的论域，使得只要在这个论域上该公式是不可满足的，便能保证该公式在任一论域上也是不可满足的? Herbrand域(简称H域)就具有这样的性质。,78,一、 Herbrand域（H域）,令H0是子句集S中出现的常量的集合。若S中没有常量出现, 则H0由单个常量a组成(即H0=a). 对于i=1,2, Hi=Hi-1所有形如f(t1,.,tn)的项的集合 其中f(t1,.,tn)是出现于S中的任一函数符号， t1,.,tnHi-1. 规定H为S的Herbrand域. （Herbrand universe of S, 简称H域）.,79,例1,S=P(z), P(x)Q(y) H0=a H1= H0 H2= H1 . H=a,80,例2,S=P(a), P(x)P(f(x) H0=a H1=af(a) = a, f(a) H2=H1f(a), f(f(a) = a, f(a), f(f(a) . H=a, f(a), f(f(a),.,81,例3,S=P(f(x)，a，g(y)，b) H0=a，b H1=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) .,82,二、基本概念,基础(ground) 没有变量的项称为基础项(ground term). f(a,b) 没有变量的原子称为基础原子(ground atom). P(a,f(b) 没有变量的文字称为基础文字(ground literal). P(a,f(b), P(a,f(b) 没有变量的子句称为基础子句(ground clause). P(b,f(b) Q(f(f(b),83,原子集（ Herbrand 基，H基）,令S是一个子句集合, 形如P(t1,.,tn)的基础原子集合, 称为S的原子集或Herbrand基(atom set, or the Herbrand base of S). 记为A. 其中, P(t1,.,tn)是出现在S中的任一谓词符号, 而t1,.,tn是S的H域的任意元素。,84,例子,S=P(z), P(x)Q(y) H=a A=P(a), Q(a) S=P(a), P(x)P(f(x) H=a, f(a), f(f(a),. A=P(a), P(f(a), P(f(f(a),. S=P(f(x), a, g(y), b) H=a, b, f(a), g(a), f(b), g(b), A=P(a,a,a,a), P(a,a,a,b), P(a,a,b,b),.,85,基础实例（基例）,定义(基础实例，基例) 当S中的某子句C中所有变量符号均以S的H域的元素代入时，所得的基子句C称作C的一个基础实例(基例, a ground instance of a clause C)。 例 S=P(x), Q(f(y)R(y), Z(f(y) H=a,f(a),f(f(a),. P(a), P(f(a)都称作子句C=P(x)的基例。同样, Q(f(a)R(a), Q(f(f(a)R(f(a)都是Q(f(y)R(y)的基例。 Q(a)R(a)不是Q(f(y)R(y)的基例。 对于任一bD,子句P(b), Q(f(b)R(b)都叫基子句。,86,注意,原子集和基础实例不同： 原子集考虑单个原子，基础实例考虑子句。 Q(f(a)R(a)是基例,但不属于S的原子集。 原子集是将某个谓词中的项改为H域中的元素，而基例是改变量。 H=a,f(a),f(f(a),. Q(a)不是Q(f(y)的基例, 但是属于S的原子集。 Q(f(a)既是Q(f(y)的基例, 又属于S的原子集。,87,三、Herbrand解释（H解释）,起因 由子句集S建立H域、原子集A; 一般论域D上对S的解释I H域上的解释I*; S在D上为真 S在H上为真; S在D上不可满足 S在H上不可满足;,88,H解释的表示,令A=A1,An ,是S的原子集, 一个H解释可被表示为: I=m1,mn , 其中mj或者是Aj或者是Aj. 如果mj是Aj, 则Aj为真, 否则, Aj为假.,89,例1,S=P(x)Q(x), R(f(y) H=a, f(a), f(f(a), . A=P(a),Q(a),R(a),P(f(a),Q(f(a),R(f(a),. 凡对A中各元素真假值的一个具体设定，都是S的一个H解释。 I1*=P(a),Q(a),R(a),P(f(a),Q(f(a),R(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*=F,90,对S的任一个解释I均可找到一个H解释I*与其对应. 例子: S=P(x)，Q(y，f(y，a) 设D=1,2,解释I作如下设定 a f(1,1) f(1,2) f(2,1) f(2,2) 2 -1- 2 -2 - 1 P(1) P(2) Q(1,1) Q(1,2) Q(2,1) Q(2,2) T -T -F -T -T- F 对x=1,y=1: P(1)Q(1,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)=T 在解释I下, S为真;,91,找I*; H=a, f(a,a), f(a,f(a,a), f(f(a,a),a), f(f(a,a), f(a,a),. A=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), . a2 f(a,a) f(2,2) 1 f(a,f(a,a) f(2,1) 2 f(f(a,a),a) f(1,2) 2 f(f(a,a),f(a,a) f(2,2) 1 . P(a) P(2) T Q(a,a) Q(2,2) F P(f(a,a) P(1) T Q(a,f(a,a) Q(2,1) T Q(f(a,a),a) Q(1,2) T Q(f(a,a),f(a,a) Q(1,1) F . I*=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), .,92,S=P(x)，Q(y，f(y，a) H=a, f(a,a), f(a,f(a,a), f(f(a,a),a), f(f(a,a), f(a,a),. 在I*下的S的真值 S|I*=P(a) Q(a,f(a,a) (x=a,y=a对应于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.,93,例2,S=P(x)Q(x), R(f(y) 设D=1,2,解释I作如下设定 f(1) f(2) P(1) P(2) Q(1) Q(2) R(1) R(2) -2 -2-T- -F -F- - T -F -T 于是有 S|I=T,94,由于I对常量符号a没有设定, 这时a设定1或2(D中元素), 便有相应于I的H解释I1*和I2*: I1*=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),. I2*=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),. 有S|I1*=T，S|I2*=T。,95,四、H解释的性质,引理 如果在论域D上的一个解释I满足S，则任一个对应于I的H解释I*，也满足S。 定理 子句集S是不可满足的，当且仅当S的所有的H解释使S为假。,96,定理 子句集S是不可满足的，当且仅当S的所有的H解释使S为假。 证明: ()设S是不可满足的. 则在任一个论域上的任一解释使S为假; H是一个论域; ()设S的所有的H解释使S为假. 假设子句集S可满足. 在某个论域上的某个解释I使S为真; I在H域上对应解释I*; 根据引理，I*满足S.,97,几个性质,(性质1)一个子句C的基础实例C对解释I为满足的, iff存在一个C的基础文字L, 使得L在I中, 即C I。 C: P(x) Q(f(x) H: a, f(a), f(f(a) C:P(a) Q(f(a) I1: P(a), Q(a), P(f(a), Q(f(a), (性质2)一个子句C在解释I下为真，iff这个子句C的每个基础实例被I所满足。 I2: P(a), Q(a), P(f(a), Q(f(a), ,98,(性质3)一个子句C在解释I下为假，iff至少存在一个C的基础实例C，使得C 不被I所满足。 C: P(x) Q(f(x) H: a, f(a), f(f(a) C:P(a) Q(f(a) I3: P(a), Q(a), P(f(a), Q(f(a), (性质4)子句集S是不可满足的, iff对每个解释I下，至少有S的某个子句的某个基例不被I所满足。,99,五、语义树(Semantic tree),Example 1 G = P Q R S = P, Q, R A = P, Q, R,100,Example 2 S=P(x)Q(x), P(f(y), Q(f(y) H=a, f(a), f(f(a), . A=P(a), Q(a), P(f(a), Q(f(a), .,101,注意,颠倒原子的顺序是可以的. 例如Q(a)为第一个顶点. 如果原子集是无限的，则对应的语义树必定是无限的. 从任一个叶节点向根节点看, 代表S的一个解释. 从任一个中间节点向根节点看, 代表S的一个部分解释.,102,证明一个定理就是寻找一棵封闭语义树. S不可满足S在所有解释下为假 S在所有H解释下为假; 完备语义树包含所有H解释;每一枝是一个H解释; S在I下为假, 则使某个基础实例为假; 这个节点称为假节点, 不用再扩展; 所有枝上都有假节点, 则为封闭语义树;,103,六、Herbrand定理,Herbrand定理(Version 1) 子句集S是不可满足的，当且仅当对应于S的任一棵完备语义树, 都存在一棵有限的封闭语义树。,104,证明,设子句集S不可满足. 要证:对应于S的任一棵完备语义树, 都存在一棵有限的封闭语义树。 设T是S的完备语义树. 任选T的一个分支B, I(B)是B上所有连线上的文字的集合的并. I(B)是S的一个解释. S不可满足, 则I(B)一定使S中的一个子句C为假; I(B)一定使C的某个基础实例C为假(性质3); C的每个原子一定都在原子集A中. 因为C的文字数目是有限的, 所以在B上一定存在一个假节点. 因为B的任意性, T的每个分支都有假节点. T是封闭的.,105,T是有限的. T是有限的封闭语义树. 设对应于S