Prove an Abstract Algebraic Theorem
Mathematica 6 takes a theorem in abstract algebra, entered in standard notation, and immediately proves it.
In[1]:=  |  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]=  |  |