(Possibly should not collapse True vertex)
In[]:=
VertexReplace[TokenEventSubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee},1,GraphLayout->"SpringElectricalEmbedding"],v_:>(symbolifyPatterns[v]/.TwoWayRule->Equal)]
Out[]=
In[]:=
vvvv=VertexList[%93,_Equal]
Out[]=
In[]:=
notablethms={aa⋀a,"idempotent law for and"},{aa⋁a,"idempotent law for or"},{a⋀bb⋀a,"commutativity for and"},{a⋁bb⋁a,"commutativity for or"},a,"law of double negation",⋀a⋀b,"law of noncontradiction",⋁a⋁b,"law of excluded middle",⋀,"de Morgan law",⋁,"de Morgan law",{aa⋀(a⋁b),"absorption law"},{aa⋁a⋀b,"absorption law"},{(a⋀b)⋀ca⋀(b⋀c),"associativity of and"},{(a⋁b)⋁ca⋁(b⋁c),"associativity of or"};
a
a
b
a
b
a⋁b
a
b
a⋀b
a
b
In[]:=
#->Position[vvvv,First[#]]&/@notablethms
Out[]=
{aa⋀a,idempotent law for and}{},{aa⋁a,idempotent law for or}{},{a⋀bb⋀a,commutativity for and}{{1}},{a⋁bb⋁a,commutativity for or}{{5}},a,law of double negation{},⋀a⋀b,law of noncontradiction{},⋁a⋁b,law of excluded middle{},⋀,de Morgan law{},⋁,de Morgan law{},{aa⋀(a⋁b),absorption law}{},{aa⋁a⋀b,absorption law}{},{(a⋀b)⋀ca⋀(b⋀c),associativity of and}{},{(a⋁b)⋁ca⋁(b⋁c),associativity of or}{}
a
a
b
a
b
a⋁b
a
b
a⋀b
a
b
In[]:=
VertexReplace[TokenEventBisubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee},1,GraphLayout->"SpringElectricalEmbedding"],v_:>(symbolifyPatterns[v]/.TwoWayRule->Equal)];
In[]:=
VertexCount[%]
Out[]=
280
In[]:=
vvvb=VertexList[%105,_Equal];
In[]:=
#->Position[vvvb,First[#]]&/@notablethms
Out[]=
{aa⋀a,idempotent law for and}{},{aa⋁a,idempotent law for or}{},{a⋀bb⋀a,commutativity for and}{{1}},{a⋁bb⋁a,commutativity for or}{{5}},a,law of double negation{},⋀a⋀b,law of noncontradiction{},⋁a⋁b,law of excluded middle{},⋀,de Morgan law{},⋁,de Morgan law{},{aa⋀(a⋁b),absorption law}{},{aa⋁a⋀b,absorption law}{},{(a⋀b)⋀ca⋀(b⋀c),associativity of and}{},{(a⋁b)⋁ca⋁(b⋁c),associativity of or}{}
a
a
b
a
b
a⋁b
a
b
a⋀b
a
b
In[]:=
#->Position[Reverse/@vvvb,First[#]]&/@notablethms
Out[]=
{aa⋀a,idempotent law for and}{},{aa⋁a,idempotent law for or}{},{a⋀bb⋀a,commutativity for and}{},{a⋁bb⋁a,commutativity for or}{},a,law of double negation{},⋀a⋀b,law of noncontradiction{},⋁a⋁b,law of excluded middle{},⋀,de Morgan law{},⋁,de Morgan law{},{aa⋀(a⋁b),absorption law}{},{aa⋁a⋀b,absorption law}{},{(a⋀b)⋀ca⋀(b⋀c),associativity of and}{},{(a⋁b)⋁ca⋁(b⋁c),associativity of or}{}
a
a
b
a
b
a⋁b
a
b
a⋀b
a
b
In[]:=
vvvv=VertexList[TokenEventSubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]/.{CircleTimes->Wedge,CirclePlus->Vee},1,GraphLayout->"SpringElectricalEmbedding"],_TwoWayRule];
In[]:=
Take[vvvv,6]
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_
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvv,True]]/@notablethms
Out[]=
{aa⋀a,idempotent law for and}{},{aa⋁a,idempotent law for or}{},{a⋀bb⋀a,commutativity for and}{{1}},{a⋁bb⋁a,commutativity for or}{{5}},a,law of double negation{},⋀a⋀b,law of noncontradiction{},⋁a⋁b,law of excluded middle{},⋀,de Morgan law{},⋁,de Morgan law{},{aa⋀(a⋁b),absorption law}{},{aa⋁a⋀b,absorption law}{},{(a⋀b)⋀ca⋀(b⋀c),associativity of and}{},{(a⋁b)⋁ca⋁(b⋁c),associativity of or}{}
a
a
b
a
b
a⋁b
a
b
a⋀b
a
b
In[]:=
LeafCount/@Normal[Values[FindEquationalProof[⋁a⋁b/.(Reverse/@{CircleTimes->Wedge,CirclePlus->Vee}),"BooleanAxioms","ProofDataset"][All,"Statement"]]]
a
b
Out[]=
{8,7,7,9,8,9,9,9,1}
In[]:=
Labeled[Histogram[LeafCount/@Normal[Values[FindEquationalProof[First[#]/.(Reverse/@{CircleTimes->Wedge,CirclePlus->Vee}),"BooleanAxioms","ProofDataset"][All,"Statement"]]]],#]&/@notablethms
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
{aa⋀a,idempotent law for and} |
{aa⋁a,idempotent law for or} |
{a⋀bb⋀a,commutativity for and} |
{a⋁bb⋁a,commutativity for or} |
a a |
a b |
a b |
a⋁b a b |
a⋀b a b |
{aa⋀(a⋁b),absorption law} |
{aa⋁a⋀b,absorption law} |
{(a⋀b)⋀ca⋀(b⋀c),associativity of and} |
{(a⋁b)⋁ca⋁(b⋁c),associativity of or} |
Restrict size of intermediate theorems
Restrict size of intermediate theorems
Minimal BA Axiom
Minimal BA Axiom