An Algorithm to Verify Formulas by means of (0,S,=)-BDDs
Publish place: 9th Annual Conference of Computer Society of Iran
Publish Year: 1382
نوع سند: مقاله کنفرانسی
زبان: English
View: 1,666
This Paper With 9 Page And PDF Format Ready To Download
- Certificate
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
ACCSI09_110
تاریخ نمایه سازی: 4 بهمن 1386
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.
Keywords:
Authors
Bahareh Badban
Amsterdam, The Netherlands
Jaco van de Pol
Amsterdam, The Netherlands