Logic & Boolean Algebra

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.

(OrangeLink[Logical Operators, paclet:guide/BooleanComputation])

(RefLink[True, paclet:ref/True]), (RefLink[False, paclet:ref/False]) — symbolic truth values

(RefLink[Boole, paclet:ref/Boole]) — convert symbolic truth values to 0 and 1

(OrangeLink[Boolean Computation », paclet:guide/BooleanComputation])

(RefLink[BooleanFunction, paclet:ref/BooleanFunction]) — general Boolean function

Mathematical Logic

(RefLink[FullSimplify, paclet:ref/FullSimplify]) — simplify logic expressions and prove theorems

(RefLink[ForAll, paclet:ref/ForAll]) ((RefLink[∀, paclet:ref/ForAll])), (RefLink[Exists, paclet:ref/Exists]) ((RefLink[∃, paclet:ref/Exists])) — quantifiers

(OrangeLink[Automated Theorem Proving », paclet:guide/TheoremProving])

(RefLink[FindEquationalProof, paclet:ref/FindEquationalProof]) — generate representations of proofs in equational logic

Boolean Vector Operations

(RefLink[Nearest, paclet:ref/Nearest]), (RefLink[FindClusters, paclet:ref/FindClusters]) — operate on Boolean vectors