Pruning model generation proof tree with binary decision diagrams

Yuuichirou Oka; Ryuzo Hasegawa; Miyuki Koshimura

Pruning model generation proof tree with binary decision diagrams

Yuuichirou Oka, Ryuzo Hasegawa, Miyuki Koshimura

Intelligence Science

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	49-54
Number of pages	6
Journal	Research Reports on Information Science and Electrical Engineering of Kyushu University
Volume	8
Issue number	1
Publication status	Published - Jan 1 2003

All Science Journal Classification (ASJC) codes

Computer Science(all)
Electrical and Electronic Engineering

Cite this

@article{07c40a46e8824c4bb8352dd2391d3c2b,

title = "Pruning model generation proof tree with binary decision diagrams",

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.",

author = "Yuuichirou Oka and Ryuzo Hasegawa and Miyuki Koshimura",

year = "2003",

month = jan,

day = "1",

language = "English",

volume = "8",

pages = "49--54",

journal = "Research Reports on Information Science and Electrical Engineering of Kyushu University",

issn = "1342-3819",

publisher = "Kyushu University, Faculty of Science",

number = "1",

}

TY - JOUR

T1 - Pruning model generation proof tree with binary decision diagrams

AU - Oka, Yuuichirou

AU - Hasegawa, Ryuzo

AU - Koshimura, Miyuki

PY - 2003/1/1

Y1 - 2003/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0037498192&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0037498192&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0037498192

SN - 1342-3819

VL - 8

SP - 49

EP - 54

JO - Research Reports on Information Science and Electrical Engineering of Kyushu University

JF - Research Reports on Information Science and Electrical Engineering of Kyushu University

IS - 1

ER -

Pruning model generation proof tree with binary decision diagrams

Abstract

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this