研究の内容

これまでの成果を元に以下の項目について研究及び開発を進めた。

1. 汎用並列マシン上のMGTP並列化：PIM上で開発した並列実行方式をそ のまま商用並列マシン上に実装してもPIM上で実証されたほどの性能は でないことがいくつかの実験で判明した。これは、商用並列マシンは PIMに比べ 通信効率が劣るためであると考えられる。 そこで、PE間通 信を抑えるN逐次実行方式を考案した。従来の並列化方式が「仕事があ れば並列に実行する」というものであったのに対し、新方式は、「PEが 暇なら仕事を分配し、かつPE内は逐次実行」という考えに基づいている。
2. Java-MGTPの開発：HTMLとCGIを用いたMGTPの実行環境では、MGTPはWWW サーバがあるマシン上で走行するため、サーバに負荷が集中するという 問題が生ずる。この問題を解決するために、WWWブラウザ側でMGTPの実 行を行えるように、MGTPのJava化を行った。また、MGTPのGUIシステム をJavaを用いて作成した。
3. CMGTPの改良：負制約を扱うCMGTPは、負制約処理により探索空間の刈り 込みが行える。従来の負制約処理には、いくつかの無駄な処理が行われている ことが判明し、これを改良した処理方式を考案し実装した。また、CMGTPにつ いてもJava化を行った。
4. 探索制御機能の拡張：MGTPは定理証明の探索において縦型探索で証明を 行なっているが、盲目的な探索のため無駄な計算を行なう場合が多い。そこで、 評価値をよる探索制御機構を採り入れたA*-MGTPを試作し、遺伝的アルゴリ ズムに基づく探索法との比較評価を行った。