A BDD Representation for Positive Equational Formulas

A positive equational formula (PEF) is a negation-free open formula in the language of pure equality. In this paper, we present a normal form for positive equational formulas that lends itself readily to the representation of such formulas using ordered binary decision diagrams (BDDs) whose nodes are labeled by equations. In contrast to previous work of Groote and van de Pol that treated the larger class of equational formulas with negation, we show that our normal forms for PEFs are unique in the sense that two normal forms are logically equivalent if and only if they are identical. This result means that a BDD-based representation of our normal forms can implement equivalence checking for PEFs in constant time, as well as avoid space inefficiency that could otherwise result from storing multiple syntactically distinct variants of a formula. We present a recursive algorithm that traverses an arbitrary PEF given as input and builds an equivalent normal form in a bottomup fashion. In addition, we apply ideas from the reduction algorithm to obtain bottom-up, normal-form-preserving algorithms for various logical