The Wolfram Language represents Boolean expressions in symbolic form, so they can not only be evaluated, but also be symbolically manipulated and transformed. Incorporating state-of-the-art quantifier elimination, satisfiability, and equational logic theorem proving, the Wolfram Language provides a powerful framework for investigations based on Boolean algebra.

Logical Operators »

And(&&, ∧)  ▪  Or(||, ∨)  ▪  Not(!,¬)  ▪  Nand(⊼)  ▪  Nor(⊽)  ▪  Xor(⊻)  ▪  Implies()  ▪  Equivalent(⧦)  ▪  Equal(==)  ▪  Unequal(!=)  ▪  ...

True, False — symbolic truth values

Boole — convert symbolic truth values to 0 and 1

AllTrue  ▪  AnyTrue  ▪  NoneTrue

Boolean Computation »

BooleanFunction — general Boolean function

BooleanConvert  ▪  BooleanMinimize  ▪  SatisfiableQ  ▪  ...

Mathematical Logic

FullSimplify — simplify logic expressions and prove theorems

ForAll (∀), Exists (∃) — quantifiers

Resolve  ▪  Reduce  ▪  FindInstance

Automated Theorem Proving »

FindEquationalProof — generate representations of proofs in equational logic

ProofObject  ▪  AxiomaticTheory  ▪  ...

Boolean Vector Operations

Nearest, FindClusters — operate on Boolean vectors

HammingDistance  ▪  MatchingDissimilarity  ▪  ...