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
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