博 士（ 情報科学 ）何嵩昊

学 位 論文 題 名Generati
on of a Speci
ficSolve
rf
orEac
hQ
uery‑Answering Problem（ 個 別の 求 解 問題 に 特 化し た ソ ル ノヾ ー の 生成 方 法 ）学 位 論 文 内 容 の要 旨
Inthe real world, pe
opl
edono
tonl
yw
antt
okno
w"yes"or"no"oft
heirquest
ion,bt
itth
ee
xa
ctan
swer
(like, t
he service timeoftherestaurant).Inot
herwords,t
heac
hieve
men
tofth
eded
uctiv
esystemabout
how to solve the Query‑Answering problem (QA problem), which is constituted by the prec
onditionknowledge and the query atom, is an ess
entialprobl
em in the dev
elopment ofthe real Semantic Web.
However, how to e
stablish theeffective solver for solving aconsid
erable argera
ngeQ
Aproblems
has not been clearly decided. The following fundamentalissues need to be addressed:
1. Although conventionalSkolem
izationusedin proof pro
blem always yieldsa sati
sfiabil
ity‑preserving transformation,it does notpreserv
e thelogica
l meaning of as
ourceformula(likeDes
cr
ip‑
tion Logic, or First‑
orderLogic)in the transformation betweendiffere
nt logical expressions, whichis the most essentialreaso
n whythe conventio
nal researches onsolvingQA pr
oblemsare difficul
t tobe improved. In this research, based on the meaning‑preserving Skolemization theory pfoposed byour research group, the skolem function is applied to preserve the logi
cal meaningwhen t
ransformbetweendiffer
ent log
ical expressions.
2. By introducing the skolem function, the real meaning‑preserving transformationhas bee
nrealized, and the real range of the QA problems expressed by FOL has been discovered. Therefore,
how to implement the solver based on the Bottom‑up solution in an efficient way to solve the QA
problems need to be considerd? Also, the correspondent increasing computational complexity byintroducing the skolem functions has to be considerd. Until now, a QA problemsolvi
ng system thatcan correctly deal with the skolemfunction does notexist.In or
der tosolvethe QAprobl
em intheSemantic Web automatically, the implementation of a deductive system for lar
ge range QAproblemswit
h skolem functionsis req
uired.
Thisthesis is constructed asfollows:
In chapter l, the development of the SemanticWeb isintrod
uced.And the importanceof theQA
problem has been discu
ssed.

.

Chapter 2 will hrst formalizesa cla
ss ofQA pro
blems and outlinesa general scheme for solv
ing
them based on the equivalent transformation (ET). Th
en, after describing theproble
ms ofthe conven‑tional research about QA problems, the necessity ofthe theory of mean
ing‑preserving Skolemizationwi
ll beexplai
ned andan ex
tendedclaus
e spacedefin
ed inour re
searc
hg
ro
upwi
llbeintr
odu
ced.More‑over, based onthe notion ofthe representativemodelset,a repr
esent
ati
vemo
dels
etoft
hecollect
ionof all models of an extended claus
e setwill be defined. Fi
nally,the fundamental theory difference
between this researchand previous
ly existing theories willbe described.
Chapter 3will fi
rstlypresent thenew Bot
tom‑upsolut
ion for solving QAproble
ms. Then, some QA― 689―

problem examples willbeused to illustratehow the Bottom‑up solution works.Here,the problemof
the increaseofthe computationalcomplexity by applying theSkolemfunctionsintroduced inchapter
2, willbediscussed.
Chapter4 willintroducetheresearchapproach ofgenerating theSpecificSolverforeachgivenQA
problem.As it hasbeen already discussed in Chapter3,thecomputational complexitywilldramati‑
callyincreasebecauseoftheintroductionoftheskolemfunction. Therefore,inthisresea
rch,foreachgivenQAproblem, we generate thespecific solverbyusingtheknowledge (K, clauseset) acquired
from thegiven QA Problem. Although the generacionofthespecificsolverbyanalyzingr.heQAProb‑lem willcostlittletime,theexecutiontime(Bottom‑upcomputation)for achievingtherepresentativemodelsetisthoughttobeabsolutelyfast,especiallywhenitwillberepeatedlydoneonlybycha
nging
the parameters (wheneverreinitializethe skolem functions). We callthis theQAProblem specificapproach, which is an absolutely novel technology for solving the QA Problems.
InChapter 5,themethodofset
tingv
aluesfortheskolemfunc
tionv
ariablesincludedi
ntheextend
edclause set, which areachievedbyapplying themeaning‑preservingSkolemization theoryinchapter2,willbediscussed.
Chapter6 willintroducetheveryimportantconcept,theSupportSet. Astheknowledg
esear
ching
rangedefinedin thisresearch,themethodabouthow togener
ateitistho
ughtt
obed
irectlyaffectsthe
efficiencyofthewholeQAproblemsolvingprocess.
Chapter7willdescribe howtodigitalizethesupportset.
InChapter8,thedigitalizationoftheextended clausesetandthefinalg
enerationofthesp
ecificsolverwillbedescribed.Furthermore,theefficiency ofthespecificsolverwillbeconfirm
edbyanal‑
izingtheexperiment'sresults.
InCharter9,tlx>resultsobtainedinthisthesisaresummarizedandthe futureworks w
illbedis‑cussed.As apre‑process,thesimplificationof theextended clausesetoftheQAproblembyusing theunfold transformationwillbediscussed.Moreover,thenewgeneration methodfor thesupportsetwill
alsobetalkedabout.

− 690ー

学 位論文審査の要旨
主査
副査
副査
副査

教授
教授
教授
准教授

赤栗
高棟間 清原 正仁
井 昌彰
朝 雅晴

学 位 論 文 題名

Generation ofaSpecific Solver for Each Query‑Answering Problem（ 個別 の 求解 問 題に 特化 し たソ ル バー の 生成 方 法）
質問応 答間 題は、 データ ベース 問い 合わせ などに 見られ る形の 問題であり、ある前提知識のもとで、あ る関係 を満 たすも のをす べて求 めるこ とを 要請す る。こ れは、人間にとって最も基本的で重要誼 問 題 の クラ スの1っと 考えら れる。 本研究 の目 的は、 質問応 答問題 が任意 に1つ与え られ たとき、そ れを正 確に 高速に 解くた めに、 その問 題固 有のソ ルバー を自動生成する技術を提案することである 。
本研究 の特 徴はス コーレム変数を扱う点である．。任意の一階述語論理式で書かれた前提知識を持つ質問 応答問 題を 対象と すると き、問 題をス コー レム化 を用い て変換すると、よく知られている節集合に をる。 そこ に出て くるス コーレ ム関数 は通 常の項 であり 、スコーレム変数は出現しをい。しかし証 明問題 と違 って、 質問応 答問題 の場合 には 従来の スコー レム化を用いるのは誤りであり、意味保存 スコー レム 化を用 いなけ ればな らない 。こ れによ り背景 知識として、スコーレム変数が入った節集 合を考 える 必要が 出てく る。本 研究は 、こ の意味 で、従 来考察されていをい種類の節集合を扱うと いう明 確を 新規性 を持つ 。
自 動 生 成 され る ソ ル バ ーは 、 ボ トム アップ 計算 に基づ ぃてす べての 代表モ デル の生成 を行う C
プログ ラムに をっ ている 。その ボトム アップ 計算 ではス コーレ ム変数の具体化の処理を適切に行わなけれ ばなら 社い 。各暴 礎アト ムを表 現する 整数 を配列 のイン デック スと して扱 い、配列の値を0から1に変 更する 計算を 基本 として いる。 ソルバ ー生成 は、 ポトム アップ 計算の 領域 を整数の世界に変換 するス テッ プや、 節から 得られ る操作 をC言語で コン パクト に記述 するス テッ プからなる。
本論文 の構 成は以 下の通 りであ る，
第1章で本 研究の 背景 と目的 を述べ ている 。
第2章では 、質問 応答 問題を 定義し 、質問 応答 問題を 等価変 換を用 いて解 く方 法を説 明し、意味保存ス コーレ ム化 を紹介 し、質 問応答 問題を スコ ーレム 変数が 入った節集合に対する代表モデルの共通部 分を求 める 問題に 帰着す る。
第3章では 、スコ ーレ ム変数 が入っ た節集 合に 対する 代表モ デルを すべて 求め るボト ムアップ計
算の方 法を与 える 。
第 4章 で は 、 問 題 固 有 の ソ ル バ ー を 自 動 生 成 す る 技 術 の 流 れ を 描 写 す る 。
第5章では 、スコ ーレ ム変数 を具体 化する 方法 、具体 化を確 率的に 行う方 法を 提案す る。それらは、ス コーレ ム関 数の具体化において、具体例の生成個数を抑制することを主眼とするものである。
691―

第 6章 で は、 台 集 合 を 定 義す る 。 台 集 合と は 、 ポ ト ムア ッ プ 計 算 で出 て く る 基 礎 アト ム の集 合を包 含す る 集 合 の こと で あ る 。 また 、 質 問 応 答 問題 が 与 え ら れた と きそ れに 対する 台集合 をコス ト低
く 求め る 方 法 を 与え る 。
第 7章 で は、 台 集 合 を 用 いた ボ ト ム ア ップ 計 算 を 整 数の 世 界 で 行 う手 続 き に 変 換 する 。 その ために 、各 基 礎 ア ト ムの 述 語 や 引 数に 整 数 を 割 り 当て る 方 法 、 各基 礎 アト ムに 整数を 割り当 てる方 法、
述 語や 引 数 を 表 現す る 整 数 の 組か ら 基 礎 ア ト ムを 表 現 す る 整数 を 求め る計 算方法 毅どを 提案す る。
第 8章 で は、 前 章 の 述 語 、引 数 、 基 礎 アト ム を 表 現 する 整 数 を 基 礎と し て 、 各 節 に対 応 する 手続
き を 決 定 し 、 そ れ を 実 行 す る C言 語 プ ロ グ ラム を 生 成 す る方 法 を 与 え る。 さ ら に 本 方 法に 基 づ ぃて ソル バ ー 自 動 生成 シ ス テ ム を構 築 し 、 い く っか の 問 題 に 対し て 、ソ ルバ ーを自 動生成 し、そ れを用いて実 験データ をとり、 ソルバー 自動生成 システムの 動作を確 認している。
第 9章 で は 、 本 論 文 で 得 ら れ た 結 果 を ま と め 、 今 後 の 課 題 に つ い て 述 べ て い る 。
こ れ を 要 す るに 、 本 論 文 は、 ス コ ー レ ム変 数 と い う 新た な 要 素 を含 む広い 問題ク ラスに 対し て、質 問 応 答 問 題 の正 当 で 効 率 的 極解 法 を 目 指 して 、 問 題 固 有の ソ ル バ ー を自 動 生 成 す る 技術 を 提 案
し 、自 動 生 成 シ ステ ム を 試 作 し、 動 作 を 確 認 した も の で あ り、 人 工知 能お よびソ フトウ エア科 学の分 野に 貢 献 す る とこ ろ 大 な る もの が あ る 。
よ っ て 著 者 は 、 博 士 （ 情 報 科 学 ） を 授 与 さ れ る 資 格 あ る も の と 認 め る 。

− 692―