謂詞演算與消解歸結(jié)原理

《謂詞演算與消解歸結(jié)原理》由會(huì)員分享，可在線閱讀，更多相關(guān)《謂詞演算與消解歸結(jié)原理（79頁珍藏版）》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。

1、Department of Computer Science (P Q) (P=Q) 4Department of Computer Science begincase end %end caseendq首 先 ,它 遞 歸 地 試 圖 對(duì) 表 達(dá) 式 的 初 始 成 分 合 一 。 如 果 成功 , 這 次 合 一 返 回 的 任 何 代 入 式 被 用 到 兩 個(gè) 表 達(dá) 式 的 剩下 部 分 , 然 后 以 這 兩 個(gè) 表 達(dá) 式 為 參 數(shù) 。q終 止 條 件 是 兩 個(gè) 參 數(shù) 之 一 為 一 個(gè) 符 號(hào) (謂 詞 名 , 函 詞 名 , 變 元 , 常 元 ), 或 兩 個(gè) 表 達(dá)

2、 式 的 每 一 元 素 都 已 匹 配 了 。 21Department of Computer Science E1是 一 個(gè) 變 元 : if E1在 E2中 出 現(xiàn) then return FAIL else return E2/E1;E2是 一 個(gè) 變 元 : if E2在 E1中 出 現(xiàn) then return FAIL else return E1/E2; 其 他 情 況 : % E1和 E2都 是 表 22Department of Computer Science HE2:= E2的 第 一 個(gè) 元 素 ; SUBS1:= unify (HE1, HE2); if SUBS1

3、 FAIL then return FAIL TE1:= apply (SUBS1, E1的 后 半 部 ) TE2:= apply (SUBS1, E2的 后 半 部 ) SUBS2:= unify (TE1, TE2 ), if SUBS2 FAIL then return FAIL else return SUBS1與 SUBS2 的 合 成 end 23Department of Computer Science minincome (X) = 15000 + (4000 * X) 27Department of Computer Science （ 15） couple(吳 ,周 )

4、 couple(吳 ,徐 ) couple(吳 ,李 )（ 16） couple (吳 ,李 ) （ 15） （ 10） （ 11） 進(jìn) 行 歸 結(jié) ;（ 17） couple （ 王 ， 周 ） couple （ 王 ， 徐 ）（ 18） couple （ 王 ， 徐 ） （ 17） 與 （ 6） 歸 結(jié)（ 19） couple （ 孫 ， 周 ） 57Department of Computer Science (2) 用 S0中 的 子 句 與 S1中 的 子 句 進(jìn) 行 所 有 可 能 的 歸 結(jié) ， 得 到 第二 層 歸 結(jié) 式 ， 把 這 些 歸 結(jié) 式 的 集 合 記 為 S 2

5、; (3) 用 S0和 S1中 的 子 句 與 S2中 的 子 句 進(jìn) 行 所 有 可 能 的 歸 結(jié) ， 得到 第 三 層 歸 結(jié) 式 ， 把 這 些 歸 結(jié) 式 的 集 合 記 為 S3; 如 此 繼 續(xù) ， 知 道 得 出 空 子 句 或 不 能 再 繼 續(xù) 歸 結(jié) 為 止 。 60Department of Computer Science & Technology, Nanjing University Spring I(x) R(x) I(a) R(y) L(y) L(a)R(a) I(x) L(x) R(a)L(a) L(a) I(a) I(a) NILSS1S2例 3.19 設(shè)

6、 有 如 下 子 句 集 ： S= I(x) R(x), I(a), R(y) L(y), L(a) 用 寬 度 優(yōu) 先 策 略 證 明 S為 不 可 滿 足 。 寬 度 優(yōu) 先 策 略 的 歸 結(jié) 樹 如 下 ： 61Department of Computer Science & Technology, Nanjing University Spring u 寬 度 優(yōu) 先 策 略 歸 結(jié) 出 了 許 多 無 用 的 子 句 ， 既 浪 費(fèi) 時(shí) 間 ， 又浪 費(fèi) 空 間 。u 但 是 ， 這 種 策 略 有 一 個(gè) 有 趣 的 特 性 ， 就 是 當(dāng) 問 題 有 解 時(shí) 保證 能 找 到

7、最 短 歸 結(jié) 路 徑 。u 它 是 一 種 完 備 的 歸 結(jié) 策 略 。u 寬 度 優(yōu) 先 對(duì) 大 問 題 的 歸 結(jié) 容 易 產(chǎn) 生 組 合 爆 炸 ， 但 對(duì) 小 問 題卻 仍 是 一 種 比 較 好 的 歸 結(jié) 策 略 。3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-廣 度 優(yōu) 先 策 略 62Department of Computer Science & Technology, Nanjing University Spring u 支 持 集 策 略 是 沃 斯 (Wos)等 人 在 1965年 提 出 的 一 種 歸 結(jié) 策略 。u 它 要 求 每 一 次 參 加 歸

8、結(jié) 的 兩 個(gè) 親 本 子 句 中 ， 至 少 應(yīng) 該 有一 個(gè) 是 由 目 標(biāo) 公 式 的 否 定 所 得 到 的 子 句 或 它 們 的 后 裔 。u 可 以 證 明 支 持 集 策 略 是 完 備 的 ， 即 當(dāng) 子 句 集 為 不 可 滿 足時(shí) ， 則 由 支 持 集 策 略 一 定 能 夠 歸 結(jié) 出 一 個(gè) 空 子 句 。u 也 可 以 把 支 持 集 策 略 看 成 是 在 寬 度 優(yōu) 先 策 略 中 引 入 了 某種 限 制 條 件 ， 這 種 限 制 條 件 代 表 一 種 啟 發(fā) 信 息 ， 因 而 有較 高 的 效 率 3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-

9、支 持 集 策 略 63Department of Computer Science & Technology, Nanjing University Spring I(x) R(x) I(a) R(y) L(y) L(a)R(a) I(x) L(x)L(a) L(a) I(a)NIL例 3.20 設(shè) 有 如 下 子 句 集 ： S= I(x) R(x), I(a), R(y) L(y), L(a) 其 中 ， I(x) R(x)為 目 標(biāo) 公 式 的 否 定 。 用 支 持 集 策 略 證 明 S為 不 可滿 足 。 64Department of Computer Science & Te

10、chnology, Nanjing University Spring u 各 級(jí) 歸 結(jié) 式 數(shù) 目 要 比 寬 度 優(yōu) 先 策 略 生 成 的 少u 但 在 第 二 級(jí) 還 沒 有 空 子 句 。 就 是 說 這 種 策 略 限 制 了 子 句 集 元 素的 劇 增 ， 但 會(huì) 增 加 空 子 句 所 在 的 深 度 。u 支 持 集 策 略 具 有 逆 向 推 理 的 含 義 ， 由 于 進(jìn) 行 歸 結(jié) 的 親 本 子 句 中至 少 有 一 個(gè) 與 目 標(biāo) 子 句 有 關(guān) ， 因 此 推 理 過 程 可 以 看 作 是 沿 目 標(biāo)、 子 目 標(biāo) 的 方 向 前 進(jìn) 的 。 3.7 歸 結(jié)

11、 演 繹 推 理 的 歸 結(jié) 策 略-支 持 集 策 略 65Department of Computer Science & Technology, Nanjing University Spring u 主 要 想 法 是 ： 歸 結(jié) 過 程 在 尋 找 可 歸 結(jié) 子 句 時(shí) ， 子 句 集 中 的 子 句越 多 ， 需 要 付 出 的 代 價(jià) 就 會(huì) 越 大 。 如 果 在 歸 結(jié) 時(shí) 能 把 子 句 集 中無 用 的 子 句 刪 除 掉 ， 這 就 會(huì) 縮 小 搜 索 范 圍 ， 減 少 比 較 次 數(shù) ， 從而 提 高 歸 結(jié) 效 率 。u 常 用 的 刪 除 方 法 有 以 下

12、幾 種 ： 純 文 字 重 言 式 包 孕 3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-刪 除 策 略 66Department of Computer Science & Technology, Nanjing University Spring u純 文 字 刪 除 法 ： 如 果 某 文 字 L在 子 句 集 中 不 存 在 可 與 其 互 補(bǔ) 的 文 字 L， 則 稱 該 文 字 為 純 文 字 。 在 歸 結(jié) 過 程 中 ， 純 文 字 不 可 能 被 消 除 ， 用 包 含 純 文字 的 子 句 進(jìn) 行 歸 結(jié) 也 不 可 能 得 到 空 子 句 ， 因 此 對(duì) 包 含純

13、文 字 的 子 句 進(jìn) 行 歸 結(jié) 是 沒 有 意 義 的 ， 應(yīng) 該 把 它 從 子句 集 中 刪 除 。 對(duì) 子 句 集 而 言 ， 刪 除 包 含 純 文 字 的 子 句 ， 是 不 影 響其 不 可 滿 足 性 的 。 例 如 ， 對(duì) 子 句 集 S=P Q R, Q R, Q, R其 中 P是 純 文 字 ， 因 此 可 以 將 子 句 P Q R從 子 句 集 S中 刪 除 。 3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-刪 除 策 略 67Department of Computer Science & Technology, Nanjing University Spr

14、ing u 重 言 式 刪 除 法 如 果 一 個(gè) 子 句 中 包 含 有 互 補(bǔ) 的 文 字 對(duì) ， 則 稱 該 子 句 為 重 言 式 。例 如 P(x) P(x), P(x) Q(x) P(x) 都 是 重 言 式 ， 不 管 P(x)的 真 值 為 真 還 是 為 假 ， P(x) P(x)和P(x) Q(x) P(x)都 均 為 真 。 重 言 式 是 真 值 為 真 的 子 句 。 對(duì) 一 個(gè) 子 句 集 來 說 ， 不 管 是 增 加 還是 刪 除 一 個(gè) 真 值 為 真 的 子 句 ， 都 不 會(huì) 影 響 該 子 句 集 的 不 可 滿足 性 。 因 此 ， 可 從 子 句 集

15、 中 刪 去 重 言 式 。3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-刪 除 策 略 68Department of Computer Science & Technology, Nanjing University Spring u 包 孕 刪 除 法 設(shè) 有 子 句 C1和 C2， 如 果 存 在 一 個(gè) 置 換 ， 使 得 C1 C2， 則 稱C1包 孕 于 C2。 例 如 P(x) 包 孕 于 P(y) Q(z) =x/y P(x) 包 孕 于 P(a) =a/x P(x) 包 孕 于 P(a) Q(z) =a/x P(x) Q(a) 包 孕 于 P(f(a) Q(a) R(

16、y) =f(a)/x P(x) Q(y) 包 孕 于 P(a) Q(u) R(w) =a/x, u/y 對(duì) 子 句 集 來 說 ， 把 其 中 包 孕 的 子 句 刪 去 后 ， 不 會(huì) 影 響 該 子 句 集的 不 可 滿 足 性 。 因 此 ， 可 從 子 句 集 中 刪 除 哪 些 包 孕 的 子 句 。3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-刪 除 策 略 69Department of Computer Science & Technology, Nanjing University Spring u 如 果 一 個(gè) 子 句 只 包 含 一 個(gè) 文 字 ， 則 稱 此 子

17、 句 為 單 文 字 子 句 。單 文 字 子 句 策 略 是 對(duì) 支 持 集 策 略 的 進(jìn) 一 步 改 進(jìn) ， 它 要 求 每 次參 加 歸 結(jié) 的 兩 個(gè) 親 本 子 句 中 至 少 有 一 個(gè) 子 句 是 單 文 字 子 句 。3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-單 文 字 子 句 策 略 70Department of Computer Science & Technology, Nanjing University Spring I(x) R(x) I(a) R(y) L(y) L(a)R(a) R(a)NIL例 3.21 設(shè) 有 如 下 子 句 集 ： S= I(

18、x) R(x), I(a), R(y) L(y), L(a) 用 單 文 字 子 句 策 略 證 明 S為 不 可 滿 足 。 q采 用 單 文 字 子 句 策 略 ， 歸 結(jié) 式 包 含 的 文 字 數(shù) 將 少 于 其 親 本 子 句 中 的 文 字 數(shù)， 這 將 有 利 于 向 空 子 句 的 方 向 發(fā) 展 ， 因 此 會(huì) 有 較 高 的 歸 結(jié) 效 率 。 q但 這 種 策 略 是 不 完 備 的 ， 即 當(dāng) 子 句 集 為 不 可 滿 足 時(shí) ， 用 這 種 策 略 不 一 定 能歸 結(jié) 出 空 子 句 。 71Department of Computer Science & Tec

19、hnology, Nanjing University Spring u 這 種 策 略 要 求 每 次 參 加 歸 結(jié) 的 兩 個(gè) 親 本 子 句 中 ， 至 少 應(yīng)該 有 一 個(gè) 是 初 始 子 句 集 中 的 子 句 。u 所 謂 初 始 子 句 集 是 指 開 始 歸 結(jié) 時(shí) 所 使 用 的 子 句 集 。 3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-線 形 輸 入 策 略 72Department of Computer Science & Technology, Nanjing University Spring I(x) R(x) I(a) R(y) L(y) L(a)R

20、(a) I(x) L(x) R(a) I(a) L(a) L(a) I(a)NIL例 3.22 設(shè) 有 如 下 子 句 集 ： S= I(x) R(x), I(a), R(y) L(y), L(a) 用 線 性 輸 入 策 略 證 明 S為 不 可 滿 足 。 73Department of Computer Science & Technology, Nanjing University Spring q線 性 輸 入 策 略 可 限 制 生 成 歸 結(jié) 式 的 數(shù) 目 ， 具 有 簡 單 和 高 效的 優(yōu) 點(diǎn) 。q但 是 ， 這 種 策 略 也 是 一 種 不 完 備 的 策 略 。 74

21、Department of Computer Science & Technology, Nanjing University Spring u 這 種 策 略 與 線 性 輸 入 策 略 有 點(diǎn) 相 似 ， 但 是 ， 放 寬 了 對(duì) 子 句 的限 制 。 每 次 參 加 歸 結(jié) 的 兩 個(gè) 親 本 子 句 ， 只 要 滿 足 以 下 兩 個(gè) 條件 中 的 任 意 一 個(gè) 就 可 進(jìn) 行 歸 結(jié) ： (1) 兩 個(gè) 親 本 子 句 中 至 少 有 一 個(gè) 是 初 始 子 句 集 中 的 子 句 。 (2) 如 果 兩 個(gè) 親 本 子 句 都 不 是 初 始 子 句 集 中 的 子 句 ， 則

22、 一 個(gè) 子句 應(yīng) 該 是 另 一 個(gè) 子 句 的 先 輩 子 句 。 所 謂 一 個(gè) 子 句 (例 如 C1)是 另一 個(gè) 子 句 (例 如 C2)的 先 輩 子 句 是 指 C2是 由 C1與 別 的 子 句 歸 結(jié)后 得 到 的 歸 結(jié) 式 。3.7 歸 結(jié) 演 繹 推 理 的 歸 結(jié) 策 略-祖 先 過 濾 策 略 75Department of Computer Science & Technology, Nanjing University Spring Q(x) P(x) Q(y) P(y) P(x) Q(w) P(w) Q(w) Q(a) P(a)P(a)NIL例 3.23 設(shè)

23、 有 如 下 子 句 集 ：S= Q(x) P(x), Q(y) P(y)， Q(w) P(w) , Q(a) P(a) 用 祖 先 過 濾 策 略 證 明 S為 不 可 滿 足祖 先 過 濾 策 略 也 是 完 備 的 76Department of Computer Science & Technology, Nanjing University Spring 用 歸 結(jié) 反 演 求 取 問 題 的 答 案u 歸 結(jié) 原 理 出 了 可 用 于 定 理 證 明 外 ， 還 可 用 來 求 取 問 題 答 案 ， 其 思想 與 定 理 證 明 相 似 。u 其 一 般 步 驟 為 ： (1)

24、 把 問 題 的 已 知 條 件 用 謂 詞 公 式 表 示 出 來 ， 并 化 為 相 應(yīng) 的 子 句 集； (2) 把 問 題 的 目 標(biāo) 的 否 定 用 謂 詞 公 式 表 示 出 來 ， 并 化 為 子 句 集 ； (3) 對(duì) 目 標(biāo) 否 定 子 句 集 中 的 每 個(gè) 子 句 ， 構(gòu) 造 該 子 句 的 重 言 式 （ 即 把該 目 標(biāo) 否 定 子 句 和 此 目 標(biāo) 否 定 子 句 的 否 定 之 間 再 進(jìn) 行 析 取 所 得 到的 子 句 ） ， 用 這 些 重 言 式 代 替 相 應(yīng) 的 目 標(biāo) 否 定 子 句 式 ， 并 把 這 些重 言 式 加 入 到 前 提 子 句 集

25、 中 ， 得 到 一 個(gè) 新 的 子 句 集 ； (4) 對(duì) 這 個(gè) 新 的 子 句 集 ， 應(yīng) 用 歸 結(jié) 原 理 求 出 其 證 明 樹 ， 這 時(shí) 證 明 樹 的 根 子 句 不 為 空 ， 稱 這 個(gè) 證 明 樹 為 修 改 的 證 明 樹 ； (5) 用 修 改 證 明 樹 的 根 子 句 作 為 回 答 語 句 ， 則 答 案 就 在 此 根 子 句 中。 77Department of Computer Science & Technology, Nanjing University Spring u 一 個(gè) 例 子 來 說 明 如 何 求 取 問 題 的 答 案 ： 例 3.2

26、4 已 知 ： “張 和 李 是 同 班 同 學(xué) ， 如 果 x和 y是 同 班 同 學(xué) ， 則 x的 教 室 也 是 y的 教 室 ， 現(xiàn) 在 張 在 302教 室 上 課 。 ” 問 ： “現(xiàn) 在 李 在 哪 個(gè) 教 室 上 課 ？ ” 解 ： 首 先 定 義 謂 詞 ： C(x, y) x和 y是 同 班 同 學(xué) ； At(x, u) x在 u教 室 上 課 。 把 已 知 前 提 用 謂 詞 公 式 表 示 如 下 ： C(zhang, li) ( x) ( y) ( u) (C(x, y) At(x, u)At(y,u) At(zhang, 302) 把 目 標(biāo) 的 否 定 用 謂

27、詞 公 式 表 示 如 下 ： ( v)At(li, v) 78Department of Computer Science & Technology, Nanjing University Spring 把 上 述 公 式 化 為 子 句 集 ： C(zhang, li) C(x, y) At(x, u) At(y, u) At(zhang, 302)把 目 標(biāo) 的 否 定 化 成 子 句 式 ， 并 用 重 言 式 At(li,v) At(li,v)代 替 之 。 把 此 重 言 式 加 入 前 提 子 句 集 中 ， 得 到 一 個(gè) 新 的 子 句 集 ， 對(duì)這 個(gè) 新 的 子 句 集

28、， 應(yīng) 用 歸 結(jié) 原 理 求 出 其 證 明 樹 。 其 求 解 過程 如 下 圖 所 示 。 該 證 明 樹 的 根 子 句 就 是 所 求 的 答 案 ， 即 “李 明 在 302教 室 ”。 79Department of Computer Science & Technology, Nanjing University Spring At(li,v) At(li,v) C(x, y) At(x, u) At(y, u)At(li,v) C(x, li) At(x, v) C(zhang, li) At(zhang,v) At(li, v) At(zhang, 302)At(li, 302)li/y,v/uZhang/x 302/v