WOLFRAM NOTEBOOK

In[]:=
FindEquationalProof[p·q==q·p,"WolframAxioms"]
Out[]=
ProofObject
Logic: EquationalLogic
Steps: 102
Theorem: p·qq·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]},AspectRatio2,ImageSizeScaled[.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]},AspectRatio2,ImageSizeScaled[.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

Wolfram Cloud

You are using a browser not supported by the Wolfram Cloud

Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.


I understand and wish to continue anyway »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.