Presentation	2001/7/16 Pruning Model Generation Proof Tree with Binary Decision Diagrams Yuuichirou Oka, Miyuki Koshimura, Ryuzo Hasegawa,
PDF Download Page	PDF download Page Link
Abstract(in Japanese)	(See Japanese page)
Abstract(in English)	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.
Keyword(in Japanese)	(See Japanese page)
Keyword(in English)	Model Generation / Binary Decision Diagram
Paper #	OFS2001-6,AI2001-11
Date of Issue

Conference Information
Committee	AI
Conference Date	2001/7/16(1days)
Place (in Japanese)	(See Japanese page)
Place (in English)
Topics (in Japanese)	(See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To	Artificial Intelligence and Knowledge-Based Processing (AI)
Language	JPN
Title (in Japanese)	(See Japanese page)
Sub Title (in Japanese)	(See Japanese page)
Title (in English)	Pruning Model Generation Proof Tree with Binary Decision Diagrams
Sub Title (in English)
Keyword(1)	Model Generation
Keyword(2)	Binary Decision Diagram
1st Author's Name	Yuuichirou Oka
1st Author's Affiliation	Graduate School of Information Science and Electrical Engineering Kyushu University()
2nd Author's Name	Miyuki Koshimura
2nd Author's Affiliation	Graduate School of Information Science and Electrical Engineering Kyushu University
3rd Author's Name	Ryuzo Hasegawa
3rd Author's Affiliation	Graduate School of Information Science and Electrical Engineering Kyushu University
Date	2001/7/16
Paper #	OFS2001-6,AI2001-11
Volume (vol)	vol.101
Number (no)	210
Page	pp.pp.-
#Pages	8
Date of Issue