In[]:=
ParallelMap[Labeled[TokenEventSubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory[#[[1]]]],1,"TokenLabeling"->False,GraphLayout->"SpringElectricalEmbedding",ImageSize120],Text[Style[#[[2]],Small]]]&,{{"AbelianGroupAxioms","commutative group theory"},{"BooleanAxioms","Boolean algebra"},{"CommutativeRingAxioms","commutative ring theory"},{"GroupAxioms"," group theory"},{"HigmanNeumannAxioms","group theory (minimal axiom)"},{"MonoidAxioms","monoid theory"},{"RingAxioms","ring theory"},{"SemigroupAxioms","semigroup theory"},{"SemiringAxioms","semiring theory"}},DistributedContexts"WolframMetamathematics`"]
{{"SemigroupAxioms","semigroup theory"},{"MonoidAxioms","monoid theory"},{"GroupAxioms"," group theory"},{"HigmanNeumannAxioms","group theory (minimal axiom)"},{"AbelianGroupAxioms","commutative group theory"},{"SemiringAxioms","semiring theory"},{"RingAxioms","ring theory"},{"CommutativeRingAxioms","commutative ring theory"},{"BooleanAxioms","Boolean algebra"},{"ShefferAxioms","Boolean algebra (Nand axioms)"},{"WolframCommutativeAxioms","Boolean algebra (minimal commutative axiom)"},{"WolframAxioms","Boolean algebra (minimal axiom)"}}
In[]:=
Length@{{"SemigroupAxioms","semigroup theory"},{"MonoidAxioms","monoid theory"},{"GroupAxioms"," group theory"},{"HigmanNeumannAxioms","group theory (minimal axiom)"},{"AbelianGroupAxioms","commutative group theory"},{"SemiringAxioms","semiring theory"},{"RingAxioms","ring theory"},{"CommutativeRingAxioms","commutative ring theory"},{"BooleanAxioms","Boolean algebra"},{"ShefferAxioms","Boolean algebra (Nand axioms)"}}
Out[]=
10
AxiomaticTheory["MeredithAxioms","EquivalentTheories"]
{{"Boolean algebra","ShefferAxioms"},​​{"Boolean algebra","HillmanAxioms"},​​{"Boolean algebra","WolframCommutativeAxioms"},​​{"Boolean algebra","WolframAxioms"},​​{"Boolean algebra","WolframAlternateAxioms"},​​{"equivalential calculus","EquivalentialCalculusAxioms"},​​{"implicational calculus","ImplicationalCalculusAxioms"},​​{"junctional calculus","JunctionalCalculus"},​​{"semigroups","SemigroupAxioms"},​​{"groups","HigmanNeumannAxioms"},​​{"Abelian groups","AbelianTarskiAxioms"},​​{"central groupoids","CentralGroupoidAxioms"}}
In[]:=
PlotAxX[{axs_,ths_}->mat_]:=MatrixPlot[mat,Mesh->True,FrameTicks->{{MapIndexed[{First[#2],#1,0}&,axs],None},{None,MapIndexed[{First[#2],Rotate[#1,Pi/2],0}&,ths]}}]
In[]:=
allst=SortBy[Union[First[Sort[{#,#/.{a->b,b->a}}]]&/@DeleteCases[Union[Sort/@canonicalizePatterns/@(TwoWayRule@@@Tuples[(Flatten[Groupings[#,SmallCircle->2]&/@Table[Tuples[{a,b},n],{n,3}]]/.{a->a_,b->b_}),2])]/.{p_Pattern:>First[p],TwoWayRule->Equal},Except[_Equal]]],StringLength[ToString[#]]&];
In[]:=
With[{axx={"ShefferAxioms","WolframCommutativeAxioms","WolframAxioms","WolframAlternateAxioms"}},{axx,Take[allst,70]}->Partition[ParallelMap[If[Head[#]===Failure,None,#["ProofLength"]]&[FindEquationalProof[ForAll[{a,b},#[[2]]],#[[1]],TimeConstraint10]]&,Tuples[{(AxiomaticTheory[#]/.CenterDot->SmallCircle)&/@axx,Take[allst,70]}]],70]]
Out[]=
{{ShefferAxioms,WolframCommutativeAxioms,WolframAxioms,WolframAlternateAxioms},{ab,aa∘a,aa∘b,ab∘a,ab∘b,a∘aa∘b,a∘ab∘a,a∘ab∘b,a∘bb∘a,a∘bb∘b,aa∘(a∘a),aa∘(a∘b),aa∘(b∘a),aa∘(b∘b),ab∘(a∘a),ab∘(a∘b),ab∘(b∘a),ab∘(b∘b),a(a∘a)∘a,a(a∘a)∘b,a(a∘b)∘a,a(a∘b)∘b,a(b∘a)∘a,a(b∘a)∘b,a(b∘b)∘a,a(b∘b)∘b,a∘aa∘(a∘a),a∘aa∘(a∘b),a∘aa∘(b∘a),a∘aa∘(b∘b),a∘ab∘(a∘a),a∘ab∘(a∘b),a∘ab∘(b∘a),a∘ab∘(b∘b),a∘a(a∘a)∘a,a∘a(a∘a)∘b,a∘a(a∘b)∘a,a∘a(a∘b)∘b,a∘a(b∘a)∘a,a∘a(b∘a)∘b,a∘a(b∘b)∘a,a∘a(b∘b)∘b,a∘ba∘(a∘a),a∘ba∘(a∘b),a∘ba∘(b∘a),a∘ba∘(b∘b),a∘bb∘(a∘a),a∘bb∘(a∘b),a∘bb∘(b∘a),a∘bb∘(b∘b),a∘b(a∘a)∘a,a∘b(a∘a)∘b,a∘b(a∘b)∘a,a∘b(a∘b)∘b,a∘b(b∘a)∘a,a∘b(b∘a)∘b,a∘b(b∘b)∘a,a∘b(b∘b)∘b,a∘(a∘a)b∘a,a∘(a∘a)b∘b,a∘(a∘b)b∘a,a∘(a∘b)b∘b,a∘(b∘a)b∘a,a∘(b∘a)b∘b,a∘(b∘b)b∘a,a∘(b∘b)b∘b,a∘(a∘a)a∘(a∘b),a∘(a∘a)a∘(b∘a),a∘(a∘a)a∘(b∘b),a∘(a∘a)b∘(a∘a)}}{{None,None,None,None,None,None,None,None,10,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None},{None,None,None,None,None,None,None,None,3,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None},{None,None,None,None,None,None,None,None,102,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None},{None,None,None,None,None,None,None,None,78,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None,None}}
In[]:=
PlotAxX[%]
Out[]=
In[]:=
Clear[ATECThms23]
In[]:=
ATECThms23[thmct_,t_]:=Module[{uu,axin=(AxiomaticTheoryTWP[AxiomaticTheory[#]/.CenterDot->SmallCircle])&/@{"ShefferAxioms","WolframCommutativeAxioms","WolframAxioms","WolframAlternateAxioms"}},With[{axlist=SortBy[Union[First[Sort[{#,#/.{a->b,b->a}}]]&/@DeleteCases[Union[Sort/@canonicalizePatterns/@(TwoWayRule@@@Tuples[(Flatten[Groupings[#,SmallCircle->2]&/@Table[Tuples[{a,b},n],{n,3}]]/.{a->a_,b->b_}),2])]/.{p_Pattern:>First[p],TwoWayRule->Equal},Except[_Equal]]],StringLength[ToString[#]]&]},uu=Map[(VertexList[AccumulativeTokenEventGraph[#,t],_TwoWayRule]/.{p_Pattern:>First[p],TwoWayRule->Equal})&,axin(*,DistributedContexts"Wolfram`Metamathematics`"*)];{axin,Take[axlist,thmct]}->With[{thmsG=Take[axlist,thmct]},Normal[SparseArray[Thread[#->1],Length[thmsG]]]&/@Map[First@FirstPosition[thmsG,#]&,(Intersection[#,thmsG]&/@uu),{2}]]]]
In[]:=
ATECThms23[70,1]
Out[]=
{{{(a_∘a_)∘(a_∘a_)a_,a_∘(b_∘(b_∘b_))a_∘a_,(a_∘(b_∘c_))∘(a_∘(b_∘c_))((b_∘b_)∘a_)∘((c_∘c_)∘a_)},{a_∘b_b_∘a_,(a_∘b_)∘(a_∘(b_∘c_))a_},{((b_∘c_)∘a_)∘(b_∘((b_∘a_)∘b_))a_},{(a_∘((c_∘a_)∘a_))∘(c_∘(b_∘a_))c_}},{ab,aa∘a,aa∘b,ab∘a,ab∘b,a∘aa∘b,a∘ab∘a,a∘ab∘b,a∘bb∘a,a∘bb∘b,aa∘(a∘a),aa∘(a∘b),aa∘(b∘a),aa∘(b∘b),ab∘(a∘a),ab∘(a∘b),ab∘(b∘a),ab∘(b∘b),a(a∘a)∘a,a(a∘a)∘b,a(a∘b)∘a,a(a∘b)∘b,a(b∘a)∘a,a(b∘a)∘b,a(b∘b)∘a,a(b∘b)∘b,a∘aa∘(a∘a),a∘aa∘(a∘b),a∘aa∘(b∘a),a∘aa∘(b∘b),a∘ab∘(a∘a),a∘ab∘(a∘b),a∘ab∘(b∘a),a∘ab∘(b∘b),a∘a(a∘a)∘a,a∘a(a∘a)∘b,a∘a(a∘b)∘a,a∘a(a∘b)∘b,a∘a(b∘a)∘a,a∘a(b∘a)∘b,a∘a(b∘b)∘a,a∘a(b∘b)∘b,a∘ba∘(a∘a),a∘ba∘(a∘b),a∘ba∘(b∘a),a∘ba∘(b∘b),a∘bb∘(a∘a),a∘bb∘(a∘b),a∘bb∘(b∘a),a∘bb∘(b∘b),a∘b(a∘a)∘a,a∘b(a∘a)∘b,a∘b(a∘b)∘a,a∘b(a∘b)∘b,a∘b(b∘a)∘a,a∘b(b∘a)∘b,a∘b(b∘b)∘a,a∘b(b∘b)∘b,a∘(a∘a)b∘a,a∘(a∘a)b∘b,a∘(a∘b)b∘a,a∘(a∘b)b∘b,a∘(b∘a)b∘a,a∘(b∘a)b∘b,a∘(b∘b)b∘a,a∘(b∘b)b∘b,a∘(a∘a)a∘(a∘b),a∘(a∘a)a∘(b∘a),a∘(a∘a)a∘(b∘b),a∘(a∘a)b∘(a∘a)}}{{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}}
In[]:=
ATECThms23[70,2]
Out[]=
$Aborted
In[]:=
AxiomaticTheory[#]/.First[Values[AxiomaticTheory[#,"Operators"]]]SmallCircle&/@Last/@faxlist
Out[]=

∀
a.
(a.∘a.)∘(a.∘a.)a.,
∀
{a.,b.}
a.∘(b.∘(b.∘b.))a.∘a.,
∀
{a.,b.,c.}
(a.∘(b.∘c.))∘(a.∘(b.∘c.))((b.∘b.)∘a.)∘((c.∘c.)∘a.),
∀
{a.,b.}
(a.∘a.)∘(a.∘b.)a.,
∀
{a.,b.}
a.∘(a.∘b.)a.∘(b.∘b.),
∀
{a.,b.,c.}
a.∘(a.∘(b.∘c.))b.∘(b.∘(a.∘c.)),
∀
{a.,b.}
a.∘b.b.∘a.,
∀
{a.,b.,c.}
(a.∘b.)∘(a.∘(b.∘c.))a.,
∀
{a.,b.,c.}
((b.∘c.)∘a.)∘(b.∘((b.∘a.)∘b.))a.,
∀
{a.,b.,c.}
(a.∘((c.∘a.)∘a.))∘(c.∘(b.∘a.))c.,
∀
{a.,b.,c.}
(a.∘b.)∘c.a.∘(b.∘c.),
∀
{a.,b.}
a.∘b.b.∘a.,
∀
{a.,b.}
(b.∘b.)∘a.a.,
∀
{a.,b.}
(a.∘b.)∘a.a.,
∀
{a.,b.,c.}
a.∘(b.∘c.)b.∘(a.∘c.),
∀
{a.,b.}
(a.∘b.)∘b.(b.∘a.)∘a.,
∀
{a.,b.,c.}
(a.∘b.)∘c.a.∘(b.∘c.),
∀
{a.,b.}
a.∘b.b.∘a.,
∀
{a.}
a.∘a.a.,
∀
{a.,b.,c.}
a.∘(b.∘c.)(a.∘b.)∘c.,
∀
{a.,b.,c.}
a.∘((((a.∘a.)∘b.)∘c.)∘(((a.∘a.)∘a.)∘c.))b.,
∀
{a.,b.,c.}
a.∘(b.∘(c.∘(a.∘b.)))c.,
∀
{a.,b.,c.}
(a.∘b.)∘(b.∘c.)a.
In[]:=
ModelTheorem
∀
a.
(a.∘a.)∘(a.∘a.)a.,
∀
{a.,b.}
a.∘(b.∘(b.∘b.))a.∘a.,
∀
{a.,b.,c.}
(a.∘(b.∘c.))∘(a.∘(b.∘c.))((b.∘b.)∘a.)∘((c.∘c.)∘a.),Take[allst,10],3
Out[]=
$Aborted
In[]:=
ModelTheoremAnd@@Last/@
∀
a.
(a.∘a.)∘(a.∘a.)a.,
∀
{a.,b.}
a.∘(b.∘(b.∘b.))a.∘a.,
∀
{a.,b.,c.}
(a.∘(b.∘c.))∘(a.∘(b.∘c.))((b.∘b.)∘a.)∘((c.∘c.)∘a.),Take[allst,10],3
Out[]=
$Aborted

Groups