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 »
WOLFRAM NOTEBOOK
In[]:=
Groupings[{a,b,c,d},CenterDot->2]
Out[]=
{((a·b)·c)·d,a·((b·c)·d),(a·(b·c))·d,a·(b·(c·d)),(a·b)·(c·d)}
In[]:=
FindEquationalProofFirst==Last,ForAll[{a.,b.,c.},a.·(b.·c.)(a.·b.)·c.]
Out[]=
ProofObject
In[]:=
Out[]=
Pick any Axiom and Ask for Easy-to-Prove Results...
Pick any Axiom and Ask for Easy-to-Prove Results...
In[]:=
Out[]=
In[]:=
VertexList[%]
Out[]=
{((a_·b_)·c_)·(a_·((a_·c_)·a_))c_,(((((a_·b_)·c_)·(a_·((a_·c_)·a_)))·d_)·e_)·(c_·((c_·e_)·c_))e_,((((a_·b_)·(c_·d_))·(a_·((a_·(c_·d_))·a_)))·e_)·(c_·((c_·e_)·c_))e_,(((a_·b_)·((c_·d_)·e_))·(a_·((a_·((c_·d_)·e_))·a_)))·(c_·((c_·e_)·c_))e_,((a_·(((b_·c_)·d_)·(b_·((b_·d_)·b_))))·e_)·(a_·((a_·e_)·a_))e_,((a_·b_)·(((c_·d_)·e_)·(c_·((c_·e_)·c_))))·(a_·((a_·(((c_·d_)·e_)·(c_·((c_·e_)·c_))))·a_))e_,((a_·b_)·(((c_·d_)·e_)·(c_·((c_·e_)·c_))))·(a_·((a_·e_)·a_))e_,((a_·b_)·c_)·((((d_·e_)·a_)·(d_·((d_·a_)·d_)))·((a_·c_)·a_))c_,((a_·b_)·c_)·(((d_·e_)·(a_·((a_·c_)·a_)))·(d_·((d_·(a_·((a_·c_)·a_)))·d_)))c_,((a_·b_)·c_)·(a_·(((((d_·e_)·a_)·(d_·((d_·a_)·d_)))·c_)·a_))c_,((a_·b_)·c_)·(a_·((((d_·e_)·(a_·c_))·(d_·((d_·(a_·c_))·d_)))·a_))c_,((a_·b_)·c_)·(a_·(((d_·e_)·((a_·c_)·a_))·(d_·((d_·((a_·c_)·a_))·d_))))c_,((a_·b_)·c_)·(a_·((a_·(((d_·e_)·c_)·(d_·((d_·c_)·d_))))·a_))c_,((a_·b_)·c_)·(a_·((a_·c_)·(((d_·e_)·a_)·(d_·((d_·a_)·d_)))))c_,((a_·b_)·c_)·(a_·((a_·c_)·a_))((d_·e_)·c_)·(d_·((d_·c_)·d_)),a_a_,{Event,1,1}}
In[]:=
Cases[%85]/.TwoWayRule->Equal,_Equal
Out[]=
{((a·b)·c)·(a·((a·c)·a))c,(((((a·b)·c)·(a·((a·c)·a)))·d)·e)·(c·((c·e)·c))e,((((a·b)·(c·d))·(a·((a·(c·d))·a)))·e)·(c·((c·e)·c))e,(((a·b)·((c·d)·e))·(a·((a·((c·d)·e))·a)))·(c·((c·e)·c))e,((a·(((b·c)·d)·(b·((b·d)·b))))·e)·(a·((a·e)·a))e,((a·b)·(((c·d)·e)·(c·((c·e)·c))))·(a·((a·(((c·d)·e)·(c·((c·e)·c))))·a))e,((a·b)·(((c·d)·e)·(c·((c·e)·c))))·(a·((a·e)·a))e,((a·b)·c)·((((d·e)·a)·(d·((d·a)·d)))·((a·c)·a))c,((a·b)·c)·(((d·e)·(a·((a·c)·a)))·(d·((d·(a·((a·c)·a)))·d)))c,((a·b)·c)·(a·(((((d·e)·a)·(d·((d·a)·d)))·c)·a))c,((a·b)·c)·(a·((((d·e)·(a·c))·(d·((d·(a·c))·d)))·a))c,((a·b)·c)·(a·(((d·e)·((a·c)·a))·(d·((d·((a·c)·a))·d))))c,((a·b)·c)·(a·((a·(((d·e)·c)·(d·((d·c)·d))))·a))c,((a·b)·c)·(a·((a·c)·(((d·e)·a)·(d·((d·a)·d)))))c,((a·b)·c)·(a·((a·c)·a))((d·e)·c)·(d·((d·c)·d))}
In[]:=
ParallelMapFindEquationalProof[#,"WolframAxioms"]["ProofLength"]&,
Out[]=
{3,4,4,4,3,5,4,4,4,4,4,4,4,4,4}
In[]:=
TakeLargestByParallelMapFindEquationalProof[#,"WolframAxioms"]&,,#["ProofLength"]&,3
Out[]=
ProofObject,ProofObject,ProofObject
In[]:=
ProofObject["ProofDataset"]
Out[]=
Do we sample all the small lemmas in a typical proof?
Do we sample all the small lemmas in a typical proof?
What is the analog of making random patterns in a CA?
In[]:=
lemma2=CasesVertexList["WolframAxioms"],2,"Identity"True,"TokenLabeling"->False/.TwoWayRule->Equal,_Equal;
In[]:=
Length[lemma2]
Out[]=
5392
In[]:=
ParallelMap[FindEquationalProof[#,"WolframAxioms",TimeConstraint->10]["ProofLength"]&,lemma2];
In[]:=
Counts[%]
Out[]=
3184,4307,5569,63071,7784,8306,10102,944,116,1318,171
In[]:=
Histogram
,{1},{"Log","Count"}
Out[]=
In[]:=
ListPlotTransposeLeafCount/@lemma2,
,PlotRange->All,AxesLabel->{"leaf count","proof length"}
Out[]=
This never tries critical pair lemmas...
But substitution was how the entailment cone was made ... so it’s wasting time here....
But substitution was how the entailment cone was made ... so it’s wasting time here....
Pure Substitution Lemmas
Pure Substitution Lemmas
Pure Associativity
Pure Associativity
Lemmas in the Actual Proof
Lemmas in the Actual Proof
So this is in fact going through a lot of lemmas, even though it happens to make direct use of the axiom.....
C40:
This is essentially an evaluation ordering of reducing by the axioms.....
[AKA a path in the entailment cone]
[AKA a path in the entailment cone]