In[]:=
FindEquationalProof[p·q==q·p,"WolframAxioms"]
Out[]=
ProofObject
Logic: EquationalLogic
Steps: 102
Theorem: p·qq·p

[◼]
ReverseTokenEventProofGraph
[FindEquationalProof[a∘((a∘b)∘a)==(b∘b)∘(a∘b),{ForAll[{a,b,c},{(b∘a)∘(c∘((c∘a)∘c))==a}]},TimeConstraint->50]["TokenEventProofGraph",​​"TokenLabeling"->False,VertexSize->{{"Event",__}.5,r:HoldForm[_Equal]:>.25Sqrt@LeafCount[r]},AspectRatio2,ImageSizeScaled[.4]​​],​​(*FindEquationalProofsometimesreversesstatements*)​​HoldForm[a∘((a∘b)∘a)(b∘b)∘(a∘b)]​​]
In[]:=
FindEquationalProof[p·q==q·p,"WolframAxioms"]["TokenEventProofGraph",​​"TokenLabeling"->False,VertexSize->{{"Event",__}.5,r:HoldForm[_Equal]:>.25Sqrt@LeafCount[r]},AspectRatio2,ImageSizeScaled[.4]​​]
Out[]=
a.·a.  a.·((a.·a.)·a.) is roughly in the middle, and has lots of outgoing branches
Also work out BetweennessCentrality etc. for lemmas.....
In[]:=
VertexCount[%]
Out[]=
201
In[]:=
VertexOutDegree

Out[]=
{1,5,7,1,1,2,1,8,1,4,1,1,29,1,5,1,1,1,3,1,1,7,1,1,8,1,1,1,1,1,1,2,2,1,2,4,1,1,1,1,1,1,1,1,1,2,1,1,1,3,4,1,2,1,1,1,3,1,1,1,1,1,1,1,1,0,2,1,1,1,1,1,4,3,1,1,1,1,1,1,1,2,1,1,3,1,4,4,1,1,1,1,1,1,1,1,1,1,1,1,3,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1}
In[]:=
FindEquationalProof[p·q==q·p,"WolframAxioms"]["ProofGraph"]
Out[]=
In[]:=
VertexCount[%]
Out[]=
102
This is pure events without lemmas
In[]:=
VertexList


ATP Systems

Proof graphics

Red piece is like an inflated axiom ... that proves certain useful, derived theorems that can be used as more efficient axioms

Reverse Proving of Axiom from Lemmas