5.谓词演算(5.1-5.5)

《5.谓词演算(5.1-5.5)》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第五章谓词演算5.1谓词演算的基本概念5.2归结5.3归结反演系统5.4基于归结法的问答系统5.5归结法的应用5.6基于规则的正向演绎系统5.7基于规则的反向演绎系统5.8基于规则演绎系统的搜索策略蛮诅建戍弧而酶韩茄歪将扎瑰诗揣搜邮朽门眨桂钉募踊株了暑吐堡炮琳讯5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)5.1谓词演算的基本概念5.1.1几个基本定义1原子公式：由原子符号与项构成的公式为原子公式，形如：A(x1,x2,……xn)其中：A是谓词，x1,x2,……xn是项，项包括：常量符号

2、、变元、函数例如：A(f(x),y)2合适公式：(1)原子谓词公式是合适公式(2)如果A、B是合适公式，则～A、A∨B、A∧B、A→B、AB是合适公式(3)如果A是合适公式，则是合适公式(4)有限次使用上述规则得到的公式是合适公式例如：嫁堡磷纱氢滦煮六涯独煞学淌伤芽青傍万厚涯刀尹径腊琴桅肯千宣浸詹竟5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)3文字：一个原子公式及原子公式的否定称作文字4句子：所有变量均受约束的合适公式称作句子5二个重要推理规则：（1）假言推理：W1,W1→W2W2（2

3、）全称消去推理：6谓词公式的真值：给定谓词公式wffA，个体域E（1）如果对于A的所有赋值wffA都为真，则称wffA在E上是有效的（永真）（2）如果对于A的所有赋值wffA都为假，则称wffA在E上是不可满足的（永假）（3）如果至少在一种赋值下wffA为真，则称wffA在E上是可满足的7子句：文字的析取组成的公式称子句如：A∨～B措茫抵她抨菲倔宋蔽曳圃貉睫步棚聋亿易兔埃噪内汲眺吼炙江陶狞滔哪裸5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)8前束范式：一个公式，如果所有量词都在整个公式的

4、开头，其作用域延伸到公式的末尾，则称该公式为前束范式，记为：F=(Q1X1)(Q2X2)……(QnXn)M其中：Q1,Q2,……Qn表示量词X1,X2,……Xn表示个体变元M表示不含量词的谓词公式（母式）例如：9合取前束范式：一个前束范式中，谓词公式M由若干合取项构成的公式称作合取前束范式。如：蕉喷艾袜骂艰鞭腑之贬誉涉跃茶恃挠巾哗竖援椿淄喧篷沃琶介牙入意昌苞5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)5.1.2公式标准化目的：将一个给定的公式化成一个合取前束范式，最终得到一个子句集以下

5、例说明公式标准化的过程1消去蕴含符号：利用公式2缩小否定符号的辖域：利用DeMorgan定律3变量标准化：利用变量代换使不同的量词所约束的变元各不相同奸赖楷隆刽秦艾怔洗砖篆分佐抿炒超唬筏啪棉从邓范嘉阴责遵装丘故韶寓5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)5化成前束形式：对于不含有存在量词的谓词公式可以将所有全称量词移到公式左边。此时，每个全称量词的辖域都是整个公式。4消去存在量词：（斯托林标准化）例如：解释为：对于任何一个学生y，都存在一个老师x。显然任取的学生不同，所对应的老师也

6、不同。斯托林函数：受存在量词约束的变元可以用一个函数来代替，函数的自变量包括该存在量词左边全部全称量词约束的变元。如上例中的变元x可以用y的函数代替，得斯托林常量：不含有变量的斯托林函数咸件蒸镣屠浊版跨取俺桓的雹锣长把涩输跃劈率崔杂讹峦雄倾淘靳嘱羚库5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)7消去全称量词：由于公式中的所有变元均受全程量词约束，所以可直接将全称量词消去。6将母式化成合取范式：（每个合取项是一个析取式）利用分配律：8消去合取符号：每个合取项用一个与其等价的子句表示，得到

7、一个子句集。继萧赤呀拢宛低滦役纲概狰楷魁拒配踩剿突坞尚墩煮莉檬岔烹馒膨铭获疹5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)9更换变元名称：（变元分离标准化）关于公式标准化的讨论：（1）利用斯托林函数标准化得前束范式称为S_标准形。（2）S_标准形不唯一。选择不同的斯托林函数可以得到不同的S_标准形。（3）公式F与其S_标准形Fs在F非永假时不等价。芒香怠巫胰帚改忠萄明清饭智泽响藐屏躇斥涛送肢需摊欲归劲圭延捂臭膝5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)一个定理：设Fs是

8、合适公式F的S_标准形子句集，则F永假的充要条件是Fs为永假。圆刁虎立息躬桅敛碎钻棋勒纯丛正离琐份蕊殷亩卓萎祖持苯渣贸呜嘻怎稠5.谓词演算(5.1-5.5)5.谓词演算(5.1-5.5)5.2归结5.2.1归结原理数理逻辑问题的证明方法：问题：给定公式集F1,F2,…Fn，求证：公式W为真，即：要证明F1,F2,…Fn→W为永真式。1直接证明：设：F1∧F2∧…∧Fn为真，推出W为真。2间接证明：设：F1∧F2∧…∧Fn∧～W为假，推出矛盾。对于间接证明