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.

Predicates

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