| 講演名 | 2001/7/16 二分決定グラフによるモデル生成木の刈込み 岡 雄一郎, 越村 三幸, 長谷川 隆三, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 論理関数を計算機上で表現する方法として二分決定グラフ(BDD)があり、論理演算や恒偽、恒真性の判定を効率よく計算できるとされている。これをモデル生成法に基づく一階述語定理証明システムMGTPに組み込むことによりMGTPが生成するモデル生成木を刈り込むことができる。本研究では、実際にBDDを組み込んだMGTPを実装し、従来のMGTPと性能を比較した。 |
| 抄録(英) | Binary Decision Diagram(BDD)is a data structure that expresses Boolean expressions on computers. We can effectively manipulate Boolean expressions and determine their satisfiability with BDDs. We can enhance proving power of MGTP (Model Generation Theorem Prover) by pruning proof tree of MGTP using BDDs. We implement MGTP with BDD, and compare it with standard MGTP. |
| キーワード(和) | モデル生成法 / 二分決定グラフ |
| キーワード(英) | Model Generation / Binary Decision Diagram |
| 資料番号 | OFS2001-6,AI2001-11 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2001/7/16(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 二分決定グラフによるモデル生成木の刈込み |
| サブタイトル（和） | |
| タイトル（英） | Pruning Model Generation Proof Tree with Binary Decision Diagrams |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル生成法 / Model Generation |
| キーワード(2)（和/英） | 二分決定グラフ / Binary Decision Diagram |
| 第 1 著者 氏名（和/英） | 岡 雄一郎 / Yuuichirou Oka |
| 第 1 著者 所属（和/英） | 九州大学大学院システム情報科学府 Graduate School of Information Science and Electrical Engineering Kyushu University |
| 第 2 著者 氏名（和/英） | 越村 三幸 / Miyuki Koshimura |
| 第 2 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 Graduate School of Information Science and Electrical Engineering Kyushu University |
| 第 3 著者 氏名（和/英） | 長谷川 隆三 / Ryuzo Hasegawa |
| 第 3 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 Graduate School of Information Science and Electrical Engineering Kyushu University |
| 発表年月日 | 2001/7/16 |
| 資料番号 | OFS2001-6,AI2001-11 |
| 巻番号（vol） | vol.101 |
| 号番号（no） | 210 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |