WOLFRAM NOTEBOOK

(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={aaa,"idempotent law for and"},{aaa,"idempotent law for or"},{abba,"commutativity for and"},{abba,"commutativity for or"},a
a
,"law of double negation",
a
a
b
b,"law of noncontradiction",
a
a
b
b,"law of excluded middle",
ab
a
b
,"de Morgan law",
ab
a
b
,"de Morgan law",{aa(ab),"absorption law"},{aaab,"absorption law"},{(ab)ca(bc),"associativity of and"},{(ab)ca(bc),"associativity of or"};
In[]:=
#->Position[vvvv,First[#]]&/@notablethms
Out[]=
{aaa,idempotent law for and}{},{aaa,idempotent law for or}{},{abba,commutativity for and}{{1}},{abba,commutativity for or}{{5}},a
a
,law of double negation{},
a
a
b
b,law of noncontradiction{},
a
a
b
b,law of excluded middle{},
ab
a
b
,de Morgan law{},
ab
a
b
,de Morgan law{},{aa(ab),absorption law}{},{aaab,absorption law}{},{(ab)ca(bc),associativity of and}{},{(ab)ca(bc),associativity of or}{}
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[]=
{aaa,idempotent law for and}{},{aaa,idempotent law for or}{},{abba,commutativity for and}{{1}},{abba,commutativity for or}{{5}},a
a
,law of double negation{},
a
a
b
b,law of noncontradiction{},
a
a
b
b,law of excluded middle{},
ab
a
b
,de Morgan law{},
ab
a
b
,de Morgan law{},{aa(ab),absorption law}{},{aaab,absorption law}{},{(ab)ca(bc),associativity of and}{},{(ab)ca(bc),associativity of or}{}
In[]:=
#->Position[Reverse/@vvvb,First[#]]&/@notablethms
Out[]=
{aaa,idempotent law for and}{},{aaa,idempotent law for or}{},{abba,commutativity for and}{},{abba,commutativity for or}{},a
a
,law of double negation{},
a
a
b
b,law of noncontradiction{},
a
a
b
b,law of excluded middle{},
ab
a
b
,de Morgan law{},
ab
a
b
,de Morgan law{},{aa(ab),absorption law}{},{aaab,absorption law}{},{(ab)ca(bc),associativity of and}{},{(ab)ca(bc),associativity of or}{}
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_
b_
a_,a_(b_
b_
)a_,a_b_b_a_,a_b_c_(a_b_)(a_c_)
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvv,True]]/@notablethms
Out[]=
{aaa,idempotent law for and}{},{aaa,idempotent law for or}{},{abba,commutativity for and}{{1}},{abba,commutativity for or}{{5}},a
a
,law of double negation{},
a
a
b
b,law of noncontradiction{},
a
a
b
b,law of excluded middle{},
ab
a
b
,de Morgan law{},
ab
a
b
,de Morgan law{},{aa(ab),absorption law}{},{aaab,absorption law}{},{(ab)ca(bc),associativity of and}{},{(ab)ca(bc),associativity of or}{}
In[]:=
LeafCount/@Normal[Values[FindEquationalProof[
a
a
b
b/.(Reverse/@{CircleTimes->Wedge,CirclePlus->Vee}),"BooleanAxioms","ProofDataset"][All,"Statement"]]]
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[]=
{aaa,idempotent law for and}
,
{aaa,idempotent law for or}
,
{abba,commutativity for and}
,
{abba,commutativity for or}
,
a
a
,law of double negation
,
a
a
b
b,law of noncontradiction
,
a
a
b
b,law of excluded middle
,
ab
a
b
,de Morgan law
,
ab
a
b
,de Morgan law
,
{aa(ab),absorption law}
,
{aaab,absorption law}
,
{(ab)ca(bc),associativity of and}
,
{(ab)ca(bc),associativity of or}

Restrict size of intermediate theorems

Minimal BA Axiom

Wolfram Cloud

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 »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.