図 2: MTGP+MTGP


のようなMGTPルールに変換される。ここに、Ei は Γ の基礎例の部分集合で
あり、アトム Ai が依存する仮説集合を表す。また、cc は次のように定義される
関数である。



MGTP-1が新しい基礎アトムを導くたびに、組み合わされる仮説集合の無矛盾性
がMGTP-2によって検査される。この構成(図2)においては、一度に生成され
る複数のMGTP-2に並列性がある。

Skip方式

Σの任意の節が、その前件部に仮定可能なアトム H1,...,Hm (Hi∈Γ, m≧0)を含んでいるとき、すなわち、



であるとき、これを以下のような形式のMGTPルールに変換して扱う:



つまり、前件部における各仮説はマッチングの対象から除外され、右辺にSkipさ
れる。この方式では、もしモデル候補がHと¬KHとを含んでいたならば、次
のスキーマによって棄却される:




このシステムでは、MGTPが提供するOR並列を利用した並列化がなされてい
る。また、この方式において、構成されるモデル候補の組合せ数を減少させるよ
うな知識を自動的に生成する方法についても示す。


					- 72 -