論理における含意(logical implication)を計算する演繹推論(logical deduction)の逆操作であり、例からの論理的知識を学習する帰納推論(logical induction)は、今後の知識処理で重要になる機能である。論理における理論的研究の進歩が論理的帰納システムを可能とし、これは今日、帰納論理プログラミング(ILP)と呼ばれている。ILPシステムの主な目的は、与えられた正例を満たし、負例を含まない述語論理プログラムを帰納によって求めることである。述語論理は命題論理のもつ知識表現能力の限界を克服し、またILPシステムは帰納のプロセスにおいて背景知識の利用を可能にした。

　基本的にILPの問題は、生成-テストのアルゴリズムを用いることで解くことができる。解の空間は、一般化階層の格子の形で構成されている。したがって、解の探索は一般化と特殊化の演算子を用いて効率的に実行できる。各々の演算子により、解空間をトップダウンやボトムアップの方法で探索することができる。論理式の一般化の上位-下位の順序関係は、証明可能性関係(├)によって計算される包摂(subsumption)テストで確認することができる。節に対しては、包摂と呼ばれるより単純な包摂テストが存在する。開発された大部分のILPシステムは包摂に基づく一般化と特殊化の演算子を用いている。ところが、含意(implication)を考える場合、包摂は不完全であることが分っている。言い換えると、包摂に基づく演算子は常に与えられた節を導出する全ての節を常には生成することはできない。この問題は再帰節に対して生じ、その結果、再帰論理プログラムに対しても生ずる。

　我々はforced simulationと呼ばれる手法を拡張して、MiMFoSという名のILPシステムを開発した。インプリメントされたアルゴリズムは線形再帰型ij-確定項(linear recursive closed ij-determinate)の2節から成る論理プログラムと呼ばれる再帰論理プログラムの制限されたクラスを帰納することができる。この手法では仮説は包摂による演算子では生成されない。代わりに、ベース節と再帰節の初期仮説は正例の初期集合から生成され、再帰リテラルは最初に生成された再帰節に含まれる変数の置き換えによって生成される。この理由により、仮説は関数を含まない形で生成されねばならないが、これは厳しい制約とはならない。なぜなら、関数項はflattening操作によって節から取り除き、unflattening操作によって回復することができるからである。仮説の正当性(correctness)は、深さ制限のある(depth-bounded)論理的証明器(theorem prover)によって検査される。証明の過程で初期仮説は必要ならば一般化され、再帰の各ステップごとに新しい基礎アトム(ground atom)が生成される。これらの新しい基礎アトムは初期例の集合には含まれず、与えられた正例からスターとする再帰の推論の連鎖から形成される。

　初期仮説を一般化するために、これまでの手法では神託(oracle)によって正例を(ベース節で証明できる)ベースケース、および(証明に再帰節を必要とする)再帰ケースに分類する必要があった。我々の独自の手法で、この神託を制約付2極小多重汎化(constrained 2-minimal multiple generalization(2-mmg))と呼ぶアルゴリズムで実現している。よく知られた最小汎化(lgg)アルゴリズムは、基礎アトムの集合から一つの最小汎化リテラルを見い出す。制約付2-mmgアルゴリズムはlggの考えを拡張し、基礎アトムの集合から二つの節を見い出す。この見い出した二つの節は、正例の集合をベースケースと再帰ケースに弁別するのに用いることができる。

　MiMFoSプログラムはProlog言語で開発されている。図1はMiMFoSによって例から帰納的に生成されたいくつかの再帰論理プログラムを例示している。

図1:MiMFoSによって帰納された再帰プログラム

　本論文は"A Study on Induction of Recursive Logic Programs(再帰論理プログラムの帰納に関する研究)"と題し、与えられた正事例を証明でき、負事例を証明しない論理プログラムを自動生成する帰納論理(inductive logic)において、論理プログラムの重要な形式であるが従来手法では困難であった再帰論理プログラムを自動生成する新手法を示しており、英文で記されている。

　第1章は序論であり、帰納論理の基本メカニズムについて説明し、再帰論理プログラムの帰納に関するこれまでの関連研究について紹介している。

　第2章"Inductive Logic Programming(帰納論理プログラミング)"では、まず帰納論理を構築する上での基礎手法についてまとめている。モデル論と証明論による帰納論理の原理について記し、現実の帰納論理プログラムは証明論の立場から構成されることを述べている。与えられた正例を包含し負例を包含しない論理プログラムを解として生成するためには、一般化と特殊化が基本操作となる。これを効率的に実現するための有用な要素手法として、包摂(subsumption)テスト、最小汎化、背景知識の存在も考慮に入れた相対最小汎化(relative least general generalization)、背景知識の存在下である論理知識を生成するのに必要な仮説知識を求めるSaturation操作、逆含意演算操作(inverting implication)等について記している。

　論理式間の一般化-特殊化の上位-下位関係は、証明可能性関係(├)によって計算できる包摂テストで確認することができるが、節形式の論理式に対しては包摂と呼ばれる単純な包摂テストが存在する。この包摂は、現在最も優れているとされるProgolをはじめ、これまでの帰納論理プログラミングで有効に利用されてきた。しかし、包摂に基づく一般化、特殊化の操作は不完全性があり、再帰を含む節に対しては一般化した節が常には下位となる節を導出できないことがあることを指摘し、これが従来の論理プログラミングの手法で再帰節をうまく生成できない主要な要因となっていることを示している。

　第3章"Forced Simulation-Principles and Extension(強制シミュレーション-原埋と拡張)"では、再帰節の帰納における上記の問題を克服するための手法を示している。これはW.Cohenにより導入された強制シミュレーション(forced simulation)法の拡張となっており、線形再帰型ij-確定項(linear recursive closed ij-determinate)の2節から成る再帰論理プログラムの帰納を対象にしている。

　この手法では解候補となる仮説の生成に包摂による演算操作を用いず、代わりにベース節(非再帰節)と再帰節の初期仮説を正例の初期集合から生成し、再帰りテラルは最初に生成された再帰節に含まれる変数の置き換えによって生成する。このとき、仮説となる節は関数を含まない形で生成する必要があることがら、関数項を除くflattening操作、その逆操作であるunflattening操作を導入している。生成した仮説の正当性の検査には、深さ制限を持つ定理証明器(theorem prover)を用いるが、証明過程の再帰の各ステップ毎に新しい基礎アトム(ground atom)の生成と、これらも包含するように仮説の負例を包含しない範囲内での一般化を行う。

　第4章"Constrained Mininal Multiple Generalization(制約付極小多重汎化)"では、第3章の帰納手法を適用する前処理として必要な正例の分類手法について示している。第3章の手法は正例を(ベース節で証明できる)ベースケースと(証明に再帰節を必要とする)再帰ケースに分類して与える必要があるが、この自動分類手法はこれまでに存在しなかった。ここでは制約付2極小多重汎化と呼ぶアルゴリズムで実現している。2極小多重汎化(2-mmg)は、基礎アトムの集合から一つの最小汎化リテラルを見い出す最小汎化(1gg)の拡張であり、基礎アトムの集合から極小な二つの汎化リテラルを見い出す。これだけでは不十分な場合が生じるので、ここではある変数に値の範囲を制約する機能を付した制約付極小多重汎化を考案している。これにより、正例の自動分類を実現する手法としている。

　第5章は"Implementation of MiMFoS"であり、第3、4章に記した手法に基づく、MiMFoSと名付けた再帰論理プログラムの帰納システムの詳細について記している。MiMFoSはProlog言語を用いて実装されている。

　第6章"Experiments with MiMFoS"では、MiMFoSにより与えられた例からの再帰論理プログラムを帰納したいくつかの実験結果を示している。ベース節と再帰節という2節から成る再帰論理プログラムに限られているが、従来手法では不能であった再帰論理プログラムの帰納が、効率的速度で可能になったことを示している。

　第7章は結論であり、本論文の研究成果を要約している。

　以上を要するに、帰納論理プログラミングにおいて、従来手法では困難であった例からの再帰論理プログラムの帰納に関し、拡張強制シミュレーションと制約付極小多重汎化に基づく新しい手法を考案し、これを実装したソフトウェアを作成して効果を実証的に示したものであり、電子情報工学上貢献するところが少なくない。

　よって本論文は博士(工学)の学位請求論文として合格と認められる。