謂詞邏輯基礎(chǔ)-預(yù)覽頁
【正文】 f(x)代替之 ， 這樣得到： (?x)(?u)(?v) (P(a, x, f(x)) ∨ Q(v, b)∨ R(u)) ? 消去 (?u)，同理使用 g(x)代替之，這樣得到： (?x) (?v) ( P(a, x, f(x)) ∨ Q(v, b) ∨ R(g(x))) ? 則 ， 略去全稱變量 ， 原式的 Skolem標(biāo)準(zhǔn)形為： P(a, x, f(x)) ∨ Q(v, b) ∨ R(g(x)) ? 子句與子句集 ? 文字：不含任何連接詞的謂詞公式 。 注意： 左邊有全程量詞的存在量詞，消去時該變量改寫成為全程量詞的函數(shù)；如沒有，改寫成為常量。 在個體域 D是全總個體域時 ， 引入特殊謂詞 R(x)表示 x是人 ， 可符號化為： （ 1） ?x（ R(x) → P(x)） , 其中 ， R(x)表示 x是人； P(x)表示 x是要死的 。 謂詞邏輯基礎(chǔ) 謂詞邏輯基礎(chǔ) ? 例如： （ 1） 所有的人都是要死的 。 ? 我去買花 。 ? 8是個自然數(shù) 。 顯然前兩個謂詞表示的是事物的性質(zhì) ， 第三個謂詞 “ 去買 ” 表示的一個動作也表示了主 、 賓兩個個體詞的關(guān)系 ， 最后一個謂詞 “ 是朋友 ” 表示兩個個體詞之間的關(guān)系 。 （ 2） ?x Q(x), 其中 Q(x)表示 x活到一百歲以上 。 謂詞邏輯歸結(jié)原理 即： 把所有的量詞都提到前面去，然后消掉所有量詞 (Q1x1)(Q2x2)… (Qnxn)M(x1,x2,… ,xn) 約束變項(xiàng)換名規(guī)則： ? (Qx ） M（ x） = （ Qy ） M（ y） ? (Qx ） M（ x,z） = （ Qy ） M（ y,z） 謂詞邏輯歸結(jié)原理 ? ? ? ? ? ? ? ? ? ? ? ? ? ? 量詞消去原則： 消去存在量詞 “ ?” ，略去全程量詞“ ?” 。 注意 ：謂詞公式 G的 SKOLEM標(biāo)準(zhǔn)形同 G并不等值 。 謂詞邏輯歸結(jié)原理 ? G是不可滿足的 = S是不可滿足的 ? G與 S不等價，但在不可滿足得意義下是一致的。 ? 有 SG = S1 U S2 U S3 U … U Sn 則 SG 與 S1 U S2 U S3 U … U Sn在不可滿足得意義上是一致的 。 ? 方法： ? 和命題邏輯一樣。 其中 ， x1, x2, … , xn是互不相同的變量 ， t1, t2, … , tn是不同于 xi的項(xiàng) （ 常量 、 變量 、 函數(shù) ） ； ti/xi表示用 ti置換 xi， 并且要求 ti與 xi不能相同 ， 而且 xi不能循環(huán)地出現(xiàn)在另一個 ti中 。?。?/xn, u1/y1, u2/y2, … , un/yn } 中刪去以下兩種元素： ? i. 當(dāng) ti?=xi時 ， 刪去 ti?/xi (i = 1, 2, … , n)。 在該集合中 ， y/y滿足定義中的條件 i， 需要刪除； a/x， b/y滿足定義中的條件 ii， 也需要刪除 。 同時稱 F1，F(xiàn)2， ... ， Fn是可合一的 。 求證：張是快樂的 。 ※ Herbrand定理的不實(shí)用性引出了可實(shí)用的歸結(jié)法。 或者說 ， 少做些歸結(jié)仍能導(dǎo)出空子句 。 這樣的推理過程便稱做使用了刪除策略的歸結(jié)過程 。 然而要在歸結(jié)式 Cj產(chǎn)生后方能判別它是否可被刪除 ， 這部分計(jì)算量是要花費(fèi)的 ， 只是節(jié)省了被刪除的子句又生成的歸結(jié)式 。 就是說 ， 至少有一個子句來自于支撐集 T或由 T導(dǎo)出的歸結(jié)式 。問題是如何尋找合適的支撐集。 語義歸結(jié)策略的歸結(jié)是完備的，同樣，所有可歸結(jié)的謂詞公式都可以用采用語義歸結(jié)策略達(dá)到加快歸結(jié)速度的目的。而Bi屬于 S或是已出現(xiàn)的歸結(jié)式 Cj(ji)。否則也可能事與愿違。所以說 “ 反之不成立 ” ，即此問題不能采用單元?dú)w結(jié)策略 。 謂詞邏輯歸結(jié)原理 如同單元?dú)w結(jié)策略，不是所有的可歸結(jié)謂詞公式的最后結(jié)論都是可以從原始子句集中的
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1