定理証明器 MGTP (Model Generation Theorem Prover) [1]は， (財)新世代コンピュータ技術開発機構(ICOT)において開発された モデル生成型定理証明システムである． MGTPはフルの一階述語論理における充足可能性の判定や， 節集合の極小モデルの計算を，ボトムアップ型の前向き推論により行う． フルの一階述語論理を扱えるという点において， MGTPはPrologでは扱えないnon-Horn節をケース分割により取り扱うことができる．
しかし，Horn節によるプログラミング手法が開発され， 各種の応用プログラムが書かれているPrologと比べると， MGTPにおけるnon-Horn節プログラミングのための技法は まだ十分開発されているとは言えない．
第１に，MGTPを高速な定理証明器としてではなく，もう一つの重要な側面である， 論理プログラミング分野における 選言付論理プログラミング(disjunctive logic programming)のボトムアップ処理系として捉えた場合，各種のプログラミング 技法の整備は必須課題となる．特に，ケース分割により構成される木を用いて， 各種の探索問題が自然に実現できるように，探索方式を整備することが望まれる．
第２に，定理証明器としてのMGTPにおいても，公平な(fair)戦略を実装している とは現状では言えない．例えば，有限のモデルと無限のモデルを持つような 充足可能である節集合では，探索の仕方によっては無限の枝を探索し続けてしまい， 停止しない状況に陥ることがある．これはMGTPが提供している３つの制御戦略 [1]がいずれも 深さ優先探索を仮定しているためである．
第３に，井上らは過去２年間における研究において， MGTP上でさまざまな高次推論体系を実現する処理系 (ALP処理系[3], アクション言語処理系[4])を開発してきた． これらの処理系では，MGTPのケース分割による推論に着目し， 選言付論理プログラミング処理系によるモデル生成エンジンとしてMGTPを使用する ことで，失敗による否定(negation as failure; NAF)， アブダクション (abuduction)，およびアクション言語などの高次推論処理系を 実現している． このようなMGTP上の応用は，MGTPの有効性を実証したものと捉えることができるが， 適用できる問題のクラスには制限がある．応用においても，組合せ問題の幾つかは 解けるが，コストが付く場合の 最適化問題をうまく解くことはできない． 例えば，与えられたグラフのハミルトン閉路を求めるためのプログラムを書いて MGTPで計算できる．しかし，グラフの各枝にコストが付いた 巡回セールスマン問題(traveling salesman problem)に対しては， 決定問題・最適化問題ともにうまい解法を実現することはできない．
このように，MGTPの適用範囲を拡大し，実際の応用問題に使用するためには， コストや確率に基づいて探索を行う機能が必要となる．