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[]:=
ResourceFunction["UnformalizeSymbols"][Last/@AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee}
Out[]=
a⋀bb⋀a,a⋀(b⋁c)a⋀b⋁a⋀c,a⋁b⋀a,a⋀(b⋁)a,a⋁bb⋁a,a⋁b⋀c(a⋁b)⋀(a⋁c)
b
b
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[]=
aa⋀a,aa⋁a,a⋀bb⋀a,a⋁bb⋁a,a,⋀a⋀b,⋁a⋁b,⋀,⋁,aa⋀(a⋁b),aa⋁a⋀b,(a⋀b)⋀ca⋀(b⋀c),(a⋁b)⋁ca⋁(b⋁c)
a
a
b
a
b
a⋁b
a
b
a⋀b
a
b
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_⋀b_,⋁a_⋁b_,⋀,⋁,a_a_⋀(a_⋁b_),a_a_⋁a_⋀b_,(a_⋀b_)⋀c_a_⋀(b_⋀c_),(a_⋁b_)⋁c_a_⋁(b_⋁c_)
a_
a_
b_
a_
b_
a_⋁b_
a_
b_
a_⋀b_
a_
b_
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
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_⋀a_,a_⋀(b_⋁)a_,a_⋁b_b_⋁a_,a_⋁b_⋀c_(a_⋁b_)⋀(a_⋁c_)
b_
b_
MultiwayRulesNestGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]],(a∘b)∘a,5,GraphLayout"SpringElectricalEmbedding",VertexShapeFunction->Automatic]
In[]:=
interesting=aa⋀a,aa⋁a,a⋀bb⋀a,a⋁bb⋁a,a,⋀a⋀b,⋁a⋁b,⋀,⋁,aa⋀(a⋁b),aa⋁a⋀b,(a⋀b)⋀ca⋀(b⋀c),(a⋁b)⋁ca⋁(b⋁c);
a
a
b
a
b
a⋁b
a
b
a⋀b
a
b
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[]=