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.
|Number of pages||6|
|Journal||Research Reports on Information Science and Electrical Engineering of Kyushu University|
|Publication status||Published - Jan 1 2003|
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Electrical and Electronic Engineering