(90) MGTP/G (KL1版/KLIC版)


	マ シ ン：PIM/UNIXマシン
	環　　境：PIMOS/UNIX, KLIC
	言　　語：KL1, Prolog
	ソース量：160 KB
	文　　書：ユーザーズマニュアル (日本語・英語)

概要

ノンホーン節を対象にするグランド版定理証明器MGTP/Gの処理系

特徴

機能

MGTP/G ( Model Generation Theorem Prover/Ground Version ) は，モデル生 成法に基づく一階述語論理の定理証明システムである．問題は以下のような含 意形式の節で与えられる．この節は、Prolog で記述されたプリプロセッサに よって KL1 節に変換される。

ここで，→ の左側 (前件部) はアトムの連言 ( , )、右側 ( 後件部 ) はア トムの選言 ( ; ) である．n = 0 の時は，初期モデル (ファクト群) を表し，m = 0 の時，矛盾を表す．初期モデルを種とし，上記の節に 従って左辺から右辺へ前向きに推論が進められる．後件部が複数のアトムから なる場合 (ノンホーン節)，ケース分割によって独立に推論が進められるので 木構造の証明が得られる．

MGTP/G は，「後件部に現れる変数は，全て前件部に現れる」という値域限定 性を満たす節のみを扱っているため，証明途中で生成されるアトムは全て変数 を含まないことが保証される．これにより，単一化やケース分割時の共有変数 に関する処理が必要でなくなり，効率的実装が可能になる．モデル要素の高速 検索のために項メモリ，連言照合を高速に行なうための節インデックス機能も 実装されている．

値域限定という制約があるものの，ほとんどの AI 応用にこれで対処しうる． 失敗による否定，仮説推論，様相論理等の有用な枠組を推論規則によって表現 することにより容易に実現することができる．

ＦＴＰ

www-admin@icot.or.jp