Pruning model generation proof tree with binary decision diagrams

Yuuichirou Oka, Ryuzo Hasegawa, Miyuki Koshimura

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish
Pages (from-to)49-54
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Issue number1
Publication statusPublished - Jan 1 2003

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering


Dive into the research topics of 'Pruning model generation proof tree with binary decision diagrams'. Together they form a unique fingerprint.

Cite this