BooleanConvert

expr rewritten in the given boolean normal form — "DNF" (default), "CNF", or "NNF".

✓ checked against that system · ! checked, with disagreements (hover a chip)Wolfram LanguageBooleanConvert!

BooleanConvert(expr)expr in disjunctive normal form (an Or of Ands) — same as LogicalExpand

BooleanConvert(expr, "CNF")expr in conjunctive normal form (an And of Ors)

BooleanConvert(expr, "NNF")expr with Not pushed to the leaves, but And/Or left in their original nesting shape (not distributed)

Typed signatures

Type	Package	Applies
`(any, string?) -> any`	`combinatorics`	always

Domain: Collections

Details

"DNF" and "CNF" are Wolfram's own forms. "NNF" is an extension of ours — Wolfram 15's BooleanConvert has no "NNF" form (BooleanConvert(expr, "NNF") stays unevaluated there); we implement it anyway since it falls straight out of the same elimination pipeline, and it is documented here as a divergence rather than a Wolfram form.
Other Wolfram forms ("ESOP", "AC", "BF", …) are left unevaluated rather than approximated.
Shares LogicalExpand's elimination of Implies/Equivalent/Xor/Nand/Nor and its deterministic sort/dedup of every And/Or's operands.
A CNF clause with both a literal and its negation (a tautology) is dropped; an all-dropped result is True.
Clauses that differ only in one literal's polarity merge and absorbed clauses drop, so Implies(b, b) is True and b ∧ ¬b is False, as in Wolfram. This is not a full minimizer.