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
AxiomaticTheory — curated axioms, theorems, etc. for standard theories
Propositional Logic & Boolean Algebra »
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
PossibleZeroQ ▪ PrimeQ ▪ IsomorphicGraphQ ▪ HamiltonianGraphQ
Specific Canonical Forms
Expand ▪ RootReduce ▪ TrigExpand ▪ TrigReduce ▪ PiecewiseExpand ▪ TensorReduce ▪ DifferenceRootReduce ▪ DifferentialRootReduce
Groupings — generate all expressions with binary etc. operators