An Algorithm to Verify Formulas by means of (0,S,=)-BDDs
محل انتشار: نهمین کنفرانس سالانه انجمن کامپیوتر ایران
سال انتشار: 1382
نوع سند: مقاله کنفرانسی
زبان: انگلیسی
مشاهده: 1,688
فایل این مقاله در 9 صفحه با فرمت PDF قابل دریافت می باشد
- صدور گواهی نمایه سازی
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
ACCSI09_110
تاریخ نمایه سازی: 4 بهمن 1386
چکیده مقاله:
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.
کلیدواژه ها:
نویسندگان
Bahareh Badban
Amsterdam, The Netherlands
Jaco van de Pol
Amsterdam, The Netherlands