本章ではMGTP/Gの概要を述べる。
MGTP/Gは、値域限定条件を満たす節集合を対象にした モデル生成型定理証明器である。 値域限定条件を満たす節とは、後件部に現れる全ての変数が前件部に 現れる節のことをいう。
MGTP/Gには、SICStus Prolog上で稼働するProlog版、KLIC上で稼働するKLIC版、 PIM上で稼働するKL1版がある。
MGTP/G は、MGTP の基本となる枠組を提供するものなので、 ここで、MGTPの基本的な機能とモデル生成法の枠組などについても より詳細に説明するものとする。