In[]:=
polist=ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,aa⊗a,aa⊕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[]:=
pounion=GraphUnion@@(removeEvents/@polist);
In[]:=
GraphUnion[pounion,VertexLabels->(#->If[!FreeQ[#,a],#,None]&/@VertexList[pounion]),VertexSize->#->If[!FreeQ[#,a|a.],1.5,0.8]&/@VertexList[pounion],EdgeStyle->Opacity[.2],VertexStyle->{_List->Orange},GraphLayout"LayeredDigraphEmbedding",AspectRatio.7]
Out[]=
In[]:=
polist=ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,aa⊗a,aa⊕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[]:=
pounion=GraphUnion@@(VertexReplace[#,{"Event",__}:>{"Event",CreateUUID[]}]&/@polist);
In[]:=
GraphUnion[pounion,VertexLabels->(#->If[!FreeQ[#,a],#,None]&/@VertexList[pounion]),VertexSize->#->If[!FreeQ[#,a|a.],1.5,0.8]&/@VertexList[pounion],EdgeStyle->Opacity[.2],VertexStyle->{_List->Orange},GraphLayout"LayeredDigraphEmbedding",AspectRatio.7]
Out[]=
With Background Theorems
With Background Theorems
ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,aa⊗a,aa⊕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[]:=
CloudGet["https://wolfr.am/PO7vasDF"];
In[]:=
Take[data53,40]/.{Vee->CirclePlus,Wedge->CircleTimes,Square->OverBar}
Out[]=
aa⊗a,aa⊕a,a⊗aa⊕a,a⊗bb⊗a,a⊕bb⊕a,a,a⊗a,a⊕a,⊗aa⊗,⊕aa⊕,,,,a⊗⊗a,⊗bb⊗,a⊕⊕a,⊕bb⊕,,,⊗a⊗b,a⊗⊗b,⊗ab⊗,a⊗b⊗,⊕a⊕b,a⊕⊕b,⊕ab⊕,a⊕b⊕,⊗,⊗,⊗,⊕,⊕,⊕,⊗⊕,⊗,⊕,⊗,⊗⊗,⊕,⊕⊕
a
a
a
a
a
a
a
a
a⊗a
a
a⊕a
a⊗a
a⊕a
b
b
a
a
b
b
a
a
a⊗b
b⊗a
a⊕b
b⊕a
a
b
a
b
a
b
a
b
a
b
a
b
a
b
a
b
a
a
a
a⊗a
a
a
a⊕a
a
a
a
a
a
a⊗a
a
a
a⊕a
a
a
a
a
a
a
a⊕b
a
b
a⊗b
a
b
a⊕b
b
a
a
b
b
a
a⊗b
b
a
a
b
b
a
In[]:=
background=ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,data53/.{Vee->CirclePlus,Wedge->CircleTimes,Square->OverBar}];
In[]:=
GraphUnion@@(removeEvents/@background)
Out[]=
In[]:=
polist=ParallelMap[ProofObjectToTokenEventGraph[FindEquationalProof[#,"BooleanAxioms"],VertexShapeFunction->Automatic]&,aa⊗a,aa⊕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[]:=
pounion=GraphUnion@@(removeEvents/@polist);
In[]:=
Graph[GraphUnion@@Join[(removeEvents/@polist),(removeEvents/@background)],VertexStyle->Thread[aa⊗a,aa⊕a,a,⊗a⊗b,⊕a⊕b,⊗,⊕,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)->Red]]
a
a
b
a
b
a⊕b
a
b
a⊗b
a
b
The “eyes” are probably commutativity....