An Algorithm to Verify Formulas by means of (0,S,=)-BDDs
عنوان مقاله: An Algorithm to Verify Formulas by means of (0,S,=)-BDDs
شناسه ملی مقاله: ACCSI09_110
منتشر شده در نهمین کنفرانس سالانه انجمن کامپیوتر ایران در سال 1382
شناسه ملی مقاله: ACCSI09_110
منتشر شده در نهمین کنفرانس سالانه انجمن کامپیوتر ایران در سال 1382
مشخصات نویسندگان مقاله:
Bahareh Badban - Amsterdam, The Netherlands
Jaco van de Pol - Amsterdam, The Netherlands
خلاصه مقاله:
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 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.
کلمات کلیدی: lgorithm, Decision Diagrams, Equality, Theorem proving, Decision Procedure, Natu- ral numbers
صفحه اختصاصی مقاله و دریافت فایل کامل: https://civilica.com/doc/45821/