| 平成８年度 委託研究ソフトウェアの 最終成果報告書 |
MGTPは、モデル生成法に基づく一階述語論理の定理証明システムであ る。MGTPの実装言語はKL1であり、KLICシステムによりC言語にコンパイルされ る。証明効率を高める様々な機能をMGTPは備えている。Folding-upやNHM機能 は、証明の分岐に起因する冗長な推論を除去するものである。モデル生成法に 基づく定理証明システムでは、連言照合操作が実行効率に大きな影響を与える が、MERCやRAMS法は、この連言照合操作を高速に実行する。弁別木による検索 も付加され、これにより与えられた項に単一化(もしくは照合)可能な項の検索 が高速に行なわれるようになった。これらの機能により、MGTPの実行効率は格 段に向上する。
負(否定)制約伝搬を取り込んだCMGTPも、有限領域の制約解消システ ムとして利用する事ができる。CMGTPは、MGTPを少し改良したもので、先に述 べた様々なMGTPの機能を継承している。さらに、MGTPウィンドウ・マネージャ によりMGTPの操作がより容易になった。
www-admin@icot.or.jp