〈 情 報 学共 同研 究〉
知識情報処理 における帰納的推論
鈴 木 昇 一,中 村 三 郎
Inductive Inference in the Case of Processing Knowledge- Information
Shoichi SUZUKI and
Saburo NAKAMURA
A difference among informations, observational sentences, facts, rules and knowledges and the meanings of them are explained in terms of making an inductive inference about an accommodation of knowledges being in store for a deductive knowledge base (DKB). A model-inference algorithm, a contradiction-backtracing algorithm and a refinement algor- ithm are devised and presented here appearing in the concrete form in order to secure the DKB which adopts a Horn logic. It should be noted that the inductive inference of theories from facts proposed by E. Y. Shapiro is represented within the scope of the Horn logic which excludes the most general atom from the refinement algorithm.
1.情 報 と知 識,知 識 ベ ー ス
Theunknownisinferredfromthe
known.(未 知 は 既 知 か ら 推 論 さ れ る 。)
本 論 文 で は,知 能(intelligence)の 本 質 は,情 報 を処 理 す る 場 面 に お い て 情 報(infor‑
mation)を 知 識(knowledge)と し て 学 習 (leaming)に よ っ て 獲 得 し(knowledge acquisition),推 論(inference)に 好 都 合 な 様
に 表 現 し(knowledgerepresentation),数 式 モ デ ル と い う よ り は 記 号 的 な モ デ ル と し て 定 式 化 さ れ る 場 面 が 多 い 悪 構 造 問 題(1)(ill‑
structuredproblems)の 解 決 に 利 用 す る
(knowledgeutilization)過 程 に あ る と考 え, 変 数(variable)が 関 数(function),述 語
(predicate)の 引 数(argument)の み に 現 わ れ る こ と が 許 さ れ る 第1階 述 語 論 理(2)(first‑
orderpredicatecalculus)の 範 囲 で,そ の コ ン ピ ュ ー タ 上 で の 推 論 方 法 が 調 査 研 究 さ れ る 。
情 報(information)と は 何 か(5)?
例 え ば,状 況 意 味 論(situationsemantics) の 立 場 か ら す れ ば(3),情 報 内 容 は 表 現(repre‑
sentation)S,環 境(circumstance)・C,・ 制 約(constraint)Rに 対 し,相 対 的 で あ り,こ れ を 明 示 す る た め に,情 報 内 容(information content)をCR(S,C)で 表 わ す 。
こ こで は,知 識 の 合 成(論 理 プ ロ グ ラ ム に
よ る 知 識 の 表 現)の 立 場 か ら,情 報 と は, 対 象 とす る 世 界(universe)の 個 体 間 の 諸 関 係 が 観 測 さ れ て 得 ら れ る 観 測 文(obser・
vationalsentence)
の こ とで あ る とす る 。 例 え ば,第1階 述 語 論 理 の 範 囲 で は 原 子 論 理 式 †(atomicfor‑
mula)
10ve(x,y)と 関 数(function)wife(x)が
love(x,y)‑true・
false:::::欝 弩 ・
wife(x)=xの 妻と定 義 さ れ て い れ ば,Tomの 妻 はSusieを 愛 し て い る 文
love(wife(̀Tom'),̀Susie')
は 観 測 文 で あ る 。 な お,対 象 と す る 世 界 の な か の 個 体 定 数 の 集 合Dを 議 論 領 域(universe ofdiscourse)と い う が,̀Tom'と か̀Susie'は
Dの 要 素 で あ る 。
事 実(fact)と は 真(true)あ る い は 偽(false) と判 明 し て い る観 測 文 の こ とで あ る 。 †
Glove(wife(̀Tom'),̀Susie'),true>
clove(̀Tom',wife(̀Tom')),false>
は 事 実 で あ る 。 例 え ば,第2番 目 の 事 実 は
「TomはTomの 妻 を 愛 し て い る 」 と い う観 測 文
love(̀Tom',wife(̀Tom'))
は 偽 で あ る こ と を 表 し て い る 。
規 則(rule)と は,二 つ 以 上 の 事 実 の 間 に 成 立 す る 不 変 関 係 の こ と で あ る 。 例 え ば,
mother(x,y)̲{:rue・
alse:::::器 母で あ
parent(x,y)一{true・f
alse:::二攤 罫
woman(x)‑true・f
alse:::二 辮 あ る と い う三 つ の 原 子 論 理 式 を 導 入 し て 得 ら れ る 文
mother(x,y):‐parent(x,y),woman(x).
(xがyの 親 で,し か もxが 女 で あ れ ば, xはyの 母 で あ る)
は 一 つ の 規 則 で あ る 。
知 識(knowledge)と は,情 報,事 実,規 則 が 推 論 α①(reasoning,inference)に 利 用 可 能 な 形 式 に 加 工 さ れ た も の で あ る 。
前 述 の,知 識 の 獲 得(24)(knowledge acquisition),知 識 の 表 現(knowledge representation),知 識 の 利 用(knowledge utilization)に 関 す る,人 工 知 能(90)(artificial intelligence)の 応 用 分 科 が 知 識 工 学as)
(knowledgeengineering)と 称 せ ら れ る も の で あ る 。
最 後 に,知 識 べ 一 ス ⑳(knowledgebase) とい う の は,多 目 的 用 に 形 成 さ れ た 知 識 の 集 合 体 の こ とで あ る 。
† そ れ 自 身,論 理 記 号(A,V,〜,⊃,∀,∋)を 含 ま な い 論 理 式 が 原 子 論 理 式(素 論 理 式,基 本 式), あ る い は ア トム と い わ れ る も の で あ る 。
† 現 実 世 界 に お い て は,必 ず し も真 か 偽 か と い う よ う に 明 確 に 決 定 で き る 観 測 文 だ け で は な く,通 常 の 観 測 文 に は不 完 全 性(incompleteness),不 確 実 性(uncertainty),あ い ま い 性(ambiguity,fuzzyness),多 義 性 (polymeanings),信 念(belief)な どが 多 く入 り込 ん で お り,こ れ ら を 一 つ の 枠 組 で 扱 う こ と は 困 難 で あ る。
不 麒 性 推 論(6),非 単 調 推 論(7)(non‑monotonicreasoning),常 灘 論(8)(common‑sensereasoning,デ
フ ォ ル ト推 論(9)),近 似 推 論(Fuzzy推 論ao),au),定 性 推 論aa)(qualitativereasoning),発 想 推 論(仮 説 推 論 ⑬'￠の (hypothesis‑basedreasoning)),類 推 鳳 α⑳(analogicalreasoning)な ど が 知 識 の 利 用 に あ た っ て 必 要 と さ れ る が,こ れ ら は 表 現 法,意 味 論 が 発 展 途 上 に あ り,解 説 は 割 愛 さ れ る 。
真,偽の決定
騰 ⇔ 観測 文]:=蠶
L̲加 工
[=
l
L̲̲̲̲→ 卜
2.知 識 の 表 現
規 則1 規 則2
⇒脚
新知識
一 般 に,知 識 の 表 現 法 ⑳'伽'㈱に は (イ)論 理 †に よ る表 現 … … 古 典 論 理,直
感 主 義 論 理,命 題 論 理,述 語 論 理,非 単 調 論 理(non‑monotoniclogic),時
相 論 理(temporallogic),多 ソ ー ト論 理(manysortedlogic),多 層 論 理 (manylayeredlogic),確 定 節(̀defi・
niteclanse)に 基 づ く論 理(ホ ー ン論 理),プ ロ ダ ク シ ョ ン シ ス テ ム ㈱(pro‑
ductionsystem)
(ロ)グ ラ フ に よ る 表 現 … … 例 え ば,意 味 ネ ッ ト ワ ー ク(劾(semantic
network),フ レ ー ム 表 現(1)(frame repreSentation)等
が あ る 。
本 章 で は,Robinson(1965)に よ っ て 提 案 さ れ た 導 出 原 理 ⑳'㈱'⑳(resolutionprinciple) に 基 づ く人 工 知 能 用 の 言 語prologを 簡 単 に 説 明 す る 。 こ れ は1階 述 語 論 理 の 部 分 系 に 基 づ く"確 定 節 に 基 づ く知 識 表 現"法 を 提 供 す る 。
・ ム エ ー
DEC‑10Prologの 記 法(4)で,宣 言 型 プ ロ グ ラ ム 言 語(論 理 型 言 語)と し て のPrologを 説 明 す る 。Prologは 第5世 代 コ ン ピ ュ ー タ の 核 言 語 と し て 採 用 さ れ て い る ††。
た と え ば,与 え られ た 二 つ の 数X,Yの 内, 大 き い 方 を 求 め る 文 を 手 続 プ ロ グ ラ ム 言 語 と
し て のPL/1(3Dで 書 け ば IFX>YTHENZ=X;ELSEZ=Y;
と な る 。 変 数ZにX,Yの 内 大 き い 方 の 値 が 得 られ て い る 。
一 方,知 識 表 現 形 言 語Prologで は max(X,Y,X):‐X>Y.
max(X,Y,Y):‐X<=Y.
と書 か れ る 。 述 語max(X,Y,Z)の 第3番 目 の 引 数Zに,X,Yの 内 大 き い 方 の 値 が 得 ら れ て い る 。 こ こ に
㎜ :f:∴ ≒{繋 昏
以 下,Prologの 文 法(構 文),動 作(意 味) を 簡 単 に 説 明 す る。
1.構 文(32)(syntax)
Prologを 使 っ て 書 か れ た プ ロ グ ラ ム は 論 理 プ ロ グ ラ ム(logicprogram)と も呼 ば れ, 次 の 四 つ の 形 式(1)〜(4)か ら成 る。
(1)規 則 節(ruleclause) A:‑B1,B2,… …,Bn .
こ こ で,A,B1,… …,Bnは 各 々 一 つ の 述 語(predicate)と して の 原子 論 理 式 を 表 し,(A, B1,… …,B。 の 各 変 数 へ 任 意 の 値 を割 り当 て た
† 論 理学(鋤は,自 然言 語 の意 味や 内容,及 び その上 で の思 考や 推論 をあ い まい さ を排 除 して形式 的 に表 現 す る こ とを目的 として発 展 した こ とを考 え る と,論 理 とは あ る意味 で 自然 言語 の近 似 で あ る とみな す こ とが で き よ う。 ㈱
†† 実 際 に 核 言 語 と し て 採 用 さ れ て い る の は,プ ロ セ ス の 実 行 が そ れ ら プ ロ セ ス へ の デ ー タ の 到 着 に よ つ て 制 御 さ れ て い る デ ー タ 駆 動 のGHC(GuardedHomClauses)で あ る 。 ㈹ ・(42)
と き)Aがtrueと な る の はB1,… …,Bnが 共 に trueに な る 場 合 で あ る と 読 む †。Aは 頭 部 (head),B、,… …,Bnは 体 部(body)と 呼 ば れ る 。 い ず れ も 論 理 否 定 記 号(negation symbol)〜 ・を も た な い 述 語 で あ る 。 体 部 に 現 れ る 記 号 「,」は 連 言 記 号(conjunctionsym‑
bol)を 表 す 。
(2)事 実 節 ††(factclause)A.
こ れ は,規 則 節 の 体 部 を 空 に し た も の に 対 応 し て お り,Aは 真 で あ る と読 む 。
(3)目 標 節(goalclause)
?‑B1,・ ・… ・,Bn.
こ れ は規 則 節 の 頭 部 を 空 に し た も の に 対 応 し,B、,… …,B。 を 共 に 真 に せ よ と 読 む 。体 部 に 現 わ れ る 各 述 語Biを 副 目 標(subgoal)と
呼 ぶ 。
(4)空 節(emptyclause)?一.
・こ れ は 規 則 節 の 頭 部 と体 部 を 空 に し た も の に 対 応 し,常 にfalseで あ る と読 む 。 □
(1),(2)の 規 則 節,事 実 節 を 簡 単 に プ ロ グ ラ ム 節(programclause)と い う。
上 述 の(1)の 規 則 節 は,「B、andB2and… … andB。 はAが 成 立 す る た め の 十 分 条 件 で あ る 」 こ と を,い い か え れ ば
ifBlandBZand・ ・・…andBnthenA
(仮 定B、andB2and… …andB。 か ら結 論Aへ の 含 意)
を 意 味 し て お り,決 し て 必 要 か つ 十 分 条 件 で
は な い 。†††こ れ がPrologで 表 現 さ れ た プ ロ グ ラ ム が 肯 定 情 報 の み か ら し か 演 繹 で き な い 理 由 を 与 え る こ と に 注 意 し て お こ う 。
ま た,上 述 の(2)の 事 実 節 は 無 条 件Aが 成 立 す る こ と を 意 味 し て い る 。
II.逐 次 計 算 機 上 の 動 作(37」(意 味, semantics)… …SLD導 出 … …
逐 次 処 理 形 コ ン ピ ュ ー タ 上 のProlog論 理 プ ロ グ ラ ム の 実 行 は,1の(3)の ゴ ー ル 節 の 体 部 の 各 述 語(サ ブ ゴ ー ル)を,1の(1),(2)の 形 式 か ら成 る プ ロ グ ラ ム 節 の 集 合(論 理 プ ロ
グ ラ ム)を 適 用 し て,左 か ら右 に 順 に 実 行 し て い く こ と か ら 始 ま り,そ の と き の 実 行 サ ブ ゴ ー ル が 真 に な れ ば こ の サ ブ ゴ ー ル は 空 に 書 き換 え ら れ,1の(3)の ゴ ー ル 節 が1の(4)の 空 節 に 書 き換 え ら れ た と き に 終 了 す る 。
次 のi〜ivに 分 け て,実 行 過 程 を 更 に 詳 し く説 明 し よ う。
(i)ゴ ー ル 節Giが
G,… …?‑A1,… …,Ak.
で あ り,プ ロ グ ラ ム 節C,+、 が C1+1… …A:‑B1,… …,Bq.
で あ る とす る 。 こ の と き,G1の 体 部 の 最 左 端 に あ るA、 とAの お の お の 引 数 に 含 ま れ る 変 数 に"適 当 な 代 入e,+、"を 施 し,両 者 を 同 一 化,※ す な わ ち
Ald,+1=AB,+1
と す る こ とが で き れ ば ※※,Ci+、 の 選 択 に よ り
† 表 現Sに 含 ま れ る 変 数 をV、,… …,V,と し た と き,θ={V、/ty,… …,V。/t。}と し て,Sに θ を 作 用 さ せ た 結 果 をSθ と 書 け ば,こ のSθ はS中 の 変 数Vi(1≦i≦n)の 各 出 現(occurrence)を 項(te㎜) t,で 置 きか え た 結 果 を 表 す 。 θ は 代 入(substitution)と 呼 ば れ る 。 また,項 とは 次 の(a),(b)に よ っ て 再 帰 的 に 定 義 さ れ 得 られ た もの を い う:(a)定 数 お よ び 変 数 は各 々 項 で あ る 。(b)t、,… …,t。 の 各 々 を項,fをn引 数 の ・ 関 数 記 号 と す る と,記 号 列f(t、,… …,t。)は 項 で あ る 。
††A.はA:一.の 略 記 法 で あ る 。
††† 必 要 か つ 十 分 条 件 とす る た め に は,論 理 プ ロ グ ラ ム の 完 備 化(completion)と い う解 釈 が 必 要 で あ る ㈲ 。
※ こ の と き,代 入B,+、 を{A、,A}の 単 一 化 作 用 素(unifier)と い う。
※※ プ ロ グ ラ ムC +、の 頭 部Aと 同 一 化 で き る ゴ ー ル 節 の 原 子 式 を"選 択 さ れ た 原 子 式"(selectedatom) と い う。計 算 規 則(computationrule)と は,ゴ ー ル 節 中 か ら こ の 種 の あ る 原 子 式 を選 択 す る 仕 方 を い う。Prolog で は ゴ ー ル 節 内 の 最 も左 に あ る 原 子 式 を選 択 す る 計 算 規 則 を採 用 し て い る こ と に な る 。
"A
、は 実 行 さ れ た"
と い い,新 し い ゴ ー ル 節G1+、 を 得 る:
G1+i… …?一(B1,… …,Bq,A2,… …, Ak)B,+、.
Robinsonに よ る 導 出 原 理(resolution principle)の 用 語 で は,G1+、 をGiとCi+、 の 導 出 形(resolvent)と い う。
A、 に 対 し て 単 一 化 可 能 なC,+、 が 選 択 て き な け れ ば,A、 の 実 行 は 失 敗(failure)し,Gi が 失 敗 し た と し て,後 述 の111の ご と く後 戻 り
を行 う。(iの 説 明 ・終 り)
こ こ で,Giに お い てfA、 が 実 行 さ れ た 」 と い う こ と は,
「A1の 実 行 がG1+1で の(B1,… …,Bq) B,+1の 実 行 に 置 き換 え ら れ た 」 と い う意 味 で あ り,後 述 す る
「A、の 実 行 が 成 功 し た 」
と い う こ と を 必 ず し も意 味 し な い こ と に 注 意 す る 。 ま た,「 両 者 を 単 一 化 す る た め の 適 当 な 代 入 」 と は
「最 も一 般 的 な(最 汎)単 一 化 作 用 素(mgu;
mostgeneralunifier)な る 代 入 」 の こ とで あ る 。
θが{A,A、}の 単 一 化 作 用 素 で あ り, {A,A、}の 任 意 の 単 一 化 作 用 素Zに 対 し
て,
τ=θ ・η
(θ・η は あ る 原 子 論 理 式 に θ を 作 用 さ せ た 結 果 に η を 作 用 さ せ る 代 入) と な る 代 入 η が 存 在 す る と き,代 入 θ を
{A,A1}のmguと い う 。
AとA、 とがmguに よ り同 一 化 可 能 な ら, 両 者 は ユ ニ ィ フ ァイ 可 能,単 一 化 可 能(mifia‑
ble)で あ る とい う 。 同 一 化 操 作 の こ と を ユ ニ ィ フ ィ ケ ー シ ョ ン(unification),単 一 化 と い う 。
(ll)目 標 節Gが 与 え ら れ,こ のG(=G。) に 対 し,iを 繰 り返 す と,ゴ ー ル 節 の 系 列
Go,G1,… …,Gn と代 入 の 系 列
θ1,・・・…,en
と を 得 る 。 も し,G。 が 空 節 に な れ ば,G(=
G。)の 実 行(プ ロ グ ラ ム 節 か ら成 るPrologプ ロ グ ラ ム の 実 行)は 成 功(success)し て 終 了 す る †。 こ の 過 程 を
PFフ 。G
と 表 現 し,n回 以 下 の 導 出 ス テ ッ プ でSLD (LinearresolutionwithSelectionfunction forDefiniteclause)導 出 を用 い て,PがGを 導 出 で き る と い う。 こ こ に,Pは 入 力 節C、,
C2,… …,C。 を 含 むPrologプ ロ グ ラ ム で あ る 。
こ の と き,Gに 含 ま れ る 各 変 数 に 対 し て, 代 入 の 合 成elBnを 施 す と,通 常 の 手 続 き プ ロ グ ラ ム で の 出 力(解 答)を 得 る こ と
が で き る 。 伍 の 説 明 ・終 り)
上 述 のiの 説 明 で は そ れ ほ ど明 確 で は な か っ た と 思 わ れ る が,Gi+、 の 形 か ら,(B、,
… …,Bq)B,+1つ ま りB1θ1+1,… …,.,+1 の 実 行 が す べ て 成 功 し て か ら,Gi内 のA2が
† プ ロ グ ラ ム 節C,+、 がG。,G、,… …,Giに 現 わ れ る 変 数 を含 ん で い て は ユ ニ ィ フ ィ ケ ー シ ョ ン に と っ て 都 合 が 悪 い 。 元 来,同 じ変 数 名 で あ っ て も異 な る 節 に あ る 変 数 同 志 は 相 異 な る も の で あ る か ら。 こ の た め,プ ロ グ ラ ム 中 の 異 な る 確 定 節 に あ る 変 数 は 異 な る 変 数 名 を 付 け て お く とい う約 束 の 下 で,Gi中 の 変 数 にiを 添 字 す れ ば よ い 。 こ の 変 名 過 程 を 別 々 に標 準 化 す る(standardize)と い う。 ま た,G。,G、,… …,G.を 得 る 過 程 で 用 い ら れ た プ ロ グ ラ ム 節C、,C2,… …,C。 を 入 力 節(inputclause)と い う 。
実 行 さ れ る こ と が わ か る 。Gi内 のA、 は, (B、,… …,Bq)Bi+、 の 実 行 が す べ て 成 功 し た と き に 成 功 し,次 のA2の 実 行 に 移 る 。以 下 同 様 に,A、 か らAkの 実 行 が す べ て 成 功 す れ ば,G,は 成 功 し た こ と に な る 。
い う ま で も な く,C,+、 と し て 事 実 節 が 選 択 さ れ る と,Gi+、 の 体 部 の サ ブ ゴ ー ル の 数 はGi よ り1つ だ け 減 る 。 こ の よ う に し て,G(=
G。)が 最 終 的 に,空 節G。 に 到 達 可 能 な 場 合 が あ る こ とが わ か る 。
(iii)な ん らか の 理 由 に よ り,G,+、 の 体 部 の 先 頭 に あ るB、Bi+、 の 実 行 に 失 敗 す る と,ゴ ー ルG用 の 実 行 は 失 敗 し た と し て
,G,に 戻 り,A、 を 再 実 行 す る 。 こ の こ と を 後 戻 り
(backtrack)と い う。
A、 の 再 実 行 と は,A、 と ユ ニ ィ フ ァ イ 可 能 な 頭 部 を 持 つ 別 の プ ロ グ ラ ム 節C,+、 を 選 択 し,iと 同 様 な 操 作 を 繰 り返 す こ と を い う。
後 戻 り は,A、 と ユ ニ ィ フ ァ イ 可 能 な 頭 部 を も っ プ ロ グ ラ ム 節 が な くな る ま で 続 くが,な く な る とA1の 実 行 は 失 敗 し,後 戻 り は さ ら に Giか らG1.、 に 伝 播 し て い く。
(iiiの 説 明 ・終 り) こ の と き,以 下 で 定 義 さ れ るSLD木(SLD
‑tree)を 縦 型 に 探 索 し て い る こ と に な り ,ゴ ー ル 節 の 最 左 サ ブ ゴ ー ル と ユ ニ ィ フ ァ イ 可 能 な 頭 部 を 持 つ 入 力 節 の 選 択 順 番 はPrologプ ロ グ ラ ムP内 で の 順 番 で あ る 。
SLD‑treeの 定 義
PをPrologプ ロ グ ラ ム,Gを ゴ ー ル 節 と す る。PU{G}に 対 す るSLD木Tは 次 の よ う に定 義 され る。
(1)Tの 根(root)は 目標 節 で あ る。
(2)T内 の全 節 点 は そ れ ぞ れ の 導 出 に よ り導 か れ る 目標 節 を示 して い る。T内 の 節 点 C(目 標 節)が 子 と して のk個 の 目標 節 を も つ の はC内 の,計 算 規 則 に よ って 選 択 され た
原 子 式 とユ ニ ィ フ ァイ可 能 な プ ロ グ ラ ム節 が P内 にk個 存 在 す る場 合 で あ る。k=0の 場 合,Cを 失 敗 点(failurenode)と い う。 ま
た,Cが 空 節 で あ る と き,Cを 成 功 点(success
node)と い う。 口
なお,次 の定 義 に も注 意 して お く。
PU{G}のSLD木Tの,根 か ら葉 †ま で の 節 点 と枝 の系 列 を路(path)と い う。 葉 が 成 功 点 の と き,根 か ら この葉 まで の路 を成 功 路 とい い,葉 が 失 敗 点 の と き,失 敗 路 とい う。
路 内 の 節 点 数 が 有 限 で あ る と き,こ の路 を有 限路 とい い,無 限 数 の節 点 を含 む と き,無 限 路 とい う。 有 限 路 は成 功 路 か 失 敗 路 の い ず れ か で あ る。 成 功 路 がm個 あ る場 合 はGの 解 が
m個 あ る こ と にな る。 □
従 っ て,ゴ ー ル 節G1内 の サ ブ ゴ ー ルA、 の 実 行 に一 度 成 功 した と して も,そ の後 の サ ブ ゴ ー ルA2な ど の 実 行 結 果 に よ り後 戻 りが 発 生 し,A、 が 再 実 行 さ れ,最 終 的 に再 実 行 が 失 敗 す る こ と もあ る。
(iv)以 上,逐 次 型 コ ン ピ ュ ー タ 上 で の Prologの 基 本 計 算 機 構(SLD導 出 に基 づ く 演繹 的 推 論 法)を 整 理 す る と,次 の よ う にな る。
(iv、)プ ロ グ ラ ム節 の選 択(呼 び 出 し)は プ ロ グ ラ ム節 の頭 部 との ユ ニ ィ フ ィ ケー シ ョ ン に よ り行 わ れ る。
(iv2)後 戻 りが発 生 す る と,プ ロ グ ラ ム節 の 再 選 択 が 自動 的 に行 わ れ る。
逐 次 処 理 形 コ ン ピ ュー タ上 で,Prologプ ロ グ ラ ム を実 行 す る こ とか ら,更 に具体 的 に指 摘 す れ ば,iv3,iv4の よ うに な る。
(iv3)プ ロ グ ラ ム節 の選 択 は,プ ロ グ ラ ム 作 成 者 が 記 述 した順 に一 つ ず つ行 う。
(iv4)ゴ ール 節 の体 部 に あ るサ ブ ゴー ル は 左 か ら右 に一 つず つ実 行 す る。
† 子 を もた な い 節 点 を 葉(1eaf)と い う。
3.人 工 知 能 ωの 定 義
人 工 知 能(artificialintelligence)と は ヒ ト と 同 様 な 知 能 の 働 き を コ ン ピ ュ ー タ ・プ ロ グ ラ ム で 実 現 す る こ と で あ る。
初 期 の 人 工 知 能 に お い て は,人 工 知 能 に よ る 問 題 解 決(problem‑solving)は 次 の よ う に 定 義 さ れ て い た αの。
5つ の 概 念
S:状 態 空 間A:オ ペ レ ー タ 集 合 f:状 態 遷 移 関 数s1:初 期 状 態 Sg:目 標 状 態
を 導 入 す る 。状 態s∈Sは オ ペ レ ー タa∈A が 適 用 さ れ る と,
f(s,a)ES
と い う状 態 に 遷 移 す る。初 期 状 態Siに 与 え ら れ た 問 題 を 反 映 させ,s茸 か ら 出 発 し,オ ペ レ タakの 列a、,a2,… …,anを こ の 順 に 次 々 と適 用 し,最 終 状 態Sgが 得 ら れ る過 程 に こ の 問 題 の 解 が 反 映 さ れ る と 考 え る 訳 で あ る 。
2つ の 集 合S,Aお よ び 定 義 域S×A(S とAと の 直 積 集 合)か ら値 域Sへ の 部 分 関 数
(定 義 域 内 の あ り と あ ら ゆ る 要 素 に 対 し,そ の 値 域 の 要 素 が 対 応 す る と は 限 ら な い 関 数)'
fSxA‑一>S
更 に,Sの2つ の 要 素s1,Sgを 付 加 し て 得 ら れ る5つ 組
GS,A,f,s,,sg>
を 問 題 の 表 現 と い う 。 ま た,与 え ら れ た 問 題 に 対 し,
Sg=f(f(・ ・・…(f(f(Si,a1), a2),・ ・…,a。 一、),a。)
と な る よ う なAの 要 素a、,a2,… …a。 一、, a。 を 求 め る こ と を,そ の 問 題 の 問 題 解 決 と い う 。fの 構 造 を 決 定 し な が ら,オ ペ レ ー タ の 列a、,… …,a。 を 探 索 す る の が 推 論 の 働 き で あ り,S,Aが 問 題 解 決 の た め に 直 接 必 要 と
さ れ る知 識 で あ る。
状 態 空 間Sに は 問題 解 決 の た め に必 要 とさ れ る"事 実"が 反 映 さ れ,オ ペ レー タ 集 合A に は問 題 解 決 の た め に必 要 と され る"規 則"
が 反 映 され て い な けれ ば な らな い。 □ 上 述 の人 工 知 能 的 問 題 解 決 の定 義 に は,5 つ 組<S,A,f,Si,Sg>の 要 素 が 完 全 に は前 も って 与 え られ て い な い場 合 も含 め て い る こ とに注 意 して お かね ば な らな い。
当初 とは異 な り,人 工 知 能 研 究 はS,A, f,Si,Sgの 内 い くつ かが 未 知 で あ る よ うな い わ ゆ るill‑structuredproblemの 解 決 方 法
†へ と移 行 し
,そ れ に伴 っ て,状 態 空 間Sで の 探 索 の効 率 を高 め る た め の 厂 知 識 」 に 関心 が 集 中 し,
「 問 題 解 決 の対 象 とな る領 域 に 関 す る専 門 知 識(expertise)や 与 え られ た 問題 領 域 に お い て よ く 知 ら れ て い る 事 実 的 知 識 (facturalknowledge)の み な らず,問 題 解 決 の た め に ヒ トが も つ 経 験 的 な 知 識 (heuristicknowledge)を 獲 得 し,表 現 し 利 用 す る こ と」
が 研 究 され,次 第 に,知 識 べ 一 ス シ ス テ ム を 構 築 す る基 盤 技 術 の確 保 を 目的 とす る知 識 工 学(knowledgeengineering)が 誕 生 し,現 在
にい た って い る。
さて,知 識 の 記 述 単 位,推 論 の 単 位 を決 め, それ ぞ れ にい か ほ どの情報 を含 ませ るか に依存 して,あ る情 報 処 理 を実 行 す るの に そ の両 単 位 をい くつ組 み 合 わ せ るか が 決 ま る こ とは確 か で あ る。 この よ う に,知 能 の本 質 は記 述 単 位,推 論単 位 個 々 に あ るの で は な く,
記述 単 位 と記 述 単 位,記 述 単 位 と推 論 単 位, 推論 単位 と推 論 単 位
の組 み 合 わ せ に あ る。
な お,あ る状 態sに あ るオ ペ レ ー タaを 適 用 して,他 の 状 態S'に 遷 移 した 際 に,遷 移 前
† 未 知対 象 の 問題 解決 を行 う には,既 知 の対 象 との類推 と,既 知 の対 象 か らの帰納 とを本 来 の演繹 と組み 合 わせ る こ とが 必要 とな る。
後 の 二 つ の 状 態sとs'と の 間 で,何 が 変 化 し て,何 が変 化 しな い か を完 全 に記 述 して お か な い と,
「 一 般 に鳥 は 飛 べ るが
,例 外 として ペ ン ギ ン は飛 べ な い」
とい っ た"例 外 知 識"の 取 り扱 い は原 理 的 に 不 可 能 とな る。 ペ ン ギ ン も飛 べ る とい った 誤 った 推 論 が な され る こ とが あ るの で あ る。 例 外 を如 何 に取 り扱 う か に 関連 した 問題 を知 識 工 学上 の フ レー ム問 題 ⑬ の(frameproblem) とい う。
4.演 繹 知 識 ベ ー ス
以 後,論 理 で 表 現 さ れ た 知 識 を 処 理 す る 人 工 知 能 と し て の 知 能 べ 一 ス シ ス テ ム を 考 察 す る 。 事 実 節 の み を格 納 す る の は デ ー タ ベ ー ス (鉱㈲(database)と 称 せ ら れ て い る が
,知 識 べ 一 ス は 事 実 節 の み な ら ず,規 則 節 を も格 納 し て い る 。 知 識 べ 一 ス の 上 位 に あ る の が 事 実 節,規 則 節 の み な ら ず,こ の 両 知 識 を使 う た め の 知 識(メ タ 知 識)を も 格 納 し て い る メ タ 知 識 ベ ー ス(meta‑knowledgebase)で
あ る 。 デ ー タ ベ ー ス,知 識 ベ ー ス,メ タ 知 識 べ 一 ス の 知 識 処 理 機 構(推 論 エ ン ジ ン)は 各 々,
検 索 機 構,推 論 機 構,メ タ 推 論 機 構 と 呼 ば れ る もの で あ る 。
さ て,本 論 に 戻 ろ う。
演 繹 知 識 ベ ー ス(deductiveknowledge
base)DKBは,事 実 節 の 集 合 を 格 納 す る外 延 知 識 べ 一 ス(extensionalknowledgebase)
EKBと,規 則 節 の 集 合 を 格 納 す る 内 包 知 識 べ 一 ス(intensionalknowledgebase)IKBと
の 和 集 合 で あ る:
DKB=EKBUIKB,whereEKB(1 1KB=φ(emptyset).口
DKBに 対 す る 問 合 せ の 一 例 は,x、 ,x2,
… …,x。 を 自 由 変 数 † とす る 一 階 の 述 語 論 理 に お け る原 子 論 理 式
A(x1,x2,… …,Xn) を 用 い,
?‑A(x1,x2,… …,Xn).
で 記 述 さ れ る 。 こ の 間 合 せ の 解 はCiを 個 体 定 数 ま た は 具 象 項(groundterm;一 つ も変 数 を 含 ま な い 項),ト を 証 明 可 能 性 を 表 わ す 記 号 と し て,
DKBト 〔A(C1,… …,Cn).〕
で あ る よ う なc、,… …,c。 のn組 の 集 合 で あ る 。A(c、,… …,c。)は 変 数 を 一 つ も含 ま な い 原 子 論 理 式 で あ り,具 象 原 子 論 理 式 (groundatomicformula),具 象 原 子 式,具 象 ア トム と い わ れ る も の で あ る 。
論 理 式 が 閉 じ て い る(closed)と は この 論 理 式 が 自 由 変 数 を 一 つ も含 ま な い こ と を い うが, 一 般 に,閉 じ た 論 理 式(closedwe11‑formed formula)で 原 子 論 理 式 の 連 言 で 表 わ さ れ た Eと,一 つ の 閉 じ た 原 子 論 理 式Fが 与 え ら れ た 時,
DKBU{E.}ト{F.}
は 次 の もの と等 価 で あ る:
DKBト 〔F:‑E.〕 口
よ っ て,F:‑E.が 成 立 す る か ど う か を DKBに 問 い 合 わ せ る 代 りに,E.をDKBに 加 え,
DKB'=DKBU{E,}
を 新 し い 演 繹 知 識 べ 一 ス と し て 採 用 し,
?‑F.
をDKB'に 問 い 合 わ せ れ ば よ い 。
† 存 在 作 用 素(existentialquantifier)ヨx,全 称 作 用 素(㎜Liversalquantifier)∀xを 併 せ て 限 定 作 用 素(quantifier)と い う が,こ の よ う なxを 限 定 作 用 素 に よ り束 縛(bind)さ れ て い る と い い,束 縛 変 数(bound variable)と 称 す る 。 ま た,ど の 限 定 作 用 素 に よ っ て も束 縛 さ れ て い な い 変 数 を 自 由 変 数(freevariable)と い う。
目標 節Gと し て,Bjを 原 子 論 理 式 と し て, DDBに,
G… …?‑B1,… …,Bn.
が 与 え ら れ た 場 合,B、,… …,B.に 含 ま れ て い る 自 由 変 数 を
X1,X2,'° °…,Xm とす る と,
ヨx1ヨx2… 一 ヨxmBIAB2A… …A B洫
(B、 か つB2か つ … … か つB。 を 真 に す る X、,X2,… …,Xmの 値 が 少 な く と も一 つ 存 在 す る)
を 満 た すx1,x2,… …,Xmの 値 がDKBの 出 力 す る解 答 で あ る 。
さ て,目 標 節GとDKBと が 与 え ら れ た と き,演 繹 知 識 べ 一 スDKBの 処 理 系eva1に よ っ て 与 え ら れ る そ の 解Ansを
Ans:=eval(G,DKB) と表 わ そ う 。
今,IKBに 対 す る 確 定 節 変 換 †(definite clausetransformation)dctを 考 え,dctは 一
つ の 目 標 節Gに 関 し,
IKB':=dct(G,IKB)か っ eval(G,IKB'UEKB)=eval(G,IKBU
EKB)
を 満 た す と し よ う 。こ の と き,確 定 節 変 換dct を 用 い た 問 合 せ 処 理 は 次 の2つ の 段 階 に 分 け て,次 の 様 に行 な わ れ て よ い:
(i)IKB':=dct(G,IKB) (ii)Ans:=eva1(G,IKB'UEKB)
口 今,確 定 節Eの 大 き さsize(E)と し て Reynoldsの 定 義 ⑳ を 採 用 し て
size(E)=[Eに 含 ま れ る(区 切 り記 号 を 除 い た)記 号 の 出 現 回 数 か らEに 含 まれ る 異 な る変 数 の 個 数 を差 し 引 い た も の]
と し よ う。
(i)size(E)=0と な る 確 定 節Eは E=?一.(空 節)
(ll)(頭 部 へ の,サ イ ズ が1の ア トム ††の 付 加)A(x、,… …,x。)を 相 異 な るn個 の 変 数X、,… …,X.を も つ 原 子 論 理 式 と し て,
Is>n
こ の 確 定 節Eの サ イ ズ はsize(E)=1.
(iii)あ る 一 階 述 語 論 理 で の 言 語Lを 選 定 す る 。 確 定 節Aを
A=(E:‑F.) とす る 。 こ こ に,
Eは 空 ま た は,一 つ の ア トム
Fは 空 ま た は,ア トム の 有 限 集 合{F1, F2,… …}
E,Fの 元 は 言 語Lか ら任 意 に 選 ん だ ア ト ム 。
(iii‑1)(二 つ の 変 数 の 単 一 化)
Aに 出 現 す る 変 数 の う ち 二 つ の 相 異 な る 変 数 をx1,X」 と し て,A内 のXiの 出 現 箇 所 の す べ て の 出 現 箇 所 をXjで お き か え た も の をB
と す る と,
size(A)=m‑n(m,nは 各 々 記 号 の 出 現 回 数,相 異 な る 変 数 の 個 数;以 下 同 様) な ら ば
size(B)=m‐(n‑1)=m‐n十1
=size(A)十1 (iii‑2)(変 数,関 数 の 単 一 化)
Aに 出 現 す る 変 数 の う ち 唯 一 の 変 数Xiに 注
† 事 実 節,規 則 節 を あ わ せ て 確 定 節 と い う が,こ こ で の 確 定 節 変 換 は 実 は規 則 節 に 対 す る 変 換 で あ る こ と に 注 意 。
†† 項(定 数,変 数,関 数 な ど),述 語 記 号(ア トム な ど)に 対 し て も確 定 節 と 同 様 な サ イ ズ の 定 義 を考 え て お く。 ち な み に 定 数,変 数 の サ イ ズ は 各 々1,0で あ る 。 ま た,n変 数 関 数 記 号f,n変 数 述 語 記 号Pに 対 し, c、,… …,c。 を 各 々 変 数x、,… …,x。 に代 入 し て 得 られ るf(c、,… …,c。),P(c、,… …,c。)の サ イ ズ は と も にn十1で あ る 。
目 し,A内 のXiの 出 現 箇 所 の す べ て の 出 現 箇 所 を,言 語Lか ら任 意 に選 ん だ 関 数
f(Y1,Y2,… …,Ym)
で お き か え た も の をBと す る 。 こ こ に,Yr, Y2,… …,YmはAに 出 現 し な い 相 異 な る 変 数 で あ る。(iii‑2‑a)A内 で,Xiの 出 現 箇 所 がk個 あ る も の と す る 。
size(f(Y1,… …,Ym))=(m十1)‑
m=1 で あ る。
size(A)=n‐Q とす る と,
Bに 含 ま れ る 記 号 の 出 現 回 数=(n‑k)+
k(m+1)
Bに 含 ま れ る 相 異 な る変 数 の 個 数=(ゑ 一 1)+m
で あ る か ら,
size(B)=(n‑k)十k(m十1)一 〔(を一 1)+m)
=n十km‐Q十1‐m
=size(A)十m(k‑1)十1
変 数Xiの 消 え た 分 (iii‑2‑b)上 述 のaと 異 な り,A内 のXiの 出 現 箇 所 の う ち,唯 一 の 箇 所(す べ て の 箇 所 で は な い)だ け をf(Y、,… …,Ym) で お き か え た とす る と,f(Y1,… …,Ym) で お き か え な い 他 の 箇 所 で 変 数Xiは 残 っ て い る か ら,次 の 等 式 が 成 立 し て い る:
size(B)=size(A)
(iii‑3)(体 部 へ の 追 加)
Aの 体 部 に 言 語Lか ら任 意 に 選 ん だ 一 つ の ア トムG(Z、,Z2,… …,Z。)を 付 加 し た も の をBと す る:B=(E:‑F,G.)
こ こ に,Z、,Z2,… …,ZnはE,Fに 出 現 し な い 変 数 の 集 ま りで あ る 。
size(G)=(n十1)‐n=1 で あ り,
size(A)=m‐Q と す る と,
size(B)=(m十n十1)一(ゑ 十n)
=m‑2+(n+1)‑n
=size(A)十size(G)=size(A)十1 . 口 備 考:上 述 のi,iiを 合 併 し た 操 作,即 ち A=?一.
な ら ば,
B=E(X1,x2,… …,Xn):一.
と す る操 作(頭 部 へ の 付 加)とiii‑1,iii‑
2,iii‑3な る3つ の 操 作,計4操 作 の 有 限 回 の 適 用 で,任 意 の 確 定 節 論 理 プ ロ グ ラ ム が 構 成 さ れ る こ と がShapiroの 考 え た 精 密 化 演 算 子 ρ。の 意 味 を 考 え れ ば 証 明 さ れ る 。
口 今,確 定 節 の 集 合
{E1,E2,… …,En}
の サ イ ズsize({E1,E2,… …,E。})を size({E1,E2,… …,En})
=Σ
ロ
k=1size(Ek)
と定 義 し よ う。 こ の と き,目 標 節Gに 対 し, eval(G,IKB'UEKB')
=eval(G ,IKBUEKB) こ こ に,
size(IKB')?size(IKB) size(EKB')ssize(EKB)
が 成 立 す る 様 なIKB',EKBノ をG,IKB,EKB の 三 者 の 関 係 か ら決 定 す る こ とが 必 要 と さ れ る 。で き れ ば,IKBノ,EKB'は 与 え ら れ た 目標 節Gに 依 存 し な い で 決 定 す る こ とが 望 ま し い 。
こ の 定 義 に お い て は size(IKB'UEKB'),size(IKBUEKB)
な る 二 つ の 間 の 大 小 関 係 を 問 題 と し て い な い こ と に 注 意 し よ う 。
事 実 節E.∈EKBを 演 繹 知 識 べ 一 スDKB に 取 り込 み た い と し よ う 。 この 際,既 存 の 知 識 べ 一 スDKBと 矛 盾 し な い 新 た な 知 識 を 獲 得 し,同 時 にDKBか ら冗 長 性 を 除 去 し な け れ ば な ら な い 。 こ れ を 同 化(assimilation)と い う 。 同 化 さ れ た 演 繹 知 識 べ 一 スNewDKB を 求 め る に は 次 の4段 階i〜ivが 必 要 とな る 。
(i)(証 明 可 能 性)
DKBトE.
な ら ば,E.はDKBか ら得 ら れ る 定 理 で あ り,新 し い 情 報 で な い か ら,
NewDKB:=DKB.
(ll))(矛 盾 性) DKBU{E.}1‐false
な ら ば,E.はDKBと 矛 盾 し た 知 識 で あ る か ら,
NewDKB:=DKB.
な お,直 感 主 義 論 理 で は,論 理 式Eに 対 し Eornot(E)=true
と 出 来 な い 。E=trueあ る い はnot(E)=true が 証 明 さ れ た と き,Eornot(E)=trueで あ
る 。
DKBに は 確 定 節 の 形 式 で 表 わ さ れ た 知 識 の み あ る か ら,古 典 論 理 を採 用 し て い る 。 つ ま り,E:‑F.はnot(F)orEと 等 価 で あ り,Eornot(E)=trueで あ る と約 束 し て い る 。 従 っ て,
DKBk̀E.(DKBか らEが 証 明 で き な い)
で あ れ ば, DKBF‑not(E.)
と い う 「失 敗 を 否 定 とみ な す 推 論 規 則(nega‑
tionasfailure)」 を 採 用 し て い る 。 こ の 推 論 規 則 は 閉 世 界 仮 説(closedworldassump‑
tion)と も 呼 ば れ,こ の 仮 説 を 導 入 し た こ と に よ り,DKB上 で の 証 明 は 非 単 調 論 理(新 し い 公 理 を追 加 し た と き,以 前 に は成 立 し て い た 定 理 の 集 合 が 減 少 す る 可 能 性 が あ る 論 理)を 採 用 し て い る こ と に な る 。
(iii)(冗 長 性) F.EEKB と し て,
DKB':=DKB‑{F.}
を 想 定 す る 。 DKB'∪{E.}トF.
が 成 立 す る な ら ば,F.は 冗 長 な 知 識 と い う こ と に な り,
NewDKB:=DKB'U{E.}
(iv)(独 立 性) DKBおE.
の 場 合 で,DKBトnot(E)を 認 め た く な い 場 合 はDKBとE.と を 独 立 し た 知 識 と考 え,
NewDKB:=DKBU{E.}
後 章 で は,E.∈EKBが 与 え ら れ た と き, ivの ご と く,NewDKB:=DKBU{E.}と
単 純 に し な い で,DKB=IKBUEKB内 の IKB,EKBに 新 し い 規 則 節,事 実 節 を 追 加 す る な ど し て,IKB,EKB双 方 を 調 整(削 除, 変 更 な ど)し て,NewIKB,NewEKBを
NewDKBI‐E.
が 実 現 さ れ る よ う に求 め, NewDKB:=NewIKBUNewEKB NewDKBトE.
と す る 方 法 を
例 題(上 述 のE.の こ と)か ら の 学 習 (learningfromexamples)
で,Shapiroの モ デ ル 推 論 法 ⑳(帰 納 法)を 適 用 し,実 現 し よ う。 こ の 方 法 は 新 し い 知 識(上 述 のE.の こ と)に 適 合 す る よ う に,既 存 の 演 繹 知 識 ベ ー スDKBを 無 矛 盾 か つ 系 統 的 に 修 正 し て い く過 程 で あ る。 い わ ば,DKB上 の 知 識 調 節(38)(accommodation)過 程 で あ る 。
5.推 論
知 識 べ 一 ス で の 推 論 と は
(i)問 い 合 わ せ に 対 す る 解 を 出 力 す る (ll)新 た な 知 識 を この 知 識 べ 一 ス 上 に 付 加 す る か ど う か を 判 定 し,必 要 な ら ば 付 加 す る 。
(iii)対 象 と し て い る知 識 べ 一 ス 上 で 成 立 し て い る 諸 関 係 と ほ ぼ 類 似 の 関 係 が 今 一 つ の 別 の 知 識 ベ ー ス で 成 立 す る か ど う か を 発 見 し, そ の 実 現 を 図 る
と い う三 つ の 目 的 の た め に な さ れ る 。i,ll, iiiのた め に 各 々,
演 繹 的 推 論(deductiveinference) 帰 納 的 推 論(inductiveinference) 類 推(analogicalreasoning)
が あ る ㈲ 。
(1)演 繹 的 推 論(真 理 保 存 則)
推 論 の す べ て の 段 階 で,真 理 を 保 存 す る 論 法 で あ っ て,第2章 で 説 明 さ れ たRobinson
(1965)の 導 出 原 理(resolutionprinciple)
あ る い はSLD導 出 な ど が こ の 場 合 に あ た る 。 PトnG
はnス テ ヅ プ で 論 理 プ ロ グ ラ ムPか ら 目 標 節 Gが 演 繹 的 推 論 に よ っ て 得 ら れ る の 意 味 で あ る 。 こ のPは 第4章 で の 演 繹 的 知 識 べ 一 ス DKBに あ た る 。
演 繹 的 推 論 の 典 型 な も の と し て 以 下 の 三 段 論 法(syllogism)が あ る 。 この 論 法 は
DKBト(E:‑F)がtrueで あ る と き,
DKBトF.がtrue で あ れ れ ば,
DKBトE.がtrue
で あ る と結 論 す る も の で あ る 。 この と き,E はFの 特 殊 化 さ れ た 知 識 で あ る と考 え られ る 。
(II)帰 納 的 推 論(虚 偽 保 存 則)
推 論 の す べ て の 段 階 で,虚 偽 を 保 存 す る 論 法 で あ り,Shapiro(1981,1982)の モ デ ル 推 論 法(modelinferencemethod)が 代 表 的 で あ り,知 識 の 調 節 に 関 連 づ け て 次 章 で 説 明 さ れ る が,演 繹 的 推 論 に お け る 三 段 論 法 と対 応
し て,簡 単 に 説 明 し よ う 。
DKBト(E:‑F.)がtrueで あ る とす る 。 こ の と ぎ,
DKBトE.がfalse で あ れ ば,
DKBトF.がfalse
で あ る と結 論 す る の が 帰 納 的 推 論 で あ る 。 この と き,FはEの 一 般 化 さ れ た 知 識 で あ る と考 え られ る 。
(皿)類 推
構 造,機 能,そ れ か ら得 ら れ る 結 論 な どが よ く知 られ て い る 一 つ の シ ス テ ム と,今 一 つ 別 の シ ス テ ム が あ っ た 場 合,前 者 の 既 知 シ ス テ ム で 知 られ て い る 諸 関 係 を後 者 の 未 知 シ ス
テ ム に 適 用 し,末 知 シ ス テ ム に 関 す る 知 識 を 得 る 論 法 で あ る 。
二 つ の 演 繹 的 知 識 べ 一 スDKB、,DKB2を 調 べ て 以 下 の,原 子 論 理 式Ajの 有 限 集 合
W={A1,A2,… …,An}
と,二 つ の 代 入 θ、,e2の 対 θ=〈Bl,亀 〉
が 発 見 で き た と す る:
DKB、 上 で,Ajθ 、∈EKB1,j=1〜n が 成 り立 ち,さ ら に,
DKB2上 で,A擁 ∈EKB2,j=1〜n が 成 り立 ち,し か も
lyjel^,A」B2,」=1^‑n
で あ る とす る 。 〜 は1対1の 対 応 関 係 を 表 わ し て い る 。
こ こ に,x、,… …,XmをW中 に 現 わ れ る 変 数 と す る と,
el={X1/t1,X2/t2,… …,Xm/tm}
BZ={X1/t/1,X2/t/2,… …,Xm/t/m}
で あ り,
tjとt'」(j=1〜m)は1対1の 項 関 係 に あ り,同 一 視 さ れ た 項 の 対 を 表 わ す:
さ て,類 推 と は 一 般 に,類 似 し た 前 提 が 成 立 し て い る と き に,類 似 し た 結 論 が 成 立 す る
と推 論 す る こ と で あ る か ら, あ る 確 定 節Eに 関 し,
DKBII‑EBI.
が 成 立 し て い る と き に, DKB2トEel.
が 成 立 し て い る と推 論 す る の が 類 推 の 働 き で あ る 。
実 際 に,DKB2トE亀 が 証 明 さ れ れ ば,こ の 類 推 が 正 し か っ た こ と に な り,証 明 が 不 可 能 で あ る こ と が わ か れ ば 間 違 っ た 類 推 が な さ れ た こ と に な る 。
6.演 繹 知 識 ベ ー ス 上 の 知 識 の 調 節
観 測 文 α と そ の 真 偽V(=trueあ る い は
false)と か ら成 る事 実<α,V>の 集 合 に適 合
す る よ う に,既 存 の 演 繹 知 識 べ 一 スDKBを
無 矛 盾 か つ 系 統 的 に修 正 して い く過 程 す な わ ち,知 識 の 調 節(39)過 程 を,帰 納 的推 論 法 の代 表 的 と も考 え られ るE.Y.Shapiroの
InductiveInferenceofTheoriesFrom
Facts⑬ η(事 実 に よ る理 論 の 帰 納 的 推 論) を原 理 的 に適 用 し,実 現 し よ う。
本 手 法 がShapiroの 方 法 と異 な る 諸 点 は 次 の よ うに指 摘 され る:
(a)DKBを 論 理 プ ロ グ ラ ム とみ な し,確 定 節 の 集 ま り と した こ とに よ り,導 出原 理, 精 密 化,矛 盾 点 追 跡 の実 施 が 簡 単 に行 え る よ
う に な った こ と
(b)精 密 化 に お い て い わ ゆ る最 汎 ア トム を使 わ な い こ と
(c)上 述 のbか ら もた らされ る必 然 と し て,サ イ ズ を一 つず つ増 加 させ る形 で 知 識 の 調 節 を行 なわ な くて,
ヱ
L(k)か らL(k十u)(u≧1)へ
ぬ め
の 移 行 で 行 な う こ と
(d)導 出 原 理 と矛 盾 点 追 跡 過 程 と の 間 の 密 接 な 関 係 を と ら え,矛 盾 点 追 跡 を 導 出 原 理
の 逆 に 帰 着 さ せ た こ と 囗
6.1モ デ ル 推 論 シ ス テ ムMISとh従 順 な モ デ ルM
観 測 文 α は 観 測 言 語(observationallan・
guage)L。 で 表 わ さ れ,演 繹 知 識 べ 一 スDKB 上 の 確 定 節(事 実 節,規 則 節)は 仮 説 言 語
(hypothesislanguage)Lhで 表 現 さ れ る 。仮 説 と はLhの 文 の こ と で あ る 。
言 語Lと し て,一 階 述 語 論 理 言 語 が 選 ば れ て い る と す る 。
こ の と き,空 文 を 口,あ る い は?一 ・で 表 わ す と す れ ば,
ELocL,,CL
が 成 立 し て い る 。L。,Lhと し て L。:Lの グ ラ ン ド ア トム(gromdatom)
(変 数 を含 ま な い ア トム つ ま り変 数
を含 ま な い原 子 論 理 式)の 集 合 Lh:Lの 確 定 節 の 集 合
を選 定 す る と,こ の対<L。,Lh>は 次 の 意 味 で 許 容 的 で あ る こ とが 証 明 さ れ る ⑳:現 在 の DKB(⊂Lh)か ら導 出 され る観 測 文 α ∈L。
の 集 合 が モ デル †Mに お い て真 な る観 測 文 全 体 の 集 合 と一 致 す る と き,現 在 のDKBがM
で 真 で あ る よ うな対 〈L。,Lh>は 許 容 的 (admissible)で あ る とい う。 □
観 測 文 α の 真 偽 を 回答 可 能 な容 体 を モ デ ルMに 対 す る神 託(oracle)と い い,そ の よ う な神 の存 在 を仮 定 す る。 神 託 に入 力 を与 え, そ の答 を読 む 操 作 をMに お け る実 験(experi・
ment)と 呼 ぶ 。 実 験 の結 果 を記 述 した の も を モ デ ルMに つ い て の事 実F,と い い,観 測 文 α
と そ の 真 偽Vと の 対 で 表 す:Fi=<α, v>,こ こに,iは 提 示 され た 観 測 文 の番 号
(=1,2,… …)で,V={true,false}
口 さて,モ デルMに つ い て の事 実 の無 限列 F、,F2,… …
で,L。 に属 す る任 意 の α が あ るFiに 現 わ れ る もの を モ デ ルMの 枚 挙 とい う。
モ デ ル推 論 シ ス テ ム(modelinferencesys・
tem)MISと は,モ デ ルMの 枚 挙 を 読 み 込 み,推 測(conjecture)と し て の仮 説 言 語Lh の文 の 有 限 集 合DKBを 出 力 す る もの で あ る。
確 定 節(文)の 集 合DKBは モ デ ルMのL。
完 全 公 理 化 で な けれ ば な らな い 。 つ ま り, MISは モ デ ルMに つ い て 有 限 個 の 事 実 を確 か め,間 違 っ た推 測 を有 限 回行 っ た後,そ れ まで に読 み込 ん だ真 な る観 測 文 を含 め全 て の 真 な る観 測 文 ∈L。 を導 くよ うな 真 な る仮 説 の集 合 ⊂Lhに,DKBは 一 致 しな けれ ばな ら な い。
有 限 個 の 真 な る観 測 文 を除 き,そ の他 の(第 n番 目の)真 な る観 測 文 を導 出 す る 導 出 回 数 の 最 小 数 が
† モ デ ルMと は 言 語Lの 各 グ ラ ン ドア トム に 対 し,trueま た はfalseを 割 り当 て る 写 像 の こ とで あ る 。
h(n)(全 域 的 な 帰 納 的 関 数 †hの,nと い う変 数 値 に対 す る 値)
以 下 で あ る よ う な 仮 説 の 有 限 集 合 がL。 完 全 公 理 化 と し て 存 在 す る よ う な モ デ ルMをh従 順 な モ デ ル と い う。
MISが 正 し い 推 測 を い つ か 出 力 で き る た め に は,モ デ ルMは
hを あ る 全 域 的 な 帰 納 的 関 数 と し て,あ る サ イ ズk>0に 対 し てh従 順 な も の で な け れ ば な ら な い 。MISは そ の よ う な 最 小 のkをk。 と す れ ば,そ の 帰 納 的 学 習 の 下 で, kを 増 加 し つ つkoに 到 達 さ せ る こ と に な る 。
(例1)二 つ の 非 負 整 数 が 与 え ら れ た 場 合, 加 算 の 機 能 を も つDKBを モ デ ル 推 論 シ ス テ ムMISに 推 測 さ せ よ う 。
下 記 のi,llの 導 入 の 下 で,iiiを 与 え る と, ivを 出 力 す る の がMISの 役 割 で あ る 。
(i)議 論 領 域(対 象 とす る 世 界 の な か の 全 て の 個 体 の 集 合)D:非 負 整 数 の 集 合
(ll)一 階 言 語L:
0,1,2,3,… … 非 負 整 数 の 集 合 add1(X)Xの 後 続 要 素X十1を 返 す
関 数
plus(X,Y,Z)Z=X十Yな る
関 係 の 下 に の み 真 と な る 述 語 (iii)事 実 の 例(MISへ の 入 力)
<plus(0,0,0),trued
<plus(0,1,2),falser
(iv)理 論(正 し い 推 論)T(MISか ら の 出 力)
plus(X,0,X):‐.
plus(X,addl(Y),addl(Z)):‐plus (X,Y,Z),
6.2MISで の モ デ ル 推 論 ア ル ゴ リ ズ ム 言 語Lの 二 つ の 文P,qを 考 え た と き,
Pトq・(Pがqを 導 く こ と)
カ〉つsize(P)≦size(q)
で あ れ ば,qはPの 精 密 化(refinement)で あ る と い う 。 ま た,Lm(k)と は,マ ー ク
ア
付 け(marking)mの 下 で,"false"と マ ー ク さ れ て い な い 仮 説Hを 精 密 化 文 と し て も つ そ れ 以 前 の 全 て の 仮 説(こ の 仮 説 に 何 回 か 演 算 子 ρ を 適 用 す る とHが 得 ら れ な け れ ば な ら な い)が"false"と マ ー ク さ れ て い る よ う な,サ イ ズk以 下 の こ の よ う なH(マ ー ク 付 mの 下 で の ソ ー ス 文)の 全 て の 集 合 を 指 す 。 こ こ に,ρ は 精 密 化 演 算 子 と い わ れ る も の で,
ρ(P)=〔pの 精 密 化 の全 体 か ら成 る 集 合 〕=
{qIpトq,Size(P)≦size(q)}
を 表 わ し,Lm(k)は 精 密 化 演 算 子 と し て
ア
ρ を採 用 した条 件 の下 で の,サ イ ズ がk以 下 の マ ー ク付 けmの ソー ス 集 合 とい わ れ る。
マ ー ク付 けmは"false"と マ ー ク され た任 意 のqと,qを 精 密 化 と して もつ 任 意 のP∈
Lh(こ のPに 何 回 か ρ を適 用 す る とqが 得 ら れ な け れ ば な ら な い)と に 対 し,Pも
"false"と マー ク さ れ て い な け れ ば な らな い とい う意 味 で,矛 盾 して い な い こ とが 必 要 で あ り,更 に,"false"と マ ー ク さ れ た任 意 の 文 Pが モ デ ルMで 偽 で な けれ ば な らな い。 この 両 条 件 が満 た され た マ ー ク付 けmは モ デ ルM
と矛 盾 しな い と称 せ られ るが,当 然 なが ら こ れ を仮 定 す る。
以 下 のモ デル 推 論 ア ル ゴ リズ ム にお い て は, 仮 説 は,モ デルMで 偽 な る観 測 文 を導 出す る
ときMに 関 して強 過 ぎ る とい わ れ,ま た,モ デ ルMで 真 な る観 測 文 を 導 出 で きな い ときM
に関 して 弱 過 ぎ る とい わ れ て い る。
モ デ ル 推 論 ア ル ゴ リ ズ ム(modelinference algorithm)
initialization
Sf。i,e={空 文 口}
† 変 数 の 全 て の 値 に 対 し,値 が 定 ま る 関 数 を 全 域 的 と い 鯵,全 域 的 な 帰 納 的 関 数(totalrecursivefunction) とは コ ン ピ ュ ー タ で そ の 関 数 値 が 計 算 され 得 る もの で あ る こ とが 証 明 さ れ て い る。
Strue={}
サ イ ズk以 下 の 仮 説 の 集 合DKBをLm
あ
(k)と し て 初 期 化 す る†。k=0の 場 合,
LmAo(k)={空 文}と し て,こ の 空 文 に falseと マ ー ク す る 。
repeat
1.次 の 事 実F。(モ デ ルMの 枚 挙 内 の 第n 番 目 の 事 実)=<α,V>を 読 み,α を
St,ueま た はSr、1seに 追 加 す る 。 repeat
'2.1stwhile(推 測Tが 強 過 ぎ る)do falseと マ ー ク 付 け さ れ て い な い 仮 説 の 集 合(=Lm(k))にあ よ り,下 記 の よ う に"false"に 属 す る α(Sf。i、eの元) を 導 出 し て み る 。
3.あ るfalseに 属 す る α がn回 以 内 の 導 出 で 真 と 導 け て し ま っ た 時
例 外:n回 の 導 出 で 導 け な い と き 導 出 打 切(真 と 導 け な い 扱 い)
contradictionbacktracingalgorithm 矛 盾 点 の 追 跡(誤 っ た 仮 説 の 摘 出)
矛 盾 点 追 跡 に よ り上 記 の 導 出 で 用 い た 仮 説 の あ る も の がfalseと マ ー ク さ れ る。
現在 のL(k)か
のら枚 挙 と実 験 に よ り
no m,
次 のL(k+u)(u≧1)を 生 成 す る
Po
こ と。
falseと マ ー ク 付 け され た あ る仮 説 の 精 密 化 で,全 て の,真 に属 す る αiがh(i) 回以 内 の導 出 回数 で真 と導 出 で きれ ば成 功 で,そ うで な け れ ば失 敗 で あ る。
そ れ ま で はfalseと マ ー ク 付 け さ れ た 他 の 仮 説 の 精 密 化 を 試 み 繰 り返 し,全 て を 精 密 化 し て も 失 敗 す れ ば,k:=k+u
(u≧1)と し て,4を や り直 す 。
㎜ti1
6.上 記2,4の ど ち ら のwhileに も入 ら な く な る 迄 繰 り返 す 。
7.強 過 ぎ る こ と も な く弱 過 ぎ る こ と も な い 時 点 で,Lm(k)をDKBと し て 出 力 す る1へ 戻 る 。
forever
6.3contradictionbacktracingalgo‑
rithm(矛 盾 点 追 跡 ア ル ゴ リズ ム)
前 節6.2で の モ デ ル 推 論 ア ル ゴ リ ズ ム で 登 場 し たcontradictionbacktracingalgor‑
it㎞ が 記 述 さ れ る 。
全 て のfalseに 属 す る α がn回 以 内 の 導 出 で 導 け な く な る 迄,3を 繰 り返 す 。 4.2ndwhile(推 測Tが 弱 過 ぎ る)do
falseと マ ー ク 付 け さ れ て い な い 仮 説 の
m
集 合L(k)に よ りtrueに 属 す る あ る α1(St,u。 に 属 す るF,の α)が 真 とh(i) 回 以 内 の 導 出 回 数 で 導 け な か っ た と き。
5.falseと マ ー ク 付 け さ れ た あ る 仮 説 を 取 り出 し,精 密 化(古 い 仮 説 の 局 所 的 修 正) を 試 み る 。
refinementalgorithm:精 密 化
contradictionbacktracingalgorithm
前 提1.falseと マ ー ク 付 け さ れ て い な い m
仮 説 の 集 合L(k)に よ りfalseに 属 す る あ る α ∈Sf。1,eがn回 以 内 の 導 出 で 真
と導 け て し ま っ た 。 手 順
導 出(SLD導 出)の 際,作 ら れ る次 の 性 質 を 持 つ 文 の 順 序 付 き2分 木(ordered binarytree)を ゴ ー ル ヒ ス ト リ(goalhis‑
tory)と 呼 ぶ こ と に す る 。 (1)根 は 空 文 で あ る 。
†DKBが 空 で な い 場 合 はinitializationを 必 要 と し な い が,こ の 場 合 は,DKB内 の 確 定 節 の サ イ ズ の 最 大 値 をkと し て,DKBをLm(k)と し て 初 期 化 し,以 下 のrepeatか ら 実 行 す れ ば よ い 。
(2)全 て の 葉 は 仮 説(Lm(k)の 元) ま た は モ デ ルMでtrueな る 観 測 文 で あ り,ど の 葉 も 変 数 を 共 有 し な い 。 (3)葉 で な い 節 点 は 全 て,前 の ゴ ー ル 節
(左 成 分 †)と 導 出 に 使 わ れ た 確 定 節(右 成 分 †)の2分 導 出 形 †で あ る 。 □ 観 測 文?m.の 導 出 木(成 功 し たmifica‑
tion歴)をFig.1と す る と ゴ ー ル ヒ ス ト リ は Fig.2に 示 さ れ る 如 く,導 出 木 の 逆 順 と な る。
この ア ル ゴ リ ズ ム は,ゴ ー ル ヒ ス ト リ を た ど り,次 の 手 順 でfalseな る 仮 説(葉 で あ る Nk=HQ.k)を 摘 出 す る 。
1.k=0,N。=2分 木 の 根(=GE)と す る 。
2.現 在 の ゴ ー ル 節Ge.kを 導 出 し た 一 方
Fig.1観 測 文 αの 導 出 木
Fig.2観 測 文 αの ゴ ー ル ヒ ス ト リ
(右成 分)の 確 定 節 の 頭 部 が モ デルMでtrue と判 断 で きれ ば,Nk+、 と し てNkの 左 成 分 を 採 用 す る。(そ の 一 つ 前 の ゴー ル 節G召.k‑1に
ゆ くこ とに な る。)
例 外:一 つ前 の ゴ ー ル節 が 無 く,G。 に ゆ か ね ば な らな い と き,backtrace失 敗 と し て戻 る。
3.前 の2で 確 定 節 の頭 部 が 真 偽 不 明 な ら ば,N、 の 反 例 † †を作 れ る か ど うか を調 べ る。
反 例 の作 成 はGreenの 代 入 収 集 法 ⑳(こ れ まで に使 わ れ た代 入 の合 成 を作 る こ と)に よ る。
prologの 単 一 化 手 続 き と共 有 変 数 の 機 能 に よ り個 々 の 導 出 中 の 代 入 そ の もの は 自動 的 に な さ れ て い る し,ゴ ー ル ヒス トリに保 存 さ れ て い る(変 数 を含 む が)。
† 導 出 の 左 成 分,右 成 分,2分 導 出 形 の 定 義 に つ い て は,付 録 を参 照 。
††'A,Bを ク ラ ン ドア トム{P、,P、,… …,Pk}の 部 分 集 合 と し,モ デ ルMでBが 真 か つAが 偽 で あ る こ と が 判 明 し た と す れ ば,グ ラ ン ド文A←Bは モ デ ルMで 偽 で あ る 。P=A'←B'か つA'θ ⊂A,B'θ ⊂Bな る 文Pと 代 入 θ とが 存 在 し た 場 合,Pθ=(A'←B')θ ⊂A←Bが 成 立 し,こ の 様 なP(グ ラ ン ド文A←Bを 包 摂 す る 文)も モ デ ルMで 偽 で あ る こ と が わ か る 。 こ の と き,A←BはP、,P2,… …,Pkを テ ス ト し た 結 果 に
よ っ て 構 成 さ れ る,代 入 θ に よ るPの 反 例(counterexample)と い う 。
従 っ て,次 の4で 一 旦 値 が 定 ま っ た な ら ば, そ の 後 の 反 例 を 作 る た め に 同 じ代 入 を使 う 必 要 が あ る こ と を ロ ジ ッ ク 化 す る こ と で よ い 。 4.神 託 に 例 示 し て(ホ ー ン節 の 頭 部 の 例 示 で よ い)真 偽 を 問 う(実 験)。 但 し,例 示 に 変 数 が 残 れ ば 真 偽 質 問 前 に 値 を 入 力 し て も ら う 。(最 初 の み 神 託 に 聞 く こ と.)trueな ら, そ の 後 の 処 理 は2と 同 じ。
5.上 記 の2,4に お い て 確 定 節 の 頭 部 が モ デ ルMでfalseの 場 合,Nk+、 と し てNkの 右 成 分 を 採 用 す る 。
6.k:=k十1と し,Nkが 葉 で な け れ ば 2へ 戻 り追 跡 を 続 行 す る 。Nkが 葉 で あ れ ば, そ の 仮 説(=Nk)にfalseと マ ー ク 付 け を し て 戻 る 。
な お,Sf。1,eに 属 す る 全 て の 観 測 文 α がn 回 以 内 の 導 出 で 導 け な くな る 迄 の 繰 り返 し 制 御 は 呼 出 側 で 行 な う 。
6.4導 出 過 程,矛 盾 点 追 跡 過 程 の 間 の 関 係
あ る 観 測 文 α ∈Sf。1,eに 対 し,
m,.̲̲̲m
L(k)ト%nα(α がL(k)か ら
Po
n回 以 下 の 導 出 ス テ ッ プ で 導 け た) で あ る と す る 。 こ の と き,目 標 節Gと し て
G(=Go)=?‑a,
が 設 け ら れ て い る 筈 で あ り,
4≦nと し てGE≦ 口=?一.
で あ る よ う な 目 標 節GEが あ る 。 な ら ば,目 標 節 の 系 列
Go,G1,… …,G,̲1,Gi,… …,
GQ‑1,GQ
と,入 力 節 ∈Lm(k)の 系 列
C1,C2,… …,Ci̲1,Ci,… …,
Ce̲i,Ce
と,代 入 の 系 列
θ、,θ2,… …,9,.、,θ1,… …,BQ‑、,θ ε と,導 出 に 使 わ れ た ア ト ム の 系 列
Q、,Q2,… …,Qi̲、,Qi,… …,
Q￠ 一、,Qe
と が あ る 。 こ こ に,
(i)GQ=口=?一.(空 節)
(ll)C,(i=1〜 ε)はLm(k)内 の 規 則 節,事 実 節 の い ず れ か で あ る 。
(iii)ei(i=1〜 の はmgu(最 汎 単 一 化 作 用 素)で あ る 。
(iv)Qi=(C,の 頭 部)・e,
=(G, 一、の 体 部 の 一 番 左 の ア トム)・6, はGi‑、,C,か ら 代 入Biを 用 い てGiを 導 出 す る の に 用 い ら れ た"導 出 に 使 わ れ た ア トム"
で あ る 。
よ っ て,Fig.3の よ う な 導 出 過 程 の 図 示 が 可 能 で あ る 。
矛 盾 点 追 跡 過 程 はFig.3の 導 出 過 程 を 逆 に た ど り,
C1,C2,… …,Ci̲1,Ci,… …,
CQ‑lfCE
の 内,い ず れ か の プ ロ グ ラ ム 節(規 則 節,事 実 節)がfalseで あ る か を 発 見 す る も の で あ る 。 こ のfalseに な る プ ロ グ ラ ム 節 が 複 数 個 あ る 場 合,falseで あ る 添 字iの 最 も大 な る プ ロ グ ラ ム 節C1を 発 見 す る 。
そ の 発 見 法 は 次 の 通 りで あ る 。
観 測 文G。(=G=?一 α.)か らG￠=
□=?一.を 得 る と き,導 出 に 使 わ れ た ア トム の 系 列
Q、,Q2,… …,Qi̲、,Q,,… …,
Qn‐lsQn
の 真 偽 は 判 明 し て い な い 状 態 の 下 で,導 出 過 程
G。,Q、,Q2,… …,G1̲、,Gi,… …, GE‑i,Qe
は 実 行 さ れ て い る こ と に 注 意 す る 。
(1)Qi・e,=Q1に 注 意 す る 。 何 故 な ら ば,9,・e,=e,で あ り,Q1はB,を す で に 作 用 さ せ て 得 ら れ て い る か ら で あ る 。
Z￠=空 代 入 と し て,QP・BQ・ZQを グ ラ ン ド ア トム に す る 代 入 笏 を神 託 に 聞 き,こ の よ う に し て 得 ら れ た グ ラ ン ドア トム
Pe‑i=Qe・9e・Z￠ ・ne の 真 偽 を 神 託 に 聞 く。
導 出 過 程,矛 盾 点 追 跡 過 程 の 図 示 (1‑1)PQ‑、 がtrueの 場 合,GQ‑、 へ さ か の ぼ る こ と に な り,IIへ 行 く 。
(1‑2)PQ‑、 がfalseの 場 合,Ceが 求 め る"false"で あ る プ ロ グ ラ ム 節 で あ る 。
(II)τ ト1=θ1・ τ1● η1(iま 」2,2‑
1,… …,2),こ こ に,Zeは 空 代 入 で あ り,η2は 上 の1で 求 ま っ て い る,
Fig.3
と し て, P,‑i=Qi・Ti‑i
=Qi・B,・Zi・ 彿
=Qi・ 笥 ・η1
を 考 え る 。 こ こ に,η1はQi・ 笥 を グ ラ ン ドア ト ム に す る 代 入 で あ っ て,神 託 に 聞 け ば 求 ま る 。
(II‑1)P,̲1がtrueな ら ば,こ のIIの 最 初 に 戻 る 。
(II‑2)Pi‑、 がfalseな ら ば,Ciが 求 め る"false"で あ る プ ロ グ ラ ム 節 で あ
る 。 口
6.5refinementalg◎rithm(精 密 化 ア ル ゴ リズ ム)
前 の6.2節 で の モ デ ル 推 論 ア ル ゴ リズ ム で 登 場 し た 精 密 化 ア ル ゴ リ ズ ムrefinement algorit㎞ を 説 明 し よ う。
refinement‑algorithm 前 提
1.falseと マ ー ク 付 け さ れ て い な い 仮 説 の 集 合Lm(k)に よ りtrueに 属 す る あ る
ア
αiがh(i)回 以 内 の 導 出 回 数 で 真 と導 け な か った 。
手 順
ユ
1.L Po(k)か らL角(k十v)(v≧1)
を 生 成 す る た め に 以 下 の 処 理 を す る。falseと マ ー ク 付 け さ れ て い る 仮 説 を 一 つ 選 び,Aと す る 。
2.文A∈Lm(k)に 次 の(1)〜(4)の 操 作
Po
(精 密 化 演 算 子 ρ。を 定 義 し て い る 操 作)を 適 用 す る こ と に よ り,文B∈Lm(k+v)(v≧
Po
1)の 集 合 を生 成 す る。
文Aか ら文Bを 作 る方 法(精 密 化 法)は 第 4章 の 備 考 で 説 明 さ れ て い る の と全 く同 じで あ り,B∈ ρ。(A)が 成 立 して い る。 注 意 す る点 は述 語 や 関 数 に於 て引 数 の な い場 合 が あ る こ とで あ る。引 数 の な い述 語 はtrueま た は falseな る定 数 で あ り,引 数 の な い関 数 は議 論 .領域 内 の定 数 で あ る。
(1)(頭 部 へ の 付 加)
A=空 節 な ら ば,B=(P(x、,x2,
… …,x。):一.)と す る 。 こ こ に,Pは 言 語 Lか ら任 意 に 選 ん だ ア トム で あ る 。
(2)(二 つ の 変 数 の 単 一 化) 第4章 の 備 考 で 指 摘 す るiii‑1 (3)(変 数,関 数 の 単 一 化) 第4章 の 備 考 で 指 摘 す るiii‑2‑a
(4)(体 部 へ の 追 加) 第4章 の 備 考 で 指 摘 す るiii‑3
な お,Shapiroは,上 述 の 精 密 化 演 算 子 ρ。
を 考 え,こ の ρ。が 一 階 言 語Lに 対 し て 完 全 で あ る,す な わ ち,空 文 □ か ら 出 発 し て 任 意 の 推 測 が 有 限 回 の 精 密 化 演 算 子 ρ。の 適 用 で 得
ら れ る こ と を 証 明 し て い る 。
3.上 記 の2よ り得 ら れ た 文Bの 並 べ 方 は 生 成 順 ・サ イ ズ 順 と す る が,以 下 の こ と に 注 意 す る 。
上 記2の 精 密 化 の 操 作(4)に お い て は size(B)‐size(A)=1
が 成 立 し て い る が,も し,Z、,Z2,… …,Z。
がE,Fに 出 現 し て も よ い 変 数 の 集 ま り とす れ ば,
size(B)‐size(A)>1
と な り,こ の 場 合,ア ト ムG=G(Z、,Z2,
… …,Z。)はE:‑F,G.が 既 約 で あ る よ う なE:‑F.に 関 す る 最 汎 ア トム で な け れ ば な ら な い 。
ア トム の 集 合Sは 次 の 条 件 が 成 立 す れ ば 既 約(reduced)で あ る とい う:S・ σ⊆Sな る
代 入 σが 存 在 し な い 。 ロ
ア トムG(Z1,Z2,… …,Zn)に お け る 変 数Z1,Z2,… …,Z。 がE,Fに 出 現 し て
も よ い 変 数 の 集 ま り とす れ ば,GがE:‑F, G.が 既 約 で あ る よ う な 最 汎 ア ト厶(themost generalatom)で あ る とは,
(i)E:‑F.が 既 約 で あ る こ と (ll)Q・ θ=Gか つ(E:‑F.)
θ=(E:‑F.)が 成 立 す る 代 入 θが 存 在 す る任 意 の ア トムQに 対 し
E:‑F,Q.が 既 約 で な い こ と
