本章ではMGTP/Nの概要を述べる。
MGTP/Nとは，証明対象領域をホーン問題のみに限定した モデル生成型定理証明器である． ホーン問題とは，ホーン節(後件リテラルの数が高々1個の節) のみからなる節集合のことである． その代わり、MGTP/Gにあった値域限定条件はもはや課せられない．
MGTP/Nには，SICStus Prolog上で稼働するProlog版と PIM上で稼働するKL1版がある． KL1版には，内部記憶機構の違いから，モデル共有型と モデル分散型の二つのタイプがある．