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
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
FindEquationalProof — generate proofs from arbitrary equational axiom systems
ProofObject — symbolic representation of proofs suitable for analysis and manipulation
BooleanConvert — convert Boolean expressions to canonical forms
PolynomialGCD — canonicalize systems of univariate polynomial equations
GroebnerBasis — canonicalize systems of multivariate polynomial equations
CylindricalDecomposition — canonicalize combinations of equations and inequalities
Groupings — generate all expressions with binary etc. operators