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

• Item type: Journal(1)
• 公開日: 1996-01-15
• タイトル: MGTP：並行論理型言語KL1によるモデル生成型定理証明系
• タイトル / 言語: en
• タイトル: MGTP : A Model Generation Theorem Prover in the Concurrent Logic Programming Language KL1
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: 人工知能
• 著者所属: 九州大学工学部電子工学科
• 著者所属: 三菱電機（株）先端技術総合研究所
• 著者所属(英): en
• 著者所属(英): Department of Electronics, Kyushu University
• 著者所属(英): en
• 著者所属(英): Mitsubishi Electric Corporation, Advanced Technology R&D Center
• 著者名: 長谷川, 隆三; 藤田, 博
• 著者名(英): Ryuzo, Hasegawa; Hiroshi, Fujita
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 一階述語論理のための定理証明系を、モデル生成法に基づき並行諭理型書語KL1で効率良く実現する方法について述べる。モデル生成法においては、値域限定という条件を満たす節集合を対象とした場合、出現検査付き単一化が不要であり、照合操作で十分となる。その結果、入力節中の変数を直接KL1変数で表現することができ、入力節に対する単一化をKL1節の頭部単一化として実行できるなど、KL1言語処理系を活用した効率の良い実装が可能となった。しかしながら、モデル生成法で支配的な計算量を占める連言照含手続きを効率良く実現することはそれほど容易ではない。我々は、連言照合手続きに含まれる冗長計算を除くため、2つの方式を考案して比較検討した。両方式ともコーディング手法としてKL1に特化されたものであるが、一般的に前向き推諭系の効率的実装技術としてKL1以外の実装言語を用いた場合にも有効な技術である。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 37, 号 1, p. 1-12, 発行日 1996-01-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764