New in Wolfram Mathematica 6: Equational Theorem Proving ◄ previous | next ►
Prove a Recently Discovered Theorem
Mathematica 6 can establish commutativity from Wolfram's recent minimal axiom for Boolean algebra.
In[1]:=

Click for copyable input
FullSimplify[a\[SmallCircle]b == b\[SmallCircle]a, \!\(

\*SubscriptBox[\(\[ForAll]\), \({p, q, 

    r}\)]\((\((p\[SmallCircle]q)\)\[SmallCircle]r)\)\[SmallCircle]\((\

p\[SmallCircle]\((\((p\[SmallCircle]r)\)\[SmallCircle]p)\))\) == r\)]
Out[1]=