Research and algorithms in the theory of Boolean formulas

Several algorithms are presented, more or less directly related to the "minimization" theory of Boolean formulas. They give solutions to the following specific problems: computation of the sum of all the "prime implicants", starting with any "normal" formula; verification of the equivalence F a/ for "normal" formulas F; determination of some or all of the minimal F-including sets. The last problem is a two-fold generalization of the determination of the "irredundant normal formulas". More precisely if F, F1, F2,..., Fn are Boolean formulas such that F is included in ("implies") SigmaFi, a minimal F-including set is a collection of Fi such that their sum includes F, but no subcollection has the same property. Although these algorithms are of obvious practical importance, they are viewed here more as a theoretical contribution. Examples are included; the theory of Boolean formulas on which this paper is based is presented elsewhere.