MGTP：並行論理型言語KL1によるモデル生成型定理証明系

• 長谷川, 隆三

• 藤田, 博

書誌事項

タイトル別名

• MGTP : A Model Generation Theorem Prover in the Concurrent Logic Programming Language KL1
• 人工知能

抄録

一階述語論理のための定理証明系を、モデル生成法に基づき並行諭理型書語KL1で効率良く実現する方法について述べる。モデル生成法においては、値域限定という条件を満たす節集合を対象とした場合、出現検査付き単一化が不要であり、照合操作で十分となる。その結果、入力節中の変数を直接KL1変数で表現することができ、入力節に対する単一化をKL1節の頭部単一化として実行できるなど、KL1言語処理系を活用した効率の良い実装が可能となった。しかしながら、モデル生成法で支配的な計算量を占める連言照含手続きを効率良く実現することはそれほど容易ではない。我々は、連言照合手続きに含まれる冗長計算を除くため、2つの方式を考案して比較検討した。両方式ともコーディング手法としてKL1に特化されたものであるが、一般的に前向き推諭系の効率的実装技術としてKL1以外の実装言語を用いた場合にも有効な技術である。

This paper presents novel technique to implement model-generation based theorem provers for first-order logic in the concurrent logic programming language KL1. The model generation method makes it possible to use only matching in place of full-unification with occurs-check if the given clause set satisfies the condition called range-restrictedness. As a consequence, a logical variable in the clause set can be represented with a KL1 variable; unification can be executed directly by the head-unification of a KL1 clause; and many of the KL1 system features can be made available for efficient execution of the theorem provers built upon it. In addition, this paper presents two kinds of methods to eliminate redundant computations in conjunctive matching which would be a primary cause of significant speed-down of the model-generation based theorem provers.

収録刊行物

• 情報処理学会論文誌

  情報処理学会論文誌 37 (1), 1-12, 1996-01-15

  一般社団法人情報処理学会

キーワード

• 論文

詳細情報

• CRID: 1050282812863414272
• NII論文ID: 110002722918
• NII書誌ID: AN00116647
• ISSN: 18827764
• Web Site: http://id.nii.ac.jp/1001/00013735/
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • CiNii Articles