Pruning Model Generation Proof Tree with Binary Decision Diagrams - Collections | Kyushu University Library

＜departmental bulletin paper＞
Pruning Model Generation Proof Tree with Binary Decision Diagrams

Creator	Creator Name 岡, 雄一郎 Oka, Yuichiro オカ, ユウイチロウ Affiliation Affiliation Name 九州大学大学院システム情報科学府知能システム学専攻 : 修士課程 Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University : Master's Program
	Creator Name 長谷川, 隆三 Hasegawa, Ryuzo ハセガワ, リュウゾウ Affiliation Affiliation Name 九州大学大学院システム情報科学研究院知能システム学部門 Department of Intelligent Systems, Faculty of Information Science and Electrical Engineering, Kyushu University
	Creator Name 越村, 三幸 Koshimura, Miyuki コシムラ, ミユキ Affiliation Affiliation Name 九州大学大学院システム情報科学研究院知能システム学部門 Department of Intelligent Systems, Faculty of Information Science and Electrical Engineering, Kyushu University
Language	Japanese
Publisher	九州大学大学院システム情報科学研究院
Publisher	Faculty of Information Science and Electrical Engineering, Kyushu University
Date	2003-03-26
Source Title	Research reports on information science and electrical engineering of Kyushu University
Vol	8
Issue	1
First Page	49
Last Page	54
Publication Type	Version of Record
Access Rights	open access
JaLC DOI	https://doi.org/10.15017/1515817
Related DOI	https://portal.isee.kyushu-u.ac.jp/
Related URI	https://portal.isee.kyushu-u.ac.jp/
Relation	https://portal.isee.kyushu-u.ac.jp/
Abstract	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 the proving power of MGTP (Model Generation Theorem Prover) by pruning proof tree of MGTP using BDDs. In this paper, we propose a method which postpones updating BDD in order to suppress memory consumption and compare its performance with standard MGTP and a previous version of MGTP with BDDs.show more

Hide fulltext details.

File	FileType	Size	Views	Description
p049	pdf	518 KB	158

Details

PISSN	1342-3819
EISSN	2188-0891
NCID	AN10569524
Record ID	1515817
Peer-Reviewed	Refereed
Subject Terms	モデル生成
	Model generation
	二分決定グラフ
	Binary decision diagram(BDD)
	自動定理証明
	Automated theorem proving
	証明木
	Proof tree
Created Date	2015.05.29
Modified Date	2020.11.02