A Correct Optimized Algorithm for Incrementally Generating Prime Implicates

In response to the demands of some applications, we had developed an algorithm, called IPIA, to incrementally generate the prime implicates/implicants of a set of clauses. In an attempt to improve IPIA some optimizations were also presented. It was pointed out to us that some of these optimizations, namely the subsumption and history restriction, are self conflicting. Subsumption is a necessary operation to guarantee the primeness of implicates/implicants and history restriction is a scheme that exploits the history of consensus operation to avoid generating non prime implicant/implicates. The original IPIA, where history restriction was not consider, was proven correct. However, when {\em history restriction} was introduced later in the optimized version, it interacted with the subsumption operation to produce an incomplete set of prime implicants/implicates. This paper explains the problem in more details, proposes a solution and provides a proof of its correctness.