下载文档原格式
例3.1(永真性判断)给定一阶语言 , 其中 是两个常元,是 元谓词符号, 是不同的变元. 假设 是以下公式:考察公式 :即它的前束范式是:它的 Skolem 范式 是:根据以下语义推出关系:可知:若将 看成是命题变元 , 对于子句集合它具有一个反驳, 这表明它能够语义推出一个恒假式, 所以, 能够语义推出一个恒假式, 因而 是永假的.所以 是永假的.所以 是永真的.□定义3.1(文字,相反文字,子句,子句集合,空子句,基文字,基子句,子句代换,子句集合代换 )对于谓词逻辑, 可以定义类似于命题逻辑的一些概念:z原子公式或者原子公式的非称为文字.谓词逻辑归结法,,,,.L={c1,c2,P,Q}c1,c2P,Q1x,y,zA(^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x))\A\((^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x))),(^xP(x)Z^xQ(x))[]x(\P(x)[\Q(x)).^x^y]z((P(x)Z Q(y))[\P(z)[\Q(z)).C]z((P(c1)Z Q(c2))[\P(z)[\Q(z)).C(P(c1)Z Q(c2))[\P(c1)[\Q(c1)C(P(c1)Z Q(c2))[\P(c2)[\Q(c2)C X P(c1)Z Q(c2)C X\P(c1)C X\Q(c2)P(c1),Q(c2)p,q{p Z q,\p,\q},CC\AA X Xz 若 是原子公式,则 是 的 相反文字,是 的相反文字. z 文字的有限集合称为子句.z 不出现变元的文字称为基文字. z 不出现变元的子句称为基子句. z 空的子句称为空子句.z 子句的有限集合称为子句集合.z称 为一个代换. 若 是文字, 则 表示z若子句 是 , 则 表示□事实3.1(子句集合与 Skolem 范式)子句 也写为 表示的闭包. 子句集合表示以下合取范式的闭包:因而表示一个 Skolem 范式.□例3.2(基本概念)z 与 是相反文字, 但是 与 不是相反文字.z假设代换 , 则 等于 .z基子句 表示 .z子句 表示语句L \L L L \L 5:{x 1/t 1,l ,x m /t m }L 5(L)L x 1,l ,xm t 1,l ,t m.C {L 1,l ,L n }5(C){5(L 1),l ,5(L n )}.{L 1,l ,L n }L 1ZlZ L n L 1ZlZ L n {{L 1,1,l ,L 1,n 1},{L 2,1,l ,L 2,n 2},l ,{L m,1,l ,L m,n m}}(L 1,1ZlZ L 1,n 1)[(L 2,1ZlZ L 2,n 2)[l[(L m,1ZlZ L m,nm).P(c 1)\P(c 1)P(c 1)\P(z)5={z/c 1}5(\P(z))\P(c 1){P(c)}P(c){P(x),Q(y)}]x ]y(P(x)Z Q(y)).z子句集合 表示 Skolem 范式□定义3.2(可满足)给定一阶语言 , 假设 是子句,是字句集合. z的一个解释 满足 , 是指 满足 所表示的语句.记为z若以下条件成立:则称 是 和 的逻辑推论. 记为 .z若存在 的解释满足 , 则称 是可满足的; 否则称 是不可满足的.z解释 满足 是指 满足 所表示的 Skolem 范式.z若存在 的解释满足 , 则称 是可满足的; 否则称 是不可满足的.□例3.3(可满足)给定一阶语言 , 假设 是 元谓词符号,是常元, 是变元. z子句 是可满足的.z□定义3.3(归结子句)给定一阶语言 , 假设 是 的两个子句. 形如的子句称为 与 的归结子句. 其中 是两个代换,而 与 是两个相反的文字.若三个子句 具有上述关系, 则记为 .□例3.4(归结子句)对任意的赋值 , 当 及 时, 有 . {P(x)Z Q(y),P(c)Z\Q(z)}]x ]y ]z ((P(x)Z Q(y))[(P(c)Z\Q(z))).L C,C 1,C 2,C 3S L I C I C I X C I I X C 1I X C 2I X C 3C 3C 1C 2C 1,C 2X C 3L C C C I S I S L S S S L P,Q 1c x,y P(c)Z Q(x)P(c)Z Q(x),\Q(y)P(c).L C 1,C 2L (51(C 1)-{L 1})P (52(C 2)-{L 2})C 1C 251,52L 1J 51(C 1),L 2J 52(C 2),L 1L 2C 1,C 2,C 3C 1,C 2U res C 3X给定一阶语言 , 其中 是常元,是变元, 是 元函数符号, 是 元谓词符号. 有以下归结推出关系:z .z .z .z .z. z假设{ 是 . {是 . 则:□定义3.4(反驳)子句集合 的一个反驳是指子句的有限序列 , 它满足以下条件:z 是 .z对于每个 :{或者 ,{或者存在 使得 . □例3.5(反驳)给定一阶语言 , 其中 是常元,是变元, 是 元谓词符号. 子句集合有一个反驳 , 其中:L ={c,f,g,P,Q}c x,y f,g 11P(c),\P(x)U res P(c)Z Q(x),\Q(y)U res P(c)P(x)Z Q(x),\Q(y)U res P(x)P(x)Z Q(x),\Q(y)U res P(f (x))P(x)Z Q(x),\Q(y)res P(f 2(x))A P(x)Z P(f(y))Z R(g(y))B \P(y)Z\R(y)A,B res P(f(y))Z R(g(y))Z\R(y),A,B res R(g(y))Z\R(f(y)).S {C i |15i 5n}C n `i C i J S j,k<i (15j,k< n )C j ,C k U res C i L ={c 1,c 2,P,Q}c 1,c 2x P,Q 1{P(c 1)Z Q(c 2),\P(x),\Q(x)}{C 1,C 2,C 3,C 4,C 5}C 1:P(c 1)Z Q(c 2)C 2:\P(x)C 3:\Q(x)C 4:Q(c 2)C 1,C 2U res C 4C 5:`C 3,C 4U res C 5`U U U□定理3.1(归结推出与语义推出)给定一阶语言 , 假设 是 的两个子句.证明:从 可知存在代换 及两个相反的文字 与 , 使得 , , 而假设子句 分别表示公式 . 则可知 . 因为 , 所以即:□定理3.2(归结方法的可靠性)给定一阶语言 , 假设 是 的子句集合. 若 有一个反驳, 则 是不可满足的. 证明根据归结一步可以传递可满性, 若 是可满足的, 则它的反驳序列中每个子句都是可满足的, 但最後一个空子句是不可满足的. 所以 是不可满足的.□定理3.3(归结方法的完全性)给定一阶语言 , 假设 是 的子句集合. 若 是不可满足的, 则 有一个反驳.□例3.6(简单证明)给定一阶语言 , 其中 是常元,是变元, 是 元谓词符号. 语句的 Skolem 范式是:所对应的子句集合是:若 则 .L C 1,C 2L C 1,C 2U res C 3C 1,C 2X C 3C 1,C 2U res C 351,52L 1L 2L 1J 51(C 1)L 2J 52(C 2)C 3=(51(C 1)-{L 1})P (52(C 2)-{L 2}).C i 9i 9i X 5i (C i )(i=1,2)(51(C 1)-{L 1})P (52(C 2)-{L 2})C 391,92C 3,91,9293.C 1,C 2X C 3.L S L S S S S L S L S S L ={c 1,c 2,P,Q}c 1,c 2x P,Q 1\((^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x))),]z((P(c 1)Z Q(c 2))[\P(z)[\Q(z)).=X X它有一个反驳:因而是永假的, 即是永真的. 子句集合对应的基实例集合是若将 分别看成是命题变元 , 则上述基实例集合对应于命题逻辑语句集合:它有一个反驳:对应于谓词逻辑的反驳:可以直接转换为最初子句集合的反驳:□例3.7(多种证明)给定一阶语言 , 假设 是 元谓词符号, 是 元谓词符号,是三个不同的变元, 是两个不同的常元. 定义以下公式: {P(c 1)Z Q(c 2),\P(z),\Q(z)},< P (c 1)Z Q(c 2),\P(z),\Q(z),Q(c 2),`> .\((^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x)))(^xP(x)Z^xQ(x))> ^x(P(x)Z Q(x)){P(c 1)Z Q(c 2),\P(z),\Q(z)},{P(c 1)Z Q(c 2),\P(c 1),\P(c 2),\Q(c 1),\Q(c 2),},P(c 1),P(c 2),Q(c 1),Q(c 2)p 1,p 2,q 1,q 2{p 1Z q 2,\p 1,\p 2,\q 1,\q 2},<p 1Z q 2,\p 1,\q 2,q 2,`> .<P (c 1)Z Q(c 2),\P(c 1),\Q(c 2),Q(c 2),`> .< P (c 1)Z Q(c 2),\P(z),\Q(z),Q(c 2),`> .L ={c 1,c 2,P,Q,R,S}P,Q,R 1S 2x,y,z c 1,c 2A :^x(P(x)[]y(R(y)> S (x,y))),B :]x(P(x)>]y(Q(y)> \S(x,y))),C :]x(R(x)>\Q(x)).则 .□证明(解释赋值方法).若 是一个解释. 假设 , 以下证明:z从 , 可知存在 , 使得 , 且对任意的 , 都有当 时z因为 且 , 所以因而 . z所以 .证毕.□证明(归结方法).的转化为:的转化为:的转化为:前提与结论的反面可以转化为以下子句:有以下的归结推出:对任意的 , 当 时 .若 则 , , , ,., , ,,A,B X C I I X A [B a J D I R I (a )=1Q I (a )=0I X A b J D I P I (b )=1a J D I R I (a )=1S I (b ,a )=1.I X B I X P I (b )Q I (a )=1S I (b ,a )=0.Q I (a )=0I X C A ^x(P(x)[]y(R(y)>S (x,y))),^x ]y(P(x)[(R(y)>S (x,y)))^x ]y(P(x)[(\R(y)Z S(x,y)))]y(P(c 1)[(\R(y)Z S(c 1,y)))]x(P(c 1)[(\R(x)Z S(c 1,x))){P(c 1),\R(x)Z S(c 1,x)}B ]x(P(x)> ]y(Q(y)> \S(x,y))),]x ]y(P(x)>(Q(y)> \S(x,y))),]x ]y(\P(x)Z\Q(y)Z\S(x,y)),]]x(\P(y)Z\Q(z)Z\S(y,z)),{\P(y)Z\Q(z)Z\S(y,z)}.\C \]x(R(x)> \Q(x)).^x \(R(x)> \Q(x))^x(R(x)[Q(x))R()[Q(c 2){R(c 2),Q(c 2)}C 1:P(c 1)C 2:\R(x)Z S(c 1,x),C 3:\P(y)Z\Q(z)Z\S(y,z),C 4:R(c 2)C 5:Q(c 2)y c 2所以证毕.□例3.8(语义推出)给定一阶语言 , 为 元谓词符号, 为 元谓词符号, 为元谓词符号,是三个不同的常元.是四个不同的变元.是以下公式:则 .证明的转化为:的转化为:的转化为:的转化为:可得以下子句:有以下的归结关系:,,..,.,.,,.C1,C3Ures\Q(z)Z\S(c1,z),C2,C4UresS(c1,c2),\Q(z)Z\S(c1,z),S(c1,c2)Ures\Q(c2),C5,\Q(c2)Ures`.A,B X C.L={a,b,c,P,Q,R,S}P,S1R2Q 3a,b,c x,y,z,w A,B,C,D ]x]y((Q(x,x,y)[\P(y))> S(x)),^x^y(R(y,x)[\P(x))^x]yQ(x,x,y)^xS(x)A,B,C X DA]x]y((Q(x,x,y)[\P(y))> S(x)),]x]y(\Q(x,x,y)Z P(y)Z S(x)),\Q(x,x,y)Z P(y)Z S(x)B^x^y(R(y,x)[\P(x)){R(b,a),\P(a)}C^x]yQ(x,x,y)Q(c,c,z)\D\^xS(x)]x\S(x)\S(w)\Q(x,x,y)Z P(y)Z S(x)R(b,a),\P(a)Q(c,c,z)\S(w)证毕.□例3.9(不可推出)给定一阶语言 , 为 元谓词符号,是两个不同的常元. 是三个不同的变元. 则证明可以化为:可能的归结推出只有:因而上述子句集合没有反驳. 即□例3.10(符号化与证明)某些学生喜欢每门课程, 没有学生喜欢文学. 因此, 没有课程是文学. 假设学生与课程的集合为论域, 定义以下谓词:则有以下的符号化:z“某些学生喜欢每门课程”的符号化为 :\Q(x,x,y)Z P(y)Z S(x),Q(c,c,z)U res P(y)Z S(c),P(y)Z S(c),\P(a)U res S(c),S(c),\S(w)U res `.L ={c 1,c 2,P,Q}P,Q 1c 1,c 2x,y,z ^xP(x),^xQ(x)X^x(P(x)[Q(x))./^xP(x)[^xQ(x)[\^x(P(x)[Q(x))^xP(x)[^xQ(x)[]x(\P(x)Z\Q(x))^x ^y(P(x)[Q(y))[]x(\P(x)Z\Q(x))^x ^y ]z(P(x)[Q(y)[(\P(z)Z\Q(z)){P(c 1),Q(c 2),\P(z)Z\Q(z)}P(c 1),\P(z)Z\Q(z)U res \Q(c 1),Q(c 2),\P(z)Z\Q(z)U res \P(c 2).^xP(x),^xQ(x)X^x(P(x)[Q(x))./P(x)x D(x)x S(x)x L(x,y)x yA ^x(P(x)[]y(D(y)>L (x,y))).z“没有学生喜欢文学”的符号化为 :z“没有课程是文学”的符号化为 :需要证明假设 是两个不同的常元,是三个不同的变元.的转化为:的转化为:的转化为:有以下归结推出关系:因而□作业全部B\^xy(P(x)[S(y)[L(x,y)).C\^x(D(x)[S(x)).A,B X C.c1,c2x,y,zA^x(P(x)[]y(D(y)> L(x,y))).P(c1),\D(y)Z L(c1,y).P(c1),\D()Z L(c1,z).B\^xy(P(x)[S(y)[L(x,y)).\P(x)Z\S(y)Z\L(x,y).\C\\^x(D(x)[S(x)).^x(D(x)[S(x)).D(c2),S(c2).P(c1),\P(x)Z\S(y)Z\L(x,y)Ures\S(y)Z\L(c1,y),S(c2),\S(y)Z\L(c1,y)Ures\L(c1,c2),\D(z)Z L(c1,z),\L(c1,c2)Ures\D(c2),D(c2),\D(c2)Ures`.A,B X C.z。
