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={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
,"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",{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"};
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
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{},{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}{}
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
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{},{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}{}
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
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{},{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}{}
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[]=
{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
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{},{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}{}
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[]=
{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
,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
,
{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

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.