| 定理証明は、与えられた公理と推論規則から、目的とする定理が導かれているかどうかを自動的に判定する手法で、論理プログラミングや人工知能分野の基礎となっている重要な技術です。
ICOT で開発した MGTP は、モデル生成法に基づく、KL1 ベースの１階述語論理の並列定理証明システムで、MGTP は数学以外の広範な応用にも適応できます。 実際 ICOT では、法的推論システム HELIC-II のルールベース推論システムとして使用され、高度な推論機能と、高速処理の実現に大きく貢献しています。 ここでは、MGTP のルールをご覧にいれながら、MTGP の証明方法を説明します。 また、MGTP の有用性を示す例として、カナダの数学者、ベネット教授から提出された準群の存在問題を紹介します。この問題は、それまで次数８までを人手で証明しているだけでしたが、ICOT では MGTP を用いて、次数１６まで証明することに成功しました。 ここでは、次数１１の準群問題を MGTP を用いて実際に解いてみます。この時、２５６台のプロセッサ構成の PIM-m システムの稼動状況を、パフォーマンスモニターを使ってご覧に入れます。 また、次数１３のベネットの準群問題を PIM-m を用いて時の、MGTP の台数効果を示すグラフもご覧に入れます。 |