In[]:=

ParallelMap[Labeled[TokenEventSubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory[#[[1]]]],1,"TokenLabeling"->False,GraphLayout->"SpringElectricalEmbedding",ImageSize120],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]],TimeConstraint10]]&,Tuples[{(AxiomaticTheory[#]/.CenterDot->SmallCircle)&/@axx,Take[allst,70]}]],70]]

Out[]=

{{ShefferAxioms,WolframCommutativeAxioms,WolframAxioms,WolframAlternateAxioms},{ab,aa∘a,aa∘b,ab∘a,ab∘b,a∘aa∘b,a∘ab∘a,a∘ab∘b,a∘bb∘a,a∘bb∘b,aa∘(a∘a),aa∘(a∘b),aa∘(b∘a),aa∘(b∘b),ab∘(a∘a),ab∘(a∘b),ab∘(b∘a),ab∘(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∘aa∘(a∘a),a∘aa∘(a∘b),a∘aa∘(b∘a),a∘aa∘(b∘b),a∘ab∘(a∘a),a∘ab∘(a∘b),a∘ab∘(b∘a),a∘ab∘(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∘ba∘(a∘a),a∘ba∘(a∘b),a∘ba∘(b∘a),a∘ba∘(b∘b),a∘bb∘(a∘a),a∘bb∘(a∘b),a∘bb∘(b∘a),a∘bb∘(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_}},{ab,aa∘a,aa∘b,ab∘a,ab∘b,a∘aa∘b,a∘ab∘a,a∘ab∘b,a∘bb∘a,a∘bb∘b,aa∘(a∘a),aa∘(a∘b),aa∘(b∘a),aa∘(b∘b),ab∘(a∘a),ab∘(a∘b),ab∘(b∘a),ab∘(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∘aa∘(a∘a),a∘aa∘(a∘b),a∘aa∘(b∘a),a∘aa∘(b∘b),a∘ab∘(a∘a),a∘ab∘(a∘b),a∘ab∘(b∘a),a∘ab∘(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∘ba∘(a∘a),a∘ba∘(a∘b),a∘ba∘(b∘a),a∘ba∘(b∘b),a∘bb∘(a∘a),a∘bb∘(a∘b),a∘bb∘(b∘a),a∘bb∘(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.∘(b.∘(b.∘b.))a.∘a.,(a.∘(b.∘c.))∘(a.∘(b.∘c.))((b.∘b.)∘a.)∘((c.∘c.)∘a.),(a.∘a.)∘(a.∘b.)a.,a.∘(a.∘b.)a.∘(b.∘b.),a.∘(a.∘(b.∘c.))b.∘(b.∘(a.∘c.)),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.)∘c.a.∘(b.∘c.),a.∘b.b.∘a.,(b.∘b.)∘a.a.,(a.∘b.)∘a.a.,a.∘(b.∘c.)b.∘(a.∘c.),(a.∘b.)∘b.(b.∘a.)∘a.,(a.∘b.)∘c.a.∘(b.∘c.),a.∘b.b.∘a.,a.∘a.a.,a.∘(b.∘c.)(a.∘b.)∘c.,a.∘((((a.∘a.)∘b.)∘c.)∘(((a.∘a.)∘a.)∘c.))b.,a.∘(b.∘(c.∘(a.∘b.)))c.,(a.∘b.)∘(b.∘c.)a.

∀

a.

∀

{a.,b.}

∀

{a.,b.,c.}

∀

{a.,b.}

∀

{a.,b.}

∀

{a.,b.,c.}

∀

{a.,b.}

∀

{a.,b.,c.}

∀

{a.,b.,c.}

∀

{a.,b.,c.}

∀

{a.,b.,c.}

∀

{a.,b.}

∀

{a.,b.}

∀

{a.,b.}

∀

{a.,b.,c.}

∀

{a.,b.}

∀

{a.,b.,c.}

∀

{a.,b.}

∀

{a.}

∀

{a.,b.,c.}

∀

{a.,b.,c.}

∀

{a.,b.,c.}

∀

{a.,b.,c.}

In[]:=

ModelTheorem(a.∘a.)∘(a.∘a.)a.,a.∘(b.∘(b.∘b.))a.∘a.,(a.∘(b.∘c.))∘(a.∘(b.∘c.))((b.∘b.)∘a.)∘((c.∘c.)∘a.),Take[allst,10],3

∀

a.

∀

{a.,b.}

∀

{a.,b.,c.}

Out[]=

$Aborted

In[]:=

ModelTheoremAnd@@Last/@(a.∘a.)∘(a.∘a.)a.,a.∘(b.∘(b.∘b.))a.∘a.,(a.∘(b.∘c.))∘(a.∘(b.∘c.))((b.∘b.)∘a.)∘((c.∘c.)∘a.),Take[allst,10],3

∀

a.

∀

{a.,b.}

∀

{a.,b.,c.}

Out[]=

$Aborted

## Groups

Groups