講演名 2002/5/17
ブール制約解消系によるモデル生成木の刈込み(<特集>自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
越村 三幸, 長谷川 隆三,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 本論文では,モデル生成法による証明から冗長性を削除する簡便な手法を提案する.本手法は,「ブール制約」を用いるもので,ここでブール制約とは証明に用いられた節の基礎例の連言である.ブール制約は補題の集合として用いることができ,これによって冗長な証明分岐や重複証明を除去できる.制約論理型言語を用いて本手法を試験的に実装し,効果を確認した.
抄録(英) We present a simple method for eliminating redundant searches in model generation. The method employs Boolean Constraints which are conjunctions of ground instances of clauses having participated in proofs. Boolean Constraints work as sets of lemmas with which duplicate subproofs and irrelevant model extensions can be eliminated. The method has been tentatively implemented on a constraint logic programming system. We evaluated effects of the method by proving some typical problems.
キーワード(和) モデル生成 / ブール制約解消系 / 制約論理型言語
キーワード(英) Model Generation / Boolean Constraints Solver / Constraint Logic Programming System
資料番号 AI2002-6
発行日

研究会情報
研究会 AI
開催期間 2002/5/17(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Artificial Intelligence and Knowledge-Based Processing (AI)
本文の言語 JPN
タイトル(和) ブール制約解消系によるモデル生成木の刈込み(<特集>自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
サブタイトル(和)
タイトル(英) Pruning Model Generation Tree by a Boolean Constraint Solver
サブタイトル(和)
キーワード(1)(和/英) モデル生成 / Model Generation
キーワード(2)(和/英) ブール制約解消系 / Boolean Constraints Solver
キーワード(3)(和/英) 制約論理型言語 / Constraint Logic Programming System
第 1 著者 氏名(和/英) 越村 三幸 / Miyuki KOSHIMURA
第 1 著者 所属(和/英) 九州大学大学院システム情報科学研究院
Graduate School of Information Science and Electrical Engineering, Kyushu University
第 2 著者 氏名(和/英) 長谷川 隆三 / Ryuzo HASEGAWA
第 2 著者 所属(和/英) 九州大学大学院システム情報科学研究院
Graduate School of Information Science and Electrical Engineering, Kyushu University
発表年月日 2002/5/17
資料番号 AI2002-6
巻番号(vol) vol.102
号番号(no) 91
ページ範囲 pp.-
ページ数 6
発行日