（２２）並列モデル生成型プルーバ：ＭＧＴＰ


	マ シ ン：PIM
	環　　境：PIMOS
	言　　語：KL1
	ソース量：2 KB
	文　　書：マニュアル (日本語／英語：簡易版)

概要

高効率、高並列に有限領域の一階述語論理の定理証明を行う定理証明器である。

特徴

Range Restricted（節の帰結部に現れる変数はすべて前提部に現れる）な一階 述語論理の証明問題を解く非常に高速な並列プルーバである。
  1. 高度な問題解決機能を必要とする応用には、強力かつ汎用の推論機能が必 要である。
  2. 本プログラムは問題をＫＬ１述語にコンパイルすることにより、非常に高 い性能をもつ定理証明器であり、また非常に高い並列性を持っている。
  3. 並列に動作する高性能の定理証明器であることから、これまでにない全く 新しいプログラムである。

構成

ＭＧＴＰは、問題コンパイラとインタプリタの２つのモジュールにより構成さ れる。

機能

ＭＧＴＰは、与えられた問題にモデルがあればそのモデルを、モデルがなけれ ば空リストを返す。

ＦＴＰ

www-admin@icot.or.jp