In[]:=
ResourceFunction["UnformalizeSymbols"][Last/@AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee}
Out[]=
a⋀bb⋀a,a⋀(b⋁c)a⋀b⋁a⋀c,a⋁b⋀
b
a,a⋀(b⋁
b
)a,a⋁bb⋁a,a⋁b⋀c(a⋁b)⋀(a⋁c)
In[]:=
AccumulativeTokenEventGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]],1,"TokenLabeling"->False,GraphLayout->"SpringElectricalEmbedding"]
Out[]=
In[]:=
VertexList[%,_TwoWayRule]
In[]:=
ResourceFunction["UnformalizeSymbols"][VertexList[%231,_TwoWayRule]/.p_Pattern:>First[p]]/.{CircleTimes->Wedge,CirclePlus->Vee,TwoWayRule->Equal}
Out[]=
In[]:=
interesting=First/@{{a==a⋀a,"idempotent law for and"},{a==a⋁a,"idempotent law for or"},{a⋀b==b⋀a,"commutativity for and"},{a⋁b==b⋁a,"commutativity for or"},{a==a,"law of double negation"},{a⋀a==b⋀b,"law of noncontradiction"},{a⋁a==b⋁b,"law of excluded middle"},{(a⋁b)==a⋀b,"de Morgan law"},{(a⋀b)==a⋁b,"de Morgan law"},{a==a⋀(a⋁b),"absorption law"},{a==a⋁a⋀b,"absorption law"},{(a⋀b)⋀c==a⋀(b⋀c),"associativity of and"},{(a⋁b)⋁c==a⋁(b⋁c),"associativity of or"}}/.Square->OverBar
Out[]=
aa⋀a,aa⋁a,a⋀bb⋀a,a⋁bb⋁a,a
a
,
a
⋀a
b
⋀b,
a
⋁a
b
⋁b,
a⋁b

a
⋀
b
,
a⋀b

a
⋁
b
,aa⋀(a⋁b),aa⋁a⋀b,(a⋀b)⋀ca⋀(b⋀c),(a⋁b)⋁ca⋁(b⋁c)
In[]:=
Position[%236,#]&/@%238
Out[]=
{{},{},{{1}},{{5}},{},{},{},{},{},{},{},{},{}}
In[]:=
interesting/.{a->a_,b->b_,c->c_}
Out[]=
a_a_⋀a_,a_a_⋁a_,a_⋀b_b_⋀a_,a_⋁b_b_⋁a_,a_
a_
,
a_
⋀a_
b_
⋀b_,
a_
⋁a_
b_
⋁b_,
a_⋁b_

a_
⋀
b_
,
a_⋀b_

a_
⋁
b_
,a_a_⋀(a_⋁b_),a_a_⋁a_⋀b_,(a_⋀b_)⋀c_a_⋀(b_⋀c_),(a_⋁b_)⋁c_a_⋁(b_⋁c_)
In[]:=
Position[%236,#]&/@%242
Out[]=
{{},{},{{1}},{{5}},{},{},{},{},{},{},{},{},{}}
In[]:=
Position[%236,#]&/@(Reverse/@%242)
Out[]=
{{},{},{{1}},{{5}},{},{},{},{},{},{},{},{},{}}
In[]:=
thms2=ResourceFunction["UnformalizeSymbols"][VertexList[#,_TwoWayRule]/.p_Pattern:>First[p]]/.{CircleTimes->Wedge,CirclePlus->Vee,TwoWayRule->Equal}&[AccumulativeTokenEventGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]],2,"TokenLabeling"->False,GraphLayout->"SpringElectricalEmbedding"]];
Out[]=
$Aborted
Position[thms2,#]&/@interesting
Position[thms2,#]&/@(interesting/.{a->a_,b->b_,c->c_})

In Draft-04: look at pure path case, rather than accumulative

MultiwayRulesNestGraph[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,5,​​GraphLayout"SpringElectricalEmbedding",​​VertexShapeFunction->Automatic]
In[]:=
AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee}
Out[]=
a_⋀b_b_⋀a_,a_⋀(b_⋁c_)a_⋀b_⋁a_⋀c_,a_⋁b_⋀
b_
a_,a_⋀(b_⋁
b_
)a_,a_⋁b_b_⋁a_,a_⋁b_⋀c_(a_⋁b_)⋀(a_⋁c_)
MultiwayRulesNestGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]],(a∘b)∘a,5,​​GraphLayout"SpringElectricalEmbedding",​​VertexShapeFunction->Automatic]
In[]:=
interesting=aa⋀a,aa⋁a,a⋀bb⋀a,a⋁bb⋁a,a
a
,
a
⋀a
b
⋀b,
a
⋁a
b
⋁b,
a⋁b

a
⋀
b
,
a⋀b

a
⋁
b
,aa⋀(a⋁b),aa⋁a⋀b,(a⋀b)⋀ca⋀(b⋀c),(a⋁b)⋁ca⋁(b⋁c);
In[]:=
MultiwayRulesNestGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]],a,1]
Out[]=
In[]:=
MultiwayRulesNestGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]],a_,2,AspectRatio->1/2]
Out[]=
WHY are the a_’s not merged?
In[]:=
MultiwayRulesNestGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee},a_,2,GraphLayout->"SpringElectricalEmbedding"]
Out[]=
In[]:=
MultiwayRulesNestGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee},a,2,GraphLayout->"SpringElectricalEmbedding"]
Out[]=