Is the minimal conjunctive normal form for positive formula unique? If so, how do you calculate it? I am considering positive Boolean formulas (no negations). Take for example $A$. Here are two of its positive conjunctive normal forms.
$$A$$
$$A \land (A \lor B)$$
The minimal example is $A$.
Does every positive boolean formula have a unique minimal conjunctive normal form? If so, how does one calculate it?
(I conjecture that you can do so by finding a positive conjuctive normal form, and then pruning any terms that are implied by other terms (for example, $A \lor B$ is implied by the previous term $A$, so it gives no additional information in a conjuction). I don't know how to prove that this is correct, if it is so. (It is also not very efficient.))
 A: This showed up on the Wikipedia Math Help Desk, see 1. It looks like the minimal expression is unique for positive expressions.
Proof: Let S and T be two equivalent positive expressions in CNF which are both minimal. Let {Si} be the set of clauses in S and {Tj} be the set of clauses in T. Each Si and Tj, in turn, corresponds to a subset of a set of Boolean variables {xk}. Since S is minimal, no Si is contained in Sj for j≠i, and similarly for T. For each assignment a:xk → {T, F}, define Z(a) to be the set of variables for which a is F, i.e. Z(a) is the compliment of the support of a. A clause Si evaluates to F iff Si⊆Z(a) and the expression S evaluates to F iff Si⊆Z(a) for some i. A similar statements holds for T. Fix i and define the truth assignment ai(xk) to be T when xk is not in Si, in other words ai is the truth assignment so that Z(ai) = Si. The clause Si evaluates to F under this assignment, so S evaluates to F. But S and T are equivalent so T evaluates to F. Therefore Tj⊆Z(ai)= Si for some j. Similarly, for each j there is k so that Sk ⊆ Tj. (I think another way of saying this is that S and T are refinements of each other.) If Si is an element of S, then there is Tj in T so that Tj ⊆ Si, and there is an Sk so that Sk ⊆ Tj. Then Sk ⊆ Si and so, since ''S'' is minimal, i=k. We then have Si ⊆ Tj ⊆ Si, Si = Tj ∈ T. So S ⊆ T and similarly T ⊆ S, therefore S = T. 
Another (probably better) approach is to characterize the clauses that appear. 
