Wolfram 语言实现各种格式和域的定理证明. 有时候，定律证明过程隐藏在其他操作中；有时候，很明显地提供给用户. 对于使用等式逻辑指定的公理系统，Wolfram 语言包括用于生成完整符号证明对象的最先进功能功能对于使用等式逻辑指定的公理系统，Wolfram 语言包括用于生成完整符号证明对象的最先进功能功能.

谓词

Equal — 测试表达式的相等性

And (∧)  ▪  Or (∨)  ▪  Not (¬)  ▪  Implies ()

ForAll (∀)  ▪  Exists (∃)  ▪  Element (∈)  ▪  NotElement (∉)

Resolve — 消除量词

Reduce — 简化方程、不等式等的逻辑组合

FindInstance — 求满足方程、不等式等的显式范例

FullSimplify — 使用内置规则和指定公理进行简化

根据等式定理产生证明

FindEquationalProof — 根据任意等式原理系统产生证明

ProofObject — 证明的符号表示适于分析和操作

公理理论

AxiomaticTheory — 用于标准理论的精选公理、理论等

命题逻辑和布尔代数 »

SatisfiableQ  ▪  TautologyQ

BooleanConvert — 把布尔表达式转化为标准型

多项式代数 »

PolynomialGCD — 规范化一元多项式方程组

GroebnerBasis — 规范化多元多项式方程组

CylindricalDecomposition — 规范化方程和不等式的组合

特定的测试

PossibleZeroQ  ▪  PrimeQ  ▪  IsomorphicGraphQ  ▪  HamiltonianGraphQ

特定的标准型

Expand  ▪  RootReduce  ▪  TrigExpand  ▪  TrigReduce  ▪  PiecewiseExpand  ▪  TensorReduce  ▪  DifferenceRootReduce  ▪  DifferentialRootReduce

表达式枚举

Groupings — 用二进制等算符产生所有表达式