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. For axiom systems specified using equational logic, the Wolfram Language includes state-of-the-art capabilities for generating full symbolic proof objects.


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

Generating Proofs from Equational Axioms

FindEquationalProof generate proofs from arbitrary equational axiom systems

ProofObject symbolic representation of proofs suitable for analysis and manipulation

Axiomatic Theories

AxiomaticTheory curated axioms, theorems, etc. for standard theories

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