ノンホーンマジックセット法と関連性テストとの等価性

• Item type: Journal(1)
• 公開日: 1997-10-15
• タイトル: ノンホーンマジックセット法と関連性テストとの等価性
• タイトル / 言語: en
• タイトル: The Equivalence between Non - Horn Magic Sets and Relevancy Testing
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: 定期自動証明
• 著者所属: 職業能力開発大学校情報工学科
• 著者所属: 神戸大学工学部電気電子工学科
• 著者所属: 九州大学大学院システム情報科学研究科
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, University of Industrial Technology
• 著者所属(英): en
• 著者所属(英): Department of Electrical and Electronics Engineering, Kobe University
• 著者所属(英): en
• 著者所属(英): Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University
• 著者名: 太田, 好彦; 井上, 克已; 長谷川, 隆三
• 著者名(英): Yoshihiko, Ohta; Katsumi, Inoue; Ryuzo, Hasegawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: モデル生成型定理証明において，証明したいゴール（負節）に無関係である冗長な解釈の生成を避けるための手法がいくつか提案されている．その代表的手法として，SATCHMOREと呼ばれる定理証明器で用いられている関連性テストとホーンマジックセット法を拡張したノンホーンマジックセット法とがある．本論文では，Lovelandらが提案している関連性テストよりも弱い関連性テストを定義し，それとノンホーンマジックセット法との関係を詳細に考察し，その関連性テストに基づくSATCHMOREにより生成される解釈の総数が，ノンホーンマジックセット法によって生成されるそれとつねに同じであることを証明する．すなわち，ノンホーンマジックセットは，証明木の枝刈り能力に関して，弱い関連性テストと等価であることを明らかにする．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: On model generation theorem proving,there are several methods to avoid generating redundant interpretations that are irrelevant to the goal(negative clause)to be proved.As the typical methods,we consider both relevancy testing used in the SATCHMORE prover and non-Horn magic sets that are extensions of Horn magic sets.In this paper,we define a relevancy testing,which is weaker than that proposed by Loveland,et al.Then,we analyze relationships between non-Horn magic sets and weak relevancy testing in detail,and prove that the total number of generated interpretations with non-Horn magic sets is always the same as that with the SATCHMORE prover based on weak relevancy testing.Thus,we find thatnon-Horn magic sets and weak relevancy testing have the same power in pruning redundant branches of a proof tree.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 38, 号 10, p. 1894-1904, 発行日 1997-10-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764