سال انتشار: ۱۳۸۲

محل انتشار: نهمین کنفرانس سالانه انجمن کامپیوتر ایران

تعداد صفحات: ۹

نویسنده(ها):

Bahareh Badban – Amsterdam, The Netherlands
Jaco van de Pol – Amsterdam, The Netherlands

چکیده:

In this article we provide an algorithm to verify formulas of the fragment ofrst order logic, consisting of quanti er free logic with zero, successor and equality. Werst 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.