二分決定グラフによるモデル生成木の刈込み

• Item type: SIG Technical Reports(1)
• 公開日: 2001-07-23
• タイトル: 二分決定グラフによるモデル生成木の刈込み
• タイトル / 言語: en
• タイトル: Pruning Model Generation Proof Tree with Binary Decision Diagrams
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 九州大学大学院システム情報科学府
• 著者所属: 九州大学大学院システム情報科学研究院
• 著者所属: 九州大学大学院システム情報科学研究院
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Electrical Engineering, Kyushu University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Electrical Engineering, Kyushu University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Electrical Engineering, Kyushu University
• 著者名: 岡, 雄一郎; 越村, 三幸; 長谷川, 隆三
• 著者名(英): Yuuichirou, Oka; Miyuki, Koshimura; Ryuzo, Hasegawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 論理関数を計算機上で表現する方法として二分決定グラフ(BDD)があり，論理演算や恒偽，恒真性の判定を効率よく計算できるとされている．これをモデル生成法に基づく一階述語定理証明システムMGTPに組み込むことによりMGTPが生成するモデル生成木を刈り込むことができる．本研究では，実際にBDDを組み込んだMGTPを実装し，従来のMGTPと性能を比較した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11135936
• 書誌情報: 情報処理学会研究報告知能と複雑系（ICS）; 巻 2001, 号 73(2001-ICS-125), p. 1-8, 発行日 2001-07-23
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会