LogicalExpand

expr rewritten as a disjunction of conjunctions (DNF), with Implies/Equivalent/Xor/Nand/Nor eliminated.

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

LogicalExpand(expr)expr, boolean-connective-eliminated and distributed into an Or of Ands

Typed signatures

Type	Package	Applies
(any) -> any	combinatorics	always

Domain: Collections

Details

• Structural, not type-inferring: And/Or/Not/Implies/Equivalent/Xor/Nand/Nor are walked by operator, so a bare symbol is a boolean variable here regardless of what compute-engine would otherwise infer its type to be.
• Implies(a, b) becomes Or(Not(a), b); Xor and Equivalent are eliminated via their pairwise expansions before distribution; Nand/Nor become Not(And(...))/Not(Or(...)).
• A term with both a literal and its negation (a contradiction) is dropped; an empty result (no satisfiable term) is False.
• Every And/Or's operands are sorted and deduplicated by their serialized form for a deterministic result — the same input always prints the same way.
• Anything not one of the eight connectives above (a plain symbol, a comparison, a predicate call) is an opaque literal.

Examples

Basic #

live ↗

In$\mathrm{LogicalExpand}(p\implies b)$Out${{b}}∨¬{{p}}$

live ↗

In$\mathrm{LogicalExpand}(p∧¬(q∨r))$Out${{p}}∧¬{{q}}∧¬r$

Scope #

live ↗

In$\mathrm{LogicalExpand}(p∧(b∨r))$Out${{b}}∧{{p}}∨{{p}}∧r$

live ↗

In$\mathrm{LogicalExpand}(p\veebar b)$Out${{b}}∧¬{{p}}∨{{p}}∧¬{{b}}$

live ↗

In$\mathrm{LogicalExpand}(p∧¬p)$Out$\mathrm{False}$

The law of excluded middle collapses to True

live ↗

In$\mathrm{LogicalExpand}(a∨¬a)$Out$\mathrm{True}$

A contradiction collapses to False

live ↗

In$\mathrm{LogicalExpand}(a∧¬a)$Out$\mathrm{False}$

Equations are kept as atoms; the absorbed term drops

live ↗

In$\mathrm{LogicalExpand}(x=a∧y=b∨x=a∨y=b)$Out$x=a∨y=b$

live ↗

In$\mathrm{LogicalExpand}((a∨b)∧¬(c∨d∨k))$Out${{a}}∧¬{{c}}∧¬{{d}}∧¬{{k}}∨{{b}}∧¬{{c}}∧¬{{d}}∧¬{{k}}$

live ↗

In$\mathrm{LogicalExpand}(p\veebar q\veebar r)$Out${{p}}∧{{q}}∧r∨{{p}}∧¬{{q}}∧¬r∨{{q}}∧¬{{p}}∧¬r∨r∧¬{{p}}∧¬{{q}}$

Applications #

A symbol is already expanded

live ↗

In$\mathrm{LogicalExpand}(t)$Out$t$

Properties #

De Morgan: the negation of an Or is the And of negations

live ↗

In$\mathrm{LogicalExpand}(¬(a∨b))$Out$¬{{a}}∧¬{{b}}$

De Morgan the other way: negated And becomes Or of negations

live ↗

In$\mathrm{LogicalExpand}(¬(a∧b))$Out$¬{{a}}∨¬{{b}}$

About

Examples	13
Checked against	Wolfram Language 13 agree
Crosswalk	Wolfram Language

See also: BooleanConvert