MGTP/G各版について

いずれの版も、MGTP節によって与えられた問題は、前処理プログラムによってProlog節集合もしくはKL1節集合に変換される。これらがMGTP/G本体プログラムとリンクされて、証明の実行形式プログラムができる。

Prolog 版

Prolog版は、戦略の違いから三つのタイプの処理系がある。

戦略I: 全てのモデル拡張候補によって拡張を行なう。得られるモデル候補にモデル棄却規則を適用する。
戦略II: モデル拡張候補の内一つを選び、拡張を行なう。残りのモデル拡張候補はスタック% % に積まれ次回のモデル拡張の候補となる。拡張されたモデル候補についてモデル棄却規則を適用する。
戦略III: 選言を含まない全てのモデル拡張候補によって拡張を行なう。選言を含むモデル拡張候補はスタックに積まれる。得られるモデル候補(一つしかない)にモデル棄却規則を適用する。もし、選言を含むモデル拡張候補しかなかった場合は、そのうちの一つを選び拡張する。残りのモデル拡張候補はスタックに積まれる。得られるモデル候補(複数)にモデル棄却規則を適用する。

いずれも、MG節の中からProlog述語の呼出しが可能である。

KLIC版は、RAMS法を搭載した版とMERC法を搭載した版がある。ほかに、次のような機能を持つ。

機能はProlog版と、Prolog呼出の代わりに KL1呼出が行なえる点を除いて、全く同じ。前件部ではKL1ガード述語、後件部ではKL1ボディ述語呼出が可能である。