Theorem Proving

The Wolfram Language performs theorem proving in many forms and many domains. Sometimes the theorem proving is an implicit part of other operations; sometimes it is explicit.


Equal test equality of expressions

And ()  ▪  Or ()  ▪  Not (¬)  ▪  Implies ()

ForAll ()  ▪  Exists ()  ▪  Element ()  ▪  NotElement ()

Resolve eliminate quantifiers

Reduce reduce logical combinations of equations, inequalities, etc.

FindInstance find an explicit instance satisfying equations, inequalities, etc.

FullSimplify simplify using built-in rules and specified axioms

Propositional Logic & Boolean Algebra »

SatisfiableQ  ▪  TautologyQ

BooleanConvert convert Boolean expressions to canonical forms

Polynomial Algebra

PolynomialGCD canonicalize systems of univariate polynomial equations

GroebnerBasis canonicalize systems of multivariate polynomial equations

CylindricalDecomposition canonicalize combinations of equations and inequalities

Specific Tests

PossibleZeroQ  ▪  PrimeQ  ▪  IsomorphicGraphQ  ▪  HamiltonianGraphQ

Specific Canonical Forms

Expand  ▪  RootReduce  ▪  TrigExpand  ▪  TrigReduce  ▪  PiecewiseExpand  ▪  TensorReduce  ▪  DifferenceRootReduce  ▪  DifferentialRootReduce

Expression Enumeration

Groupings generate all expressions with binary etc. operators