The MGTP Primer

Model Generation Theorem Prover

Draft Version


このページでは、ボトムアップ型定理証明システム MGTP (Model Generation Theorem Prover) に関する基礎知識と利用方法に関する説明を行なう。

MGTP の基本原理を理解するために、特別な基礎的知識は前提としないが、 MGTP の処理系は、KL1 と Prolog で書かれたものを対象としているので、 処理系の詳細を理解するためには、論理型言語に関する基礎的な知識が必要 である。 なお、KL1に関しては、 AITEC のホームページを参照されたい。


MGTP とは ?
グラウンド版 MGTP
ノングラウンド版 MGTP
制約 MGTP
演習問題
参考文献


MGTP のトップページに戻る

shirai@mri.co.jp