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.
Boole — convert symbolic truth values to 0 and 1
BooleanFunction — general Boolean function
FullSimplify — simplify logic expressions and prove theorems
FindEquationalProof — generate representations of proofs in equational logic
ProofObject — symbolic representation of proofs suitable for analysis and manipulation