MGTP (Model Generation Theorem Prover) は 第５世代コンピュータプロジェクトで開発された一階述語論理の並列定理証明 システムで、モデル生成法と呼ばれる方式を採用している。モデル生成法は、 定理証明システムを並列論理型言語であるKL1言語で実装するのに最も適した 証明方式である。このため、MGTPは並列推論マシン上で極めて効率よく動作す る。
MGTP では、ユーザがルール形式で記述した問題を読み込み、 証明結果を出力する。ルールによる表現は、一階述語論理に関する知識がなくても 直観的に理解することは容易である。 まずは、
を参照されたい。ルールベースのボトムアップ推論機能や一階述語論理 などに親しみのある人は、ここはスキップしても構わない。MGTP の文法、MGTP で実現する基本機能については、下記を参照されたい。