[理學(xué)]lec08一階邏輯-資料下載頁
2025-02-21 12:50本頁面
【正文】 z)→G(x,y,t)) 是前束范式。 ?xF(x)∨ ?xG(x,y) ?x(F(x) → ?y(G(y)→H(x))) 不是前束范式 在一階邏輯中，任何公式的前束范式都是存在的 公式的前束范式不唯一 例 求下列公式的前束范式。 1.?xF(x)∧ ? ?xG(x) 2.?xF(x)∨ ? ?xG(x) 3.?xF(x)→ ? ?xG(x) 4.?xF(x)→ ? ?xG(x) 5.(?xF(x,y)→ ?yG(y))→ ?xH(x,y) 解 1. ?xF(x)∧ ? ?xG(x) ? ?xF(x)∧ ?x ? G(x) 定理 （ 2） ??x（ F(x)∧ ? G(x)） 定理 （ 1） 解法不 唯一 ,前束范式 不唯一 ： 使用 換名規(guī)則求前束范式 ? ?xF(x)∧ ?t ? G(t) 換名規(guī)則 ? ?x (F(x)∧ ?t ? G(t)) 定理 ② ? ?x ( ?t (F(x)∧ ? G(t)) ) 定理 ② ? ?x ?t (F(x)∧ ? G(t)) 2. ?xF(x)∨ ? ?xG(x) ? ?xF(x)∨ ?x ? G(x) ? ?xF(x)∨ ?y ? G(y) 換名規(guī)則 ? ?x(F(x)∨ ?y ? G(y)) ? ?x?y (F(x)∨ ? G(y)) 3. ?xF(x)→ ? ?xG(x) ? ﹁ ?xF(x)∨ ? ?xG(x) ? ?x﹁ F(x)∨ ? x ? G(x) ? ?t﹁ F(t)∨ ? x ? G(x) 換名規(guī)則 ? ?t(﹁ F(t)∨ ? x ? G(x)) ? ?t ? x(﹁ F(t)∨ ? G(x)) 4. ?xF(x)→ ? ?xG(x) ? ﹁ ?xF(x)∨ ? ?x G(x) ? ?x﹁ F(x)∨ ? x ? G(x) ? ?x﹁ F(x)∨ ? y ? G(y) 換名規(guī)則 ? ?x（ ﹁ F(x)∨ ? y ? G(y)） ??x ? y（ ﹁ F(x)∨ ? G(y)） 解法 1 ??xF(x)→ ?x ? G(x) ??xF(x)→ ?y ? G(y) ??x(F(x)→ ?y ? G(y)) ??x ?y(F(x)→ ? G(y)) 解法 2 5. (?xF(x,y)→ ?yG(y))→ ?xH(x,y) ? (?xF(x,z)→ ?yG(y))→ ?xH(x,z)代替規(guī)則 ? (?xF(x,z)→ ?yG(y))→ ?tH(t,z)換名規(guī)則 ? ?x(F(x,z)→ ?yG(y))→ ?tH(t,z) ? ?x?y(F(x,z)→G(y) )→ ?tH(t,z) ? ?x?y((F(x,z)→G(y))→ ?tH(t,z)) ? ?x?y?t ((F(x,z)→G(y))→H(t,z)) 注意事項 : ? 公式的前束范式一般是不唯一的 ? 一個公式的前束范式的各指導(dǎo)變項應(yīng)是各不相同的 ? 原公式中自由出現(xiàn)的個體變項在前束范式中還應(yīng)是自由出現(xiàn)的 ? 可用于檢查等值演算的錯誤 練習(xí) ﹁ (?xF(x,y) ∨ ?yG(x,y)) Q amp。 A ?47
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1