Enumerating Axiom Systems
Enumerating Axiom Systems
In[]:=
AllExprs[vars_,max_]:=Flatten[Groupings[#,SmallCircle->2]&/@Catenate[Table[Tuples[vars,n],{n,max}]]]
In[]:=
AllTheorems[vars_,max_]:=Union[Sort/@DeleteCases[Flatten[Outer[Equal,#,#]&[AllExprs[vars,max]]],True]]
In[]:=
AllExprs[{a,b},3]
Out[]=
{a,b,a∘a,a∘b,b∘a,b∘b,(a∘a)∘a,a∘(a∘a),(a∘a)∘b,a∘(a∘b),(a∘b)∘a,a∘(b∘a),(a∘b)∘b,a∘(b∘b),(b∘a)∘a,b∘(a∘a),(b∘a)∘b,b∘(a∘b),(b∘b)∘a,b∘(b∘a),(b∘b)∘b,b∘(b∘b)}
In[]:=
DeleteCases[#==a&/@AllExprs[{a,b},3],True]
Out[]=
{ba,a∘aa,a∘ba,b∘aa,b∘ba,(a∘a)∘aa,a∘(a∘a)a,(a∘a)∘ba,a∘(a∘b)a,(a∘b)∘aa,a∘(b∘a)a,(a∘b)∘ba,a∘(b∘b)a,(b∘a)∘aa,b∘(a∘a)a,(b∘a)∘ba,b∘(a∘b)a,(b∘b)∘aa,b∘(b∘a)a,(b∘b)∘ba,b∘(b∘b)a}
In[]:=
AllTheorems[{p,q},2]
Out[]=
{pq,pp∘p,pp∘q,pq∘p,pq∘q,qp∘p,qp∘q,qq∘p,qq∘q,p∘pp∘q,p∘pq∘p,p∘pq∘q,p∘qq∘p,p∘qq∘q,q∘pq∘q}
In[]:=
Outer[FindEquationalProof,AllTheorems[{p,q},2],DeleteCases[#==a&/@AllExprs[{a,b},3],True]]
Out[]=
$Aborted
In[]:=
Parallelize[Outer[FindEquationalProof,AllTheorems[{p,q},2],DeleteCases[ForAll[{a,b},#==a]&/@AllExprs[{a,b},3],True]]]
In[]:=
ArrayPlot[Map[If[Head[#]===Failure,0,1]&,%%,{2}],Mesh->True]
Out[]=
In[]:=
ProofObject["Properties"]
Out[]=
{Axioms,Logic,ProofDataset,ProofFunction,ProofGraph,ProofGraphWeighted,ProofLength,ProofNotebook,Theorem}
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,%574,{2}]
Out[]=
{{3,∞,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,3,3,3,3,∞,∞,∞,4,∞,∞,∞,∞,4,∞,∞,∞,∞,∞,4,4},{3,∞,3,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,∞,∞,3,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,∞,∞,3,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,∞,3,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,3,3,3,3,∞,∞,∞,4,∞,∞,∞,∞,4,∞,∞,∞,∞,∞,4,4},{3,∞,4,∞,3,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,∞,∞,4,3,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,∞,∞,∞,∞,4,4},{3,∞,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,∞,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4},{3,∞,∞,4,3,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,∞,∞,∞,∞,4,4},{3,∞,4,∞,3,∞,∞,4,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4,4}}
In[]:=
Parallelize[Outer[FindEquationalProof,AllTheorems[{p,q},2],DeleteCases[ForAll[{a,b},#]&/@AllTheorems[{a,b},2],True]]]
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,%,{2}]
Out[]=
{{3,∞,∞,∞,4,4,∞,∞,∞,∞,∞,∞,∞,∞,∞},{3,3,3,3,3,3,3,3,3,∞,∞,∞,∞,∞,∞},{3,∞,3,∞,4,4,∞,3,∞,∞,∞,∞,∞,∞,∞},{3,∞,∞,3,4,4,3,∞,∞,∞,∞,∞,∞,∞,∞},{3,∞,∞,∞,3,3,∞,∞,∞,∞,∞,∞,∞,∞,∞},{3,∞,∞,∞,3,3,∞,∞,∞,∞,∞,∞,∞,∞,∞},{3,∞,∞,3,4,4,3,∞,∞,∞,∞,∞,∞,∞,∞},{3,∞,3,∞,4,4,∞,3,∞,∞,∞,∞,∞,∞,∞},{3,3,3,3,3,3,3,3,3,∞,∞,∞,∞,∞,∞},{3,∞,4,∞,3,3,∞,4,∞,3,∞,∞,∞,∞,3},{3,∞,∞,4,3,3,4,∞,∞,∞,3,∞,∞,3,∞},{3,∞,∞,∞,4,4,∞,∞,∞,∞,∞,3,∞,∞,∞},{3,∞,∞,∞,4,4,∞,∞,∞,∞,∞,∞,3,∞,∞},{3,∞,∞,4,3,3,4,∞,∞,∞,3,∞,∞,3,∞},{3,∞,4,∞,3,3,∞,4,∞,3,∞,∞,∞,∞,3}}
In[]:=
Parallelize[Outer[FindEquationalProof,AllTheorems[{p,q,r},2],DeleteCases[ForAll[{a,b},#==a]&/@AllExprs[{a,b},3],True]]]
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,%,{2}]
Out[]=
In[]:=
Parallelize[Outer[FindEquationalProof,AllTheorems[{p,q},3],DeleteCases[ForAll[{a,b},#==a]&/@AllExprs[{a,b},3],True]]];
In[]:=
Map[If[Head[#]===Failure,Infinity,#["ProofLength"]]&,%,{2}]
Out[]=
In[]:=
Max[%/.Infinity->0]
Out[]=
6
In[]:=
Position[%585,6]
Out[]=
{{86,4},{86,15},{92,14},{103,4},{103,15},{104,9},{115,15},{130,15},{195,9},{199,14},{206,3},{206,8},{211,8},{228,3},{228,8},{229,8}}
In[]:=
Extract[Outer[Rule,AllTheorems[{p,q},3],DeleteCases[ForAll[{a,b},#==a]&/@AllExprs[{a,b},3],True]],%]
Out[]=
p∘(p∘p)q∘(q∘p)b∘aa,p∘(p∘p)q∘(q∘p)b∘(a∘a)a,p∘(p∘p)(q∘p)∘p(b∘a)∘aa,p∘(p∘q)q∘(q∘q)b∘aa,p∘(p∘q)q∘(q∘q)b∘(a∘a)a,p∘(p∘q)(p∘p)∘pa∘(a∘b)a,p∘(q∘p)q∘(p∘p)b∘(a∘a)a,p∘(q∘q)q∘(p∘q)b∘(a∘a)a,q∘(q∘p)(q∘q)∘qa∘(a∘b)a,q∘(q∘q)(p∘q)∘q(b∘a)∘aa,(p∘p)∘p(p∘q)∘qa∘ba,(p∘p)∘p(p∘q)∘q(a∘a)∘ba,(p∘p)∘q(p∘q)∘p(a∘a)∘ba,(q∘p)∘p(q∘q)∘qa∘ba,(q∘p)∘p(q∘q)∘q(a∘a)∘ba,(q∘p)∘q(q∘q)∘p(a∘a)∘ba
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
∀
{a,b}
In[]:=
FindEquationalProof[p∘(p∘p)q∘(q∘p),ForAll[{a,b},a==b∘a]]
Out[]=
ProofObject
In[]:=
ProofObjectToTokenEventGraph[%]
Out[]=
In[]:=
Map[If[Head[#]===Failure,Infinity,ProofCensus[#]]&,%584,{2}]
Out[]=
In[]:=
Position[%,{_,n_/;n>0}]
Out[]=
{{2,9},{2,14},{4,14},{4,16},{6,15},{11,16},{12,15},{14,9},{14,17},{16,8},{17,8},{19,17},{25,15},{26,16},{29,9},{29,14},{31,15},{33,14},{33,16},{36,17},{38,8},{39,8},{41,9},{41,17},{42,8},{43,8},{43,9},{43,10},{43,14},{44,8},{44,9},{45,8},{46,8},{47,15},{53,9},{53,11},{53,14},{53,15},{55,15},{57,14},{57,15},{59,15},{61,8},{62,8},{62,10},{63,8},{64,8},{64,9},{64,14},{66,15},{72,9},{72,14},{72,15},{74,11},{74,15},{76,15},{78,15},{79,8},{80,8},{80,15},{81,8},{85,16},{86,15},{88,9},{88,14},{88,16},{88,17},{92,14},{93,16},{93,17},{96,8},{97,8},{97,15},{101,15},{103,15},{104,9},{112,8},{115,15},{117,15},{118,16},{121,16},{121,17},{126,16},{126,17},{130,15},{134,9},{134,14},{141,8},{142,8},{142,9},{142,14},{143,8},{144,8},{144,10},{145,8},{146,15},{148,15},{150,11},{150,15},{152,9},{152,14},{152,15},{154,8},{155,8},{156,8},{156,9},{157,8},{157,9},{157,10},{157,14},{159,15},{161,14},{161,15},{163,15},{165,9},{165,11},{165,14},{165,15},{166,8},{167,8},{167,15},{168,8},{175,9},{175,14},{177,8},{178,8},{178,15},{179,16},{179,17},{184,16},{184,17},{187,8},{195,9},{198,16},{198,17},{199,14},{203,9},{203,14},{203,16},{203,17},{205,8},{205,15},{206,8},{207,15},{208,17},{209,15},{211,8},{212,8},{212,15},{214,15},{216,15},{217,8},{218,15},{220,15},{221,17},{223,15},{225,15},{226,8},{227,8},{227,15},{228,8},{229,8},{230,8},{230,15}}
Trying to find from enumeration
Trying to find from enumeration
BUG: should be ForAll[{a,b,c}, ....]