Distributive expansion of CNF and implicants I am looking for references for the following theorems.

Theorem 1: Distributive expansion of a CNF formula $P_c$ (product of sums)
results in a DNF formula (sum of products) consisting of all prime
implicants for $P_c$. $P_c$ is called a Blake canonical form BCF.

Theorem 2: If we transform a disjunctive clause $C_d$ with $k$ literals to a
disjunctive clause of conjunctions $C_m$ by replacing each literal
$l_i, i = (1, ..., k)$ with the conjunction $(\neg l_1 \wedge
... \wedge \neg l_{i-1} \wedge l_i)$, then $C_m$ will be logically equivalent to $C_d$. The clause $C_m$ is called a
clause with maximized conflicts.

Distributive expansion of $C_m$ shows that it is logically
equivalent to the unmaximized clause $C_d$, $C_m = C_d$.

Theorem 3: Distributive expansion of a CNF formula with maximized conflicts
$P_m$ (product of sums of products), with simplification of
outermost clauses before innermost clauses, results in a DNF
formula $P_u$ (sum of products) defining a set of (not
necessarily prime) implicants $I_u$ for $P_m$. The
implicants from $I_u$ cover all possible solutions for
$P_m$.  The implicants $I_u$ are unique, in that no
implicant $M_i \in I_u$ covers the solutions of any other
implicant $M_j \in I_u, i \ne j$.

Motivation:

With the discussion in [BROWN] I have finally found the last
piece of the puzzle.

Obviously, the restrictions for syllogistic formulae --- namely
removal of duplicate literals and elimination of clauses with
contradictory literals --- have been loosened over time. However, this
seems to have been a process of ad hoc reasoning.

I am missing an exhaustive formal discussion of the
consequences. I.e., the set of logically equivalent DNFs
represented by their minimal form of a disjunction of "atomic"
literals and the influence on the resulting DNFs of partial
assignments, which always cover all possible solutions, albeit in
different ways.

In order to find out, whether I have to do all of that on my own,
I use theorem 3 to show, that besides the well-known Blake canonical
form BCF, other non-trivial DNFs of implicants with different
properties appear, when the input clauses are generalized from
CNF to allow non-syllogistic representations, namely the DNFs
from theorem 2. Since that also requires a different order of
evaluation which is highly non-intuitive to simplification
junkies, I assume that I am out of luck.

It can especially be shown that for selection problems in "direct
encoding" (Chapter 2, Handbook of Satisfiability), the input based on theorem 2 alone allows a CDCL solver to solve the problem with
significantly less decisions than with plain CNF. Small problems
(currently 40 variables, 171 clauses) are even solved earlier with the
generally less effective "direct encoding" than with the original CNF
encoding. Note, that there is actually never a set of implicants
generated in that case.

I have prepared a PDF with examples to illustrate the effects.
Theorem 1 is related to Blake canonical form.

The Wikipedia article refers to


Brown, Frank Markham, Boolean Reasoning: The Logic of Boolean Equations,


which in turn references


Canonical expressions in Boolean algebra. Ph.D. dissertation U (1937)).