New in Wolfram Mathematica 6: Equational Theorem Proving ◄ previous | next ►
Prove an Abstract Algebraic Theorem
Mathematica 6 takes a theorem in abstract algebra, entered in standard notation, and immediately proves it.
In[1]:=

Click for copyable input
FullSimplify[\!\(

FullSimplify[ForAll[x, x \[CenterDot] e == x && a \[CenterDot] OverBar[a] == e], \
  ForAll[{x, y, z}, x \[CenterDot] (y \[CenterDot] z) == (x \[CenterDot] y) \
\[CenterDot] z && e \[CenterDot] x == x && OverBar[x] \[CenterDot] x == e]]
Out[1]=