問題解決システムの高機能化と高速化という相反する2つの要請に対して,従来から多くの研究が行われ,さまざまな手法が提案されてきたが,未だ実世界の問題が取り扱えるほどには技術が成熟していない.実世界の問題を扱うには,複数のことを同時に考え,それらの違いを検討することによって判断を下すことができるような機能が不可欠である.このような機能は「多重文脈型問題解決」と呼ばれ,人工知能研究ではエキスパートシステム,制約充足問題の解法,あるいは,非単調推論などのための次世代の要素技術として重要性が認識されている.一般に問題解決のための推論管理は真偽維持システムで行われ,多重文脈型問題解決では単一文脈型真偽維持システムを用いるよりも多重文脈型真偽維持システムを用いる方が効率がよい.例えば,電磁モータの定性シミューションでは,単一文脈型真偽維持システムの下では完全な挙動解析はできなかったのが,多重文脈型真偽維持システムの下ではコイル1個の場合の完全な挙動解析はできるようになった.しかし,2個以上の場合にはまだ完全な挙動解析はできていない.従って,多重文脈型真偽維持システムの高速化は,応用分野を拡大するために不可欠な課題である.本論文では,多重文脈型真偽維持システムを取り上げ,その高速化を検討する.

　真偽維持システムは,推論過程を表現する「正当化」としてホーン節と一般節のどちらが許されるのか,および,単一文脈と多重文脈のどちらが許されるのかによって4種類に分類される.本論文では,多重文脈型真偽維持システムであるATMS(仮定に基づいた真偽維持システム)とCMS(項管理システム)の高速化を研究課題として設定した.具体的には,この研究課題をATMSの逐次処理の高速化と並列処理による高速化,および,ATMSとCMSの二分決定グラフ(BDD)を利用した高速化という2つの項目にプレークダウンをして,研究を進めた.

　第1部では,ATMSの高速化に取り組む.まず,第2章で,ATMSの逐次処理の高速化のために新しい処理系「網」を提案した.網処理系では,ATMSを正当化のネットワークで構成することにより,ラベル更新要求を正当化ノードごとに管理することができ,その結果,更新スケジューリングを行うことが可能となった.特に,矛盾関係を表現するnogoodの優先的な処理と重複更新要求の削除により,高速化が達成できた.網処理系の評価を通じて,それが逐次処理としてはほぼ最適な処理系であることが判明した.さらに,網処理系の静的および動的な特性を解析し,さらなる高速化には,共有メモリ型マルチプロセッサが適していることを指摘した.

　次に,第3章ではATMSの並列処理の予備実験として,ATMSとその動的な振る舞いがよく似たプロダクションシステムOPS5を取り上げ,その並列処理を並列Lisp言語QLispで取り組んだ.OPS5の並列処理は,従来処理全体の90%を占める照合段階しか行われていなかったが,それではたかだか1桁程度の高速化しか達成できない.本論文では,実行時並列度制御方式,並びに,大域的データへの単一書き込み複数読み出しのreader/writerロック,先行実行を活用して,OPS5の全実行過程で並列処理を追求する枠組みを提案し,その有効性を確認した.

　第5章では,第4章で得られたOPS5のQLispによる並列処理での知見を基にして,ATMSの並列処理に取り組んだ.まず,ATMSの逐次処理でのより詳細な動的特性を解析し,並列アルゴリズム「並列網」を設計した.並列網では,網で導入した正当化ノードを並列処理単位とし,さらに,全タスクを階層的に分解し,並列単位の粗いものから細かいものまであらゆる階層で並列処理を追求した.ATMSコマンドの処理時間のばらつきが大きいので,このようなタスクの分割によって,プロセッサ使用率の向上をねらった.また,並列処理単位は,プログラム時に固定するのではなく,実行時に決定する実行時並列度制御方式をとった.この並列処理単位の制御はQLispの制御構文を使用することによって容易にコーディングできた.また,ベンチマークで並列網による効率の向上を確認した.

　第6章では,第4章と第5章で取り組んだOPS5とATMSの並列処理での知見をまとめ,他のAIシステムの並列化にも活用することをねらって並列人工知能プログラミング方法論を論じた.OPS5やATMSでは,数値計算とは異なり,計算時間のかかる部分が分散しているので並列処理の源を同定することが難しいという問題や,大域的データが頻繁にアクセスされるという問題がある.また,アルゴリズムが逐次処理を前提として書かれており,実行順序を変更すると正しい答えが得られないという問題もある.このようなシステムに対しては,大規模な並列度を見つけることが困難であり,また,数十台規模の並列度しか有していないので,並列化には共有メモリ型マルチプロセッサが適している.さらに,上記の問題を克服するためには,階層的な処理の分割と実行時並列度制御方式とreader/writerロック,および,先行実行を提案し,全実行過程での並列処理を通じて高速化を達成する方法論の糸口がつかめた.

　第2部では,ブール関数の効率的な表現法である二分決定グラフ(BDD)を用い,多重文脈型真偽維持システムの高速化に取り組んだ.この研究のアイデアは,主項の列挙を行わず,BDDにより非明示的に論理式を処理することである.そのための研究課題として,3つの課題を設定した.すなわち,既存システムとのインターフェースの設計,BDDのサイズを最小にする変数順序を求める手法の確立,および,BDDの最大ノード数を最小にする制約条件順序を求める手法の確立である.1番目の課題は,人工知能システムのためのコンパクトな表現方法としてBDDを「plug-and-play」として使用するために必要である.2番目の課題は,BDD研究に共通するよく知られた課題である.最後の課題は,組合せ的爆発を避けるために必要であるが,従来の研究では指摘されてこなかったものである.

　第8章では,論理式で与えられた制約条件の相互関係から,最適制約順序を求めるヒューリスティクスCCVOを提案した.さらに,制約順序が決まれば,それから変数順序が決まることも示した.BDDで組合せ問題の全解を同時に求める問題を対象として,CCVOによる制約順序と変数順序が最適であることを確認した.また,最大ノード数が大き過ぎて計算ができない場合には,オンライン型分割統治法を使用する解法も検討し,その分割ヒューリスティクスを提案した.CCVOとオンライン型分割統治法によって,従来解けなかったような問題がBDDで解けるようになり,より大規模な問題の全解を同時に表現する1つの手法が確立できた.

　第9章では,BDDに基づいた多重文脈型真偽維持システムの処理系BMTMSを提案した.従来の枠組みでは,処理の完全性を達成するために主項の列挙が不可欠であった.それに対して,BMTMSの設計での重要なアイデアは,主項を非明示的に扱うことによって,主項の列挙を極力排除した点にある.実際,TMSの演算はほぼすべてBDDで扱うことができ,主項の列挙を実質的に避けることができた.この結果,従来のCMSやATMSでは時間的あるいは空間的に処理できなかったような問題がBMTMSでは扱えるようになり,知的システムの応用範囲が拡大できた.さらに,BMTMSは,従来の多重文脈型真偽維持システムとのインターフェースも考慮して設計してあるので,ATMSやその拡張,あるいは,CMSを使用した既存の応用もインターフェースを変更することなく組み込むことができるようになっている.

　第10章では,制約充足問題の解法という立場からBDDとゼロサプレス型BDD(ZBDD)をとらえ,それらによる解法を提案した.従来,ATMSでは扱える論理式が命題ホーン節に限定されるためにコーディング技法とメタルールが必要であったが,BDDやZBDDではそのようなものは一切不要である.さらに,ZBDDで制約充足問題を解く時に重要な役割を果たす組合せ集合演算として制限演算と除外演算という新たな演算を導入し,その高速処理アルゴリズムを提案するとともにその演算体系を明らかにした.特に,演算体系から制限演算や除外演算を分解することができるので,問題が簡潔に表現できるだけでなく,さらなる高速化が達成できた.これにより,全解のコンパクトな表現方法であるBDDあるいはZBDDの応用分野が多重文脈型真偽維持システムだけでなく,さらに拡大するものと期待される.

　本論文で扱った多重文脈型真偽維持システムはさまざまな応用分野がある.直接的な応用は多重文脈型真偽維持システムの高速化による,応用システムの高速化であり,それを通じてより高度なAIシステムが実用に供せられるようになろう.定性推論あるいは定性シミュレーションによる物理デバイスの挙動解析では,扱える論理の限界あるいは実行効率の悪さから,大規模な解析を行うことができなかった.本論文での手法により従来よりもより規模の大きな問題が扱える糸口がつかめたと考える.また,本論文では多重文脈型真偽維持システムの高速化を論じてきたが,その副産物として人工知能研究,コンピュータサイエンス研究に新しいアプローチを提示することができたと考える.

　本論文は、「多重文脈型真偽維持システムの高速化に関する研究」と題し、11章からなる。一般に人工知能を実現する枠組として、多くのことを同時に考えそれらの差異を検討することによって判断を定めるという形、即ち多重文脈型システムは、非常に強力で柔軟性にも富むが、その処理には従来非常に多くの時間がかかり、複雑な問題を扱う上でのネックになっていた。本論文は、多重文脈型真偽維持システムの高速化について検討し、このシステムの適用範囲の拡大を試みたものである。

　第1章「序論」は、本研究の背景と目的について考察し、本研究の意義をまとめるとともに、本論文の構成述べたものである。

　第2章「真偽維持システムとその研究課題」は、知的システムの重要な機能を実現するシステムとして、命題がどのような条件で成立するかを管理する真偽維持システム、中でも能力が高く柔軟性に富み効率のよい多重文脈型真偽維持システムを概観しその研究課題をまとめて論じ、本研究の課題を設定している。

　第3章「仮定に基づく真偽維持システムの逐次型処理系」は、多重文脈型真偽維持の一つである仮定に基づく真偽維持システム(Assumption-based Truth Maintenance System(ATMS))の逐次処理の高速化について考察したものである。すなわち、文脈推論のためにATMSの新しい処理系「網」を提案し、更新要求の吸収、更新要求の統合、正当化のための活性化フラグの導入、解釈構築コマンドとその結果のキャッシュ化等の最適化手法を導入して高速化を計り、それを20の大規模なベンチマーク処理を通して、静的及び動的な特性を明らかにしている。その結果、更新処理はかなりの並列度を持つがそれほど大きくはない、ATMSのコマンド処理の実行時間の分散は大きいなどを明らかにしている。

　第4章「プロダクションシステムOPS5での予備実験」は、ATMSの処理系「網」を並列化するための予備実験として、その動的な特性がよく調べられているプロダクションシステムOPS5を取り上げ、並列言語QLISPを用いた並列化の手法を提案したもので、OPS5の並列処理では、従来、処理の照合段階に対してだけしか行なわれて来なかったが、本論文では、実行時並列度制御方式、並びに、大域的データへの単一書き込み複数読み出しのreader/writerロック、先行実行を活用して、OPS5の全実行過程で並列処理を追求する枠組を提案し、その有効性を確認している。

　第5章「仮定に基づく真偽維持システムの並列処理-並列網」は、前章迄に得られた知見に基づき、処理系「網」を並列化する手法を提案したものである。

　第6章「並列人工知能プログラミング」は、OPS5の並列化と、ATMSの並列化から得られた知見を、並列人工知能プログフミングの観点からまとめ、他のAIシステムの並列化にも活用することを狙ったもので、実行時並列制御方式、大域的データのロック機構、遅延計算と先行的計算等の手法としてまとめている。

　第7章「二分決定グラフとその研究課題」は、命題論理式をグラフで効率良く表現する方法として最近注目されている二分決定グラフ(Binary Decision Diagram:BDD)を用いて、多重文脈型真偽維持システムの高速化を図る手法を提案する為に、まず、BDDを導入し、それを用いる場合の研究課題についてまとめている。

　第8章は、「二分決定グラフのための効率的処理方法」は、二分決定グラフを応用するための予備実験として、BDDを組合せ問題に適用する時の問題点を検討し、制約順序、および変数順序の制約順序への依存性が性能に大きな影響を与えることを明らかにするとともに、その問題点を解決するための技法として、その最適な制約順序と変数順序を求めるヒューリスティクスCCVOを提案している。

　第9章「二分決定グラフによる多重文脈型真偽維持システムの実現」は、ホーン節に限らない一般節に対する多重文脈型真偽維持システム(Clause Management System:CMS)の計算を効率化する手法について述べたもので、従来、CMSのノードのラベルを計算するには、すべての正当化から主項を列挙する必要があった。しかし、本章では、その列挙を必要とせず、論理式のままで非明示的に扱う方法を提案するとともに、既存システムとのインタフェースを容易にするために二分決定グラフを用いた多重文脈型真偽維持システムとしてBMTMSを設計している。

　第10章「二分決定グラフによる制約充足問題の解法」は、BDDを用いる場合の他の可能性について論じたもので、与えられた問題記述あるいは制約条件からBDDを構築する過程を制約充足問題の解法とみなす手法を提案している。更に、本章では、BDDによる解法と、制約充足問題に於ける一貫性アルゴリズムとの関連、及びATMSとの関係を論じている。

　第11章は、「結論」である。

　以上、これを要するに本論文は、人工知能において多くの応用の基礎となる、多重文脈を扱うことのできる真偽維持システムの動作を解析し、最適化、並列化、二分決定グラフの利用等を通してその高速化を可能ならしめることにより、この扱える範囲を著しく拡大したもので、情報工学上貢献する所少なくない。

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