An Algorithm to Verify Formulas by means of (0,S,=)-BDDs
Publish place: 9th Annual Conference of Computer Society of Iran
Publish Year: 1382
Type: Conference paper
Language: English
View: 1,786
This Paper With 9 Page And PDF Format Ready To Download
- Certificate
- I'm the author of the paper
Export:
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