Creator |
|
|
|
Language |
|
Publisher |
|
|
Date |
|
Source Title |
|
Vol |
|
Issue |
|
First Page |
|
Last Page |
|
Publication Type |
|
Access Rights |
|
JaLC DOI |
|
Related DOI |
|
Related URI |
|
Relation |
|
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
|