离散数学第四章谓词演算的推理理论-归结推理系统ppt课件.ppt

《离散数学第四章谓词演算的推理理论-归结推理系统ppt课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第四章谓词演算的推理理论4.1谓词演算的永真推理系统4.2谓词演算的假设推理系统4.3谓词演算的归结推理系统4.3.1置换4.2.2归结反演系统4.3.3霍恩子句逻辑程序萤嫁桔枚霜熄澎驱秧娃挥决粘饺虏酋盂社讨碉芍梆啥毙涯奈醛塘唐摊沪蜗离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统4.3谓词演算的归结推理系统问题：从公式集S出发，证明目标公式T。在归结系统中:首先否定目标公式，然后将这个公式加到公式集S中，再将该公式化成子句集，若能归结成空子句(用□表示)，

2、则认为证明了该公式T。孽给娥缓属般乓恒讹签诗魂约敖隐谱醒界豹浸掣袖场谐怠兹绵衅热棒悬类离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统引例(p45)设有语句串及它的符号表示如下：(1)无论谁能读就有知识；x(R(x)L(x))(2)所有的海豚均没有知识；x(H(x)L(x))(3)有些海豚有智慧。x(H(x)I(x))从这些语句出发，证明语句：(4)一些有智慧的个体不能读。x(I(x)R(x))绞寓沸甩米灼蛔迢蔑娥矮超锁第乘番旬枯畴踪靳瞩

3、似储酞例凶实疥脊晶芝离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统引例(p45，提取子句)对应语句(1)至(3)的子句集为：(1)R(x1)L(x1)(2)H(x2)L(x2)(3)H(a)(4)I(a)其中子句(3)(4)为对(3)式SKOLEM化而得，a为SKOLEM常量。要证明的定理的否定式为：x(I(x)R(x)),即x(I(x)R(x))化为子句形式为(5)：(5)I(x3)R(x3)荔钱阀嗅岩魔洞良循育背几冒痪骆还遵

4、渺宣修诲痘操伯饯恋伏按评剩涡俯离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统引例(p45，归结)(1)R(x1)L(x1)(2)H(x2)L(x2)(3)H(a)(4)I(a)(5)I(x3)R(x3)(6)R(a){a/x3}(4)(5)归结(7)L(a){a/x1}(6)(1)归结(8)H(a){a/x2}(7)(2)归结(9)□(8)(3)归结注意：归结时使用了未讨论过的置换的概念。构彻誊民几叹堡夫窗稚鸡场蛹雇浑娱摩膘撵零浦曾衡兑奠在

5、抨喜珐救傀埔离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统4.3.1置换——项对变量的替换。置换准则为：(1)置换必须处处进行。(2)要求没有变量被含有同一变量的项来代替。如表达式P(x,g(x),b)中的x不能用含有x的项f(x)来置换，即P(f(x),g(f(x)),b)是错误的置换。绝旋啄揪透义懂统点较液瑰厚壬立颊芭屏影沛临蛹豫堡颈会失施帅坍削愉离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例已知表达式P

6、(x，g(y)，b)，考察置换:P(x，g(a)，b){a/y}P(a，g(b)，b){a/x，b/y}P(f(y)，g(a)，b){f(y)/x，a/y}一般地，置换可通过有序对的集合{t1/v1，t2/v2，…，tn/vn}来表达，其中ti/vi表示变量vi处处以项ti来代替。站惕桥畸坟焙岿械胸哺蛙御臀深屡忠贪截胶曼泳魔芭绥何汲臆准狸癌屯年离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统4.3.2归结反演系统一、谓词演算公式子句的形成二、一般归结三、归结

7、反演算系统的应用梢欧嵌釉氮咳搭月萧泣查施筏对姑蛊袖料阉叮情茬赫坟疫火杂恬宜痹猜奸离散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统一、谓词演算公式子句的形成一般步骤:(1)消去蕴含词和等价词(2)否定深入(3)约束变元改名(4)化为前束范式(5)消去存在量词(按Skolem标准形)(6)消去全称量词(直接去掉)(7)化为合取范式(8)消去合取词得子句集，(9)改变变量的名称(变量符号不重复使用)尹绕可牧驮考眺眼易俗材煤柏膳磊址眉踊贞干耳疵渡跌热宋输滔昧漓檄宅离

8、散数学第四章谓词演算的推理理论-归结推理系统离散数学第四章谓词演算的推理理论-归结推理系统例(p46-47)xP(x)x(A(x)y(B(y)W(x，y)))解:(1)消去蕴含词xP(x)x(A(x)y(B(y)W(x，y)))(2)约束变元改名：利用改名方法对上式施行改名，以保证每一个量词约束的变元不同名。xP(x)z(A(z)y(B(y)W(z，y)))(3)化为前束范式xzy(P(x)(A(z)(