سیویلیکا را در شبکه های اجتماعی دنبال نمایید.

An Algorithm to Verify Formulas by means of (0,S,=)-BDDs

Publish Year: 1382
Type: Conference paper
Language: English
View: 1,786

This Paper With 9 Page And PDF Format Ready To Download

Export:

Link to this Paper:

Document National Code:

ACCSI09_110

Index date: 24 January 2008

An Algorithm to Verify Formulas by means of (0,S,=)-BDDs abstract

In this article we provide an algorithm to verify formulas of the fragment of rst order logic, consisting of quanti er free logic with zero, successor and equality. We rst develop a rewrite system to extract an equivalent Ordered (0; S; =)-BDD from any given (0; S; =)-BDD. Then we show completeness of the rewrite system. Finally we make an algorithm with the same result as the rewrite system. Given an Ordered (0; S; =)-BDDs we are able to see in constant time whether the formula is a tautology, a contradiction, or only satis able.

An Algorithm to Verify Formulas by means of (0,S,=)-BDDs Keywords:

An Algorithm to Verify Formulas by means of (0,S,=)-BDDs authors

Bahareh Badban

Amsterdam, The Netherlands

Jaco van de Pol

Amsterdam, The Netherlands