# Wolfram Language & System 10.4 (2016)|Legacy Documentation

This is documentation for an earlier version of the Wolfram Language.
WOLFRAM LANGUAGE GUIDE

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

## ReferenceReference

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

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