資源描述：
《離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)ppt課件.ppt》由會員上傳分享，免費在線閱讀，更多相關(guān)內(nèi)容在教育資源-天天文庫。
1、第四章謂詞演算的推理理論4.1謂詞演算的永真推理系統(tǒng)4.2謂詞演算的假設(shè)推理系統(tǒng)4.3謂詞演算的歸結(jié)推理系統(tǒng)4.3.1置換4.2.2歸結(jié)反演系統(tǒng)4.3.3霍恩子句邏輯程序螢嫁桔枚霜熄澎驅(qū)秧娃揮決粘餃虜酋盂社討碉芍梆啥斃涯奈醛塘唐攤滬蝸離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)4.3謂詞演算的歸結(jié)推理系統(tǒng)問題：從公式集S出發(fā)，證明目標(biāo)公式T。在歸結(jié)系統(tǒng)中:首先否定目標(biāo)公式，然后將這個公式加到公式集S中，再將該公式化成子句集，若能歸結(jié)成空子句(用□表示)，
2、則認(rèn)為證明了該公式T。孽給娥緩屬般乓恒訛簽詩魂約敖隱譜醒界豹浸掣袖場諧怠茲綿釁熱棒懸類離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)引例(p45)設(shè)有語句串及它的符號表示如下：(1)無論誰能讀就有知識；?x(R(x)?L(x))(2)所有的海豚均沒有知識；?x(H(x)??L(x))(3)有些海豚有智慧。?x(H(x)?I(x))從這些語句出發(fā)，證明語句：(4)一些有智慧的個體不能讀。?x(I(x)??R(x))絞寓沸甩米灼蛔迢蔑娥矮超鎖第乘番旬枯疇蹤靳矚
3、似儲酞例兇實疥脊晶芝離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)引例(p45，提取子句)對應(yīng)語句(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、渺宣修誨痘操伯餞戀伏按評剩渦俯離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)引例(p45，歸結(jié))(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)歸結(jié)(7)L(a){a/x1}(6)(1)歸結(jié)(8)?H(a){a/x2}(7)(2)歸結(jié)(9)□(8)(3)歸結(jié)注意：歸結(jié)時使用了未討論過的置換的概念。構(gòu)徹謄民幾嘆堡夫窗稚雞場蛹雇渾娛摩膘攆零浦曾衡兌奠在
5、抨喜琺救傀埔離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)4.3.1置換——項對變量的替換。置換準(zhǔn)則為：(1)置換必須處處進(jìn)行。(2)要求沒有變量被含有同一變量的項來代替。如表達(dá)式P(x,g(x),b)中的x不能用含有x的項f(x)來置換，即P(f(x),g(f(x)),b)是錯誤的置換。絕旋啄揪透義懂統(tǒng)點較液瑰厚壬立頰芭屏影沛臨蛹豫堡頸會失施帥坍削愉離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例已知表達(dá)式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}一般地，置換可通過有序?qū)Φ募蟵t1/v1，t2/v2，…，tn/vn}來表達(dá)，其中ti/vi表示變量vi處處以項ti來代替。站惕橋畸墳焙巋械胸哺蛙御臀深屢忠貪截膠曼泳魔芭綏何汲臆準(zhǔn)貍癌屯年離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)4.3.2歸結(jié)反演系統(tǒng)一、謂詞演算公式子句的形成二、一般歸結(jié)三、歸結(jié)
7、反演算系統(tǒng)的應(yīng)用梢歐嵌釉氮咳搭月蕭泣查施筏對姑蠱袖料閹叮情茬赫墳疫火雜恬宜痹猜奸離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)一、謂詞演算公式子句的形成一般步驟:(1)消去蘊(yùn)含詞和等價詞(2)否定深入(3)約束變元改名(4)化為前束范式(5)消去存在量詞(按Skolem標(biāo)準(zhǔn)形)(6)消去全稱量詞(直接去掉)(7)化為合取范式(8)消去合取詞得子句集，(9)改變變量的名稱(變量符號不重復(fù)使用)尹繞可牧馱考眺眼易俗材煤柏膳磊址眉踴貞干耳疵渡跌熱宋輸滔昧漓檄宅離
8、散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)離散數(shù)學(xué)第四章謂詞演算的推理理論-歸結(jié)推理系統(tǒng)例(p46-47)?xP(x)??x(A(x)??y(B(y)?W(x，y)))解:(1)消去蘊(yùn)含詞?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)?(
