| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 423436 | Electronic Notes in Theoretical Computer Science | 2009 | 16 Pages |
Abstract
We provide an automatic verification for a fragment of FOL quantifier-free logic with zero, successor and equality. We use BDD representation of such formulas and to verify them, we first introduce a (complete) term rewrite system to generate an equivalent Ordered (0,S,=)-BDD from any given (0,S,=)-BDD. Having the ordered representation of the BDDs, one can verify the original formula in constant time. Then, to have this transformation automatically, we provide an algorithm which will do the whole process.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
