In this article we extend BDDs (binary decision diagrams) for plain propositional logic to the fragment of first order logic, consisting of quantifier free logic with equality, zero and successor. We insert equations with zero and successor in BDDs, and call these objects (0,S,=)-BDDs. We extend the notion of {em Ordered} BDDs in the presence of equality, zero and successor. (0,S,=)-BDDs can be transformed to equivalent Ordered (0,S,=)-BDD s by applying a number of rewrite rules. All paths in these extended OBDDs are satisfiable. The major advantage of transforming a formula to an equivalent Ordered (0,S,=)-BDD is that on the latter it can be observed in constant time whether the formula is a tautology, a contradiction, or just satisfiable.

Subsystems of classical logic (including intuitionistic logic) (msc 03B20), Decidability of theories and sets of sentences (msc 03B25), Mechanization of proofs and logical operations (msc 03B35), Logic in computer science (msc 03B70), Theorem proving (deduction, resolution, etc.) (msc 68T15)
CWI
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

Badban, B, & van de Pol, J.C. (2002). Two solutions to incorporate zero, successor and equality in binary decision diagrams. Software Engineering [SEN]. CWI.