（８１）並列定理証明器：ＭＧＴＰ／Ｇ　Ｐｒｏｌｏｇ版


	マ シ ン：UNIX/PC
	環　　境：UNIX/MS-DOS
	言　　語：Prolog
	ソース量：60 KB
	文　　書：ユーザーズマニュアル (日本語／英語)

概要

ノンホーン節を対象にするグランド版ＭＧＴＰ／Ｇの処理系

特徴

機能

MGTP/G(Model Generation Theorem Prover/Ground Version)は、モデル生成法 に基づく一階述語論理の定理証明システムである。問題は以下のような含意形 式の節で与えられる。

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

ＭＧＴＰ／Ｇは、「後件部に現れる変数は、全て前件部に現れる」という値域 限定性を満たす節のみを扱っているため、証明途中で生成されるアトムは全て 変数を含まないことが保証される。これにより、単一化やケース分割時の共有 変数に関する処理が必要でなくなり、効率的実装が可能になる。アトムの高速 検索のために項メモリも実装されている。

値域限定という制約があるものの、ほとんどのＡＩ応用にこれで対処しうる。 失敗による否定、仮説推論、様相論理等の有用な枠組みを推論規則によって表 現することにより容易に実現することができる。さらに、ボトムアップとトッ プダウンを融合するノンホーンマジックセット法により、探索空間の大幅な改 善がなされる。

ＦＴＰ

www-admin@icot.or.jp