平成８年度　委託研究ソフトウェアの成果ソフトウェア

(11) KLIC 上の MGTP 処理系

研究代表者：長谷川隆三　教授
　　　　　　九州大学大学院システム情報科学研究科知能システム学専攻

MGTP:定理証明システム

長谷川隆三 (九州大学大学院システム情報科学研究科)

配布ソフトウェアは以下の機能を有するUNIXコマンド群からなる．

定理証明システム本体：インタプリタ版MGTP，フォールディングアップ機能付MGTP，インタプリタ版制約MGTP，項書換え機能付MGTP
前処理システム：値域限定検査器，DOM述語挿入器，MERC法照合パターン生成器，MGTP節コンパイラ，NHM変換器，不要節除去器，TPTP-to-MGTP節変換器
GUIシステム

KLIC 2.002 以上が稼働していること．
Tcl/Tkが稼働していること(GUIを利用する場合)

以下の UNIX システムでは動作を確認しています．

Sun SparcStation 10 running SunOS 5.3 (Solaris 2.3) with gcc-2.6.3
Sun SparcStation 10 running SunOS 5.4 (Solaris 2.4) with gcc-2.6.3
Sun Ultra 1 running SunOS 5.5 (Solaris 2.5) with gcc-2.6.3
Gateway P5-120 and P5-133 running Linux 1.3.9 (Slackware 2.3.0) with gcc-2.6.3
Cray SuperServer 6400 running CRS-OS 5.4 with gcc-2.6.3

アーカイブファイルには以下のディレクトリが含まれます．