- 従来、MGTPのOR並列化に関して、図(a)に示すようなPEを循環割り付けする方 式がPIM上で採用され、簡易な割に（通信を含めた見かけ上の）稼働率が高く、 幅優先探索に適しているなどのメリットもあった。この方式は分岐サブタスク が生じた時点でただちにほかのPEに投げる、というものであり、確率的割り付 け方式などの方式も同じ原理に基づいている。 しかしながら、これらは、プロセッサ間通信のコストに対する配慮がなされて おらず、最悪の場合、MGTP証明木のノード数に比例した通信量が生じる。これ は、UNIXマシンの分散環境をサポートするPVMシステム上においては、著しい 性能劣化（２桁以上の速度低下）を引き起こし、事実上、並列分散化を不可能 なものにしている。
(a)循環割り付け (b)N逐次割り付け (c)N逐次タスクスタック
- この問題を解決するために、図(b)に示すように逐次アルゴリズムを使用PE台数
に応じてN本並行動作させる、N逐次方式と呼ぶ方式を考案した。この方式は、
サブタスクの発生時点ではなく、暇なPEからの要求があったときのみタスクを
投げ、各PEでは深さ優先探索を行うことを特徴とする。
図(a)は、使用PE数が３の場合の、循環割り付けによるタスクの割当を示してい る。木の各枝は、MGTPにおける探索枝を表しており、ノードに付けられた番号 はそのノードの探索を割り当てられたPEの番号を表す。一つの（親）ノードか ら分岐する三つのノードの内、再左子ノードは親ノードと同じPEに割り当てら れるが、その他の子ノードは、循環的に割り当てられる。
一方、図(b)のN逐次方式では、まず、１番PEが親ノードに割り付けられる。三 つの子ノードが生じると、最左子ノードを引続き１番PEが実行する。ここで、 ２、３番PEからのタスク分与要求があれば、残りの子ノードがそれぞれのPEに 割り付けられる。その後、各PEではそれぞれ担当したノード以下を深さ優先的 に処理することに専念し、通信はしばらく起こらない。そして、いずれかのPE が先に受け持ちタスクを完了したときは、ほかのPEにタスクの分与を要求する ことにより、負荷の分散を図る。
各PEは、図(c)のようなタスクスタックを一つずつ保持する。こうして、各PEは サブタスクが生じたとき自スタックにこれを一旦pushし、現在処理中のタスク を完了後にpop-topして残りを処理するという逐次的処理を行う。一方、他PEか らのタスク分与要求に対しては、スタックの底からpop-bottomによってタスク を取り出して与える。
すでに我々は、このN逐次方式をPIM上のMGTPに対して実験的に実装し、Loveland の例題(SYN009-1)において、従来の循環割り付け方式では２万回近く要していた タスク割当回数を100回程度に削減できることを確認している。
本研究においては、共有メモリ／分散メモリ型の汎用並列マシン上におけるN逐 次方式の実装とその評価検討を行い、効率的な並列分散化方式を確立することを 目的とする。本方式は、MGTP以外にも適用可能であり、知的バックトラックのよ うな逐次性の強いアルゴリズムの並列化に特に適していることから、一般の知識 処理プログラムに対する汎用の並列分散化機構を提供することを目指す。
- 本研究では、以下に述べるような推論機能・機構をMGTPに導入することを検討す
る。
(a) ルール間優先順位に基づく推論機構：法的推論における論証では、いわゆる法 律の条文を形式化した規則と、個々の事例における事実が一階述語論理の範囲 で記述されるほか、規則間に優先順位が設けられ、これに基づいて複数の論証 の間での優劣が問題にされることがある。たとえば、
r1 (X): t(X) → u(X).
r2 (X): t(X) → ¬u(X).
f1: true → t(a)というMG節集合は充足不能であるが、
p1 (X) : t(X) → r1 (X)>r2(X).
という優先規則（r1 (X)>r2(X) は、ルールr1(X) が r2 (X) に優先されることを表す）が追加されていれば、 A:{t(a),u(a)}なるモデルがあって充足可能となる。 p1(X) の代わりに
p2(X): t(X) → r1(X)<r 2(X).
なら、B:{t(a),¬u(a)} なるモデルがある。見方を変えると、優先規則がない場合、 A,Bの対立する帰結集合が矛盾して全体として一定の結論が得られないのだが、 優先規則が加わると、A,Bの間に優劣が定まり、全体としては優位な方の帰結 を選ぶことができる、ということである。
法的推論においては、対立するA,Bの論証がそれぞれある規則と事実の集合に 基づいてなされるとき、AとBとで使われた規則の優先順位によって勝負を判定 する、という具合に用いられる。
ここでは一つの実装方式として、MGTP上でNAFを実現する際に用いられた技法 の適用が考えられる。たとえば、規則 r1(X),r2(X) に優先順位が与えられる可能性がある場合、p(X) → Kr1 (X);Kr2(X)
のように、予め r1(X) を適用可能とする場合と r2(X) を適用可能とする場合に場合分けを行うような規則を導入する。 Kr1(X) の場合の論証課程で、 rn(X)>r1(X) のような優先順位が実際に加えられると、この論証は成立しない（勝てない）ことが わかる。これは、
KR(X),R'(X)>R(X) → false.
のようなスキーマによりモデル候補を棄却することで実現される。このような、 MGTP実行時における論証検査機構の実装のほか、静的に定まる規則間優先順位 を予め適切なMGTP入力節で表現しておく（コンパイルする）ための記述変換ツ ールの実装についても検討を行う。
(b) 探索制御機能の拡張：組み合わせ最適化問題や、一般の探索問題などを扱う 際、解の候補を動的に選別／棄却する等の機能が不可欠である。このため、MGTP に対して、（イ）個別に探索される複数の解候補（モデル候補）を比較するため、 枝分かれの際に各分枝に評価値を付与する機構、（ロ）モデル候補間の通信機 構、（ハ）評価関数に基づくモデル候補棄却規則の導入、などの拡張を行う。 これらの機能の組み合わせにより、α-β法などのアルゴリズミックな探索技 法の記述を行うことができるようになる。(c) ヒューリスティック探索の機構：上記、探索制御のほか、遺伝的アルゴリズム (GA)の手法の導入を検討する。我々は、GAの計算機構が、MGTPと同様に閉包計 算を基本とするという点にまず着目した。
ただし、我々は、一般の定理証明システムにおいて従来アドホックに行われて いた証明探索技法（項に対する重みづけと、それに基づく削除／整列化戦略な ど）を、より系統的に扱うことを目的としており、その枠組としてMGTPの推論 機構自体との相性が良さそうなGAを導入するのである。
具体的には、たとえば、MGTPのモデル候補中の帰結アトムを個体とみなし、こ れに対する、(1)染色体、遺伝子のデザイン、(2)交配、突然変異の定義、(3) 適応度関数の定義、をユーザが与えるものとする。これらは、所与の問題の意 味を良く理解しているユーザが、MGTPの試行を通じて得ることのできる「解へ の近さ」に関する直観をコーディングし、これに基づいて探索を絞り込むため の機構を（あくまでヒューリスティックではあるが）形式化したものにほかな らない。
我々は、定理証明のベンチマークであるTPTP問題集から、condensed detachment と呼ばれるクラスの問題を選び、すでにいくつかの予備実験を行っている。そ の結果、極めて簡単な遺伝子設計と適応度関数を与えた場合でも、半数あまり の例題で、これまで有効とされていたアドホックな探索技法より短い証明が得 られた。
本研究では、より複雑な遺伝子コーディング設計のための支援（たとえば、ア トムではなくモデル候補を個体とみなす、など）、を検討し、MGTPへの付加モ ジュールおよび支援ツールの開発を行う。
- 現在あるMGTPウインドウマネージャ(Tcl/Tkで記述）をベースとして、WWWブラ
ウザで稼働するMGTPのGUIシステムを開発する。本システムは、(1)問題の入力
(テキストによる入力、ファイル名による指定）、(2)MGTPの起動／実行中断／
実行再開、(3)各種オプション指定(KLIC-MGTPが提供する諸機能の他、今回作成
するルール間優先順位機能、探索制御機能、並列分散化機能、ヒューリスティ
ック探索機能などを利用するか否か）、(4)推論の説明や冗長推論の除去、など
の機能を有する。(4)については、推論過程を記号的にトレースする機能や推論
図などによる図的表示機能を実装する。
また、本システムを利用してMGTPのホームページを作成する。ホームページで は、MGTPの宣伝・配布・普及を行うが、GUIシステムを用いてホームページ上で MGTPを利用できる環境を提供する。これによって、利用者はMGTPを試用してか らダウンロードすることもできるようになる。
