An Algorithm to Verify Formulas by means of (O,S,=)-BDDs
Bahareh Badban, J.C. van dePol · Data Archiving and Networked Services (DANS) · 2004
In this article we provide an algorithm to verify formulas of the fragment of first order logic, consisting of quantifier free logic with zero, successor and equality.We first 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 satisfiable.