MGTP Primer

Since 1989

このページでは、ICOT で研究開発されたモデル生成型の定理証明システム MGTP に関する説明をします。

定理証明システムは古くて新しい研究テーマです。

定理証明システムは、AI という言葉がうまれた当初から、AI の有望なアプリケーションとして研究開発が行なわれてきた分野です。数学の定理を証明することだけではなく、その他の問題解決システムとして利用可能であるという点で、注目を集めてきました。日本では、定理証明システムというと、古典的 AI の研究というイメージが強いのですが、欧米では、依然として多くの研究者が研究開発に取り組んでおり、記述能力や推論効率、また、応用領域に関しても着実な進歩を遂げている領域となっています。

MGTP は一階述語論理に基づいています。

MGTP は、一階述語論理の論理体系に基づいており、 Prolog のようにホーン節に限定されることもありません。フルの一階述語論理は、非常に広範囲な知識を表現することができます。また、MGTP においては、さらに失敗による否定や様相オペレータを取り込むことによって、非単調推論を取り扱うこともできます。

MGTP はボトムアップ型のシステムです。

MGTP は Prolog のようなトップダウン型のシステムではなく、事実から推論を行なっていくボトムアップ型のシステムです。ボトムアップ型のシステムでは、トップダウン型に見られるような同じ証明を繰り返し実行してしまうような冗長性を排除することができます。また、ボトムアップ型に特有な、証明すべき定理と関連のない推論を実行してしまうという問題については、マジックセット法と呼ばれるトップダウン推論との融合技術が考案されています。

MGTP は並列化に適した構造を有しています。

ボトムアップ型であり、また、値域制約という条件を満足する MGTP は並列化に非常に適した推論形式です。特に、OR 分岐については、他の枝と変数を共有することなく実行させることができるので、並列化方式を工夫することによって、ほぼ線形に近い台数効果を達成することができます。ICOT で開発された PIM/m において、256 台のプロセッサを使用し、高い並列化効果を示すことができました。

MGTP の研究は今も続けて行なわれています。

ICOT から九州大学に移られた長谷川隆三教授を中心として、 MGTP の研究開発は、現在も継続しておこなわれています。汎用並列機上での効率的な並列化手法、探索制御技術、 GA などの確率的探索手法の取り込みなどが主なテーマです。また、最近では、MGTP をベースとして、法的推論への応用を考慮したシステム開発も並行して行なわれています。

MGTP 入門(MGTP Primer) MGTP のダウンロード MGTP 処理系 (CGI script) 九大サイト MGTP を用いた実験結果等
推論の効率化技法 MGTP上の高度推論機能の紹介
開発メンバーの紹介関連サイト

Last Update : 31 March, 1999
shirai@mri.co.jp