Skip to content

LogicalExpand

Status: Stable

documented, exercised by the test suite and/or worked examples, with no known limitations recorded.

Description

LogicalExpand[expr]

Expands the logical combination expr -- of equations, inequalities and Boolean atoms -- into disjunctive normal form (an Or of Ands), applying distributive, De Morgan, idempotence, complementation and absorption laws, and expanding Implies and Xor. Returns True for a tautology and False for a contradiction. Every non-logical subexpression is treated as an opaque Boolean atom (no domain reasoning), so e.g. x==a and x!=a are complementary literals.

Examples

No verified examples yet for this function.

Algorithm

reduce_companions.c

Companion builtins for `Reduce` (REDUCE_PLAN.md, Phase 8).  v1: LogicalExpand
+ a minimal NotElement head.

LogicalExpand distributes a logical statement to disjunctive normal form (an Or of Ands of literals), applying idempotence / complementation / absorption contractions, and collapsing to True (tautology) or False (contradiction)

when the statement decides.  Every non-connective subexpression is treated as

an OPAQUE Boolean atom -- a symbol, a relation x == a, a membership

`Element[..]` -- with NO domain reasoning, exactly as Mathematica's
LogicalExpand does.  Two relational atoms are complementary iff one is the

(head-flipped) logical negation of the other (x==a / x!=a, x<1 / x>=1,

`Element` / `NotElement`, `a` / `!a`).

The True/False collapse is sound and complete without truth-table enumeration: over independent opaque atoms a DNF is unsatisfiable iff every clause holds a complementary pair -- i.e. it distributes to ZERO surviving

clauses.  So `phi` empty => False, and `Not[phi]` empty => True (the negation

is unsatisfiable, hence phi is a tautology).

Implementation notes

Attributes: Protected.

References

See also: Implies, Xor, Reduce, Element, NotElement