局所的概念駆動対話型数学知識ベースシステムに関 する研究
著者 王 国傑
雑誌名 静岡大学大学院電子科学研究科研究報告
巻 17
ページ 151‑153
発行年 1996‑03‑29
出版者 静岡大学大学院電子科学研究科
URL http://hdl.handle.net/10297/1207
氏名0(本籍
)
王国
傑 (中国
)
学 位 の種 類
博
士
(工
学)
学 位 記 番 号
工博 甲第
102
号 学位授与の日付平 成 6年 9月 22日 学位授与の要件
学位規則第4条第 1項 該当
研究科。専攻の名称
電子科学研究科
電子応用工学専攻
学位論文題目
局所的概念駆動対話型数学知識ベースシステムに関する研究
論文審査委員 (委員長)
教 授 市 り
￨1
朗教 授 福 田
明
教 授 水 野 忠 則 教 授 鈴 木 淳 之
助教授 山 口 高 平 助教授 伊 東 幸 宏
論 文 内 容 の 要 旨
数学知識ベースシステムは人間による数学の理解 と創造及び数学 を道具 としての使用 に大 きな役割 を果たす ことがで きる。本研究は、このような数学知識ベースシステムを開発することを目指す もの である。数学知識ベースシステムを開発するにあたつて多 くの課題があるが、本論文は特 に、数学知 識 を効率的に検索で きること ;抽 象化 による問題解決、事例 に基づ く推論 などの高次推論が行なえる
こと ;テ キス トか らの知識獲得の自動化の三項 目について研究 した結果 をまとめた ものである。
知識ベースに対 して大局的に知識を網羅的に検索する従来の方法における効率低下の問題 を解決す るために、本研究では、概念階層 を用いて、与えられた問題 に現れている概念に関連する知識のみを 検索する概念駆動 とい う推論機構 を持つ数学知識ベースシステムを提案 した。特 に概念階層 として定 義階層 を用いることによつて、これを用いない場合 に比べて推論の効率 を大幅に改善で きた。
このシステムに基づいて、定理証明の過程において探索空間を削減するために問題解決の階層化の 手法を検討 した。抽象化 による階層的問題解決法は複雑な問題 を階層的に単純化 して解 く方法である。
従来 この手法は任意段数の階層化 に対 してはプランニングシステムにのみ適用 されていたが、概念の 定義階層 を用いることによつて定理証明に対 して も適用で きるように した。 この提案 において、定義 階層 に基づ く抽象化 を定義 し、問題解決の階層 を概念階層 における レベルによって決定 した。最良の 場合、証明の検証に要する時間は証明の長 さに比例することが実験か ら分かつた。最悪の場合には証 明を検証する効率が上が らないが、悪 くなることはない。 また、抽象空間の無矛盾性 を保存するため
‑151‑
に、従来の公理系 を表現する形に対する制約 を克服 し、命題抽象化によって抽象空間の無矛盾性 を保 存する方法 を与えた。抽象的な証明の具体化には多数の しかたがある。従来の方法では、 これを制限 していないので、問題解決の効率が大幅に下がることがある。そのために、抽象化の際に捨てた情報 を保存 してお き、具体化の際にこれを用いる方法 を提案 し効率の低下を防 ぐことがで きた。
既知証明を利用 して証明 しようとする命題(ターゲ ッ ト定理)を証明すること、いわゆる事例 に基づ く推論がある。従来の方法では、既知証明をターゲ ッ ト定理の証明に変換 して類題 を解 くが、変換 さ れた証明が ターゲ ット定理の証明になるとは限 らない。そのために、本研究は、既知証明の トレース をまず定理スキーマ(すなわち、二つの命題の抽象化)の概念を用い抽象化する。次に、その定理スキー マに基づいて証明プランを生成 し、その証明プランをターゲット定理を証明するためのガイ ドとして 使用する方法 を提案 した。証明プランは証明を生成するための手続 きである。抽象化 した証明プラン をガイ ドとして使用するだけなので、抽象化 した証明プランが必ず しも類題の証明になる必要はない。
これによって、既知証明を柔軟 にターゲ ッ ト定理 に利用で きる。
既知証明を検索するためには、その証明を持つ定理 を検索すればよい。従来の方法では、定理 を検 索する基準(つまりある決 まった特徴 を用いる)は ターグ ッ ト定理 を証明す ることと関連 していないの で、検索 された定理は必ず しもターゲ ット定理の証明に利用で きない。 この問題 を解決するために、
証明プランを生成するために使用 した定理スキーマを用いて定理 を検索する方法を提案 した。 この方 法によって検索 した定理はターゲ ッ ト定理の証明に利用で きることが実験 によって確かめ られた。
テキス トか ら数多 くの知識 を獲得するために、本研究では定義 と定理 に限定 し、従来の自然言語の 一般処理の困難 を避け、自然言語で表現 された定義 と定理からテンプレー ト(文の一種のパ ター ン)を 用いてそれ らの論理式表現 を求める方法 を提案 した。 この方法によって教科書か ら定義 と定理 を効率 的に獲得で きることが実験から分かつた。
論 文 審 査 結 果 の 要 旨
数学知識ベースシステムの開発は人間による数学の理解 と創造及び数学 を道具 として使用するため に大 きな役割 を果たす と考えられる。本論文は関連知識の検索、抽象化 による問題解決、事例に基づ く推論、テキス トか らの知識獲得の自動化 など数学知識ベースシステムに関する研究結果をまとめた ものである。
知識ベースに対 して大局的に知識 を網羅的に検索する従来の方法では効率低下が問題 となるが、こ の問題 を解決するために、第2章では、概念階層 を用いて、与えられた問題に現れている概念に関連す る知識のみを検索する概念駆動 とい う推論機構 を持つ数学知識ベースシステムを提案 している。特 に 概念階層 として定義階層 を用いることによって、これを用いない場合に比べて推論の効率 を大幅に改 善で きることを示 した。
第3章 ではシステムの推論 を効率化するために階層的問題解決の方法を提案 した。従来の手法では任 意段数の階層化はプランニングシステムにのみ適用 されているが、本研究では、任意段数の階層化 を 自動化することがで きた。概念の定義階層 を用いることによって定理証明に対 して も任意段数の階層 化 を適用で きるようにした結果、証明の検証 に要する時間が証明の長 さに比例することを実験 によっ て示 した。 また、抽象空間の無矛盾性 を保存するために、従来の公理系 を表現する形 に対する制約 を 克服 し、命題抽象化 によって抽象空間の無矛盾性 を保存する方法 を与えた。
第4章 では、既知証明を利用 して命題(ターゲ ット定理)を証明する方法 を提案 した。これは既知証明 の トレースを定理スキーマ(すなわち、二つの命題の抽象化)の概念 を用い抽象化 し、これに基づいて 生成 された証明プランを、 ターゲ ッ ト定理証明のガイ ドとして使用する方法である。抽象化 した証明 プランをガイ ドとして使用するだけなので、それが必ず しも類題の証明になる必要はな く従来の変換 による方法 と比べて事例の適用範囲を広げることがで きた。
テキス トから数多 くの知識 を獲得するために、第5章では、自然言語で表現 された定義 と定理からテ ンプレー ト(文の一種のパ ターン)を用いてそれ らの論理式表現 を求める方法 を提案 している。ここで は、定義 と定理に限定 し、従来の自然言語の一般処理の困難を避けた。 この方法によって教科書か ら 定義 と定理の論理表現 を効率的に獲得で きることを実験 によって示 した。
以上述べたように、本論文は数学知識ベースシステムに関する研究の進歩 に大 きく貢献する内容 を 有するもので、博士(工学)の学位 を授与するためにふ さわ しい内容であること認定する。
‑153‑
