[From Euclid Post]
[From Euclid Post]
Finding Theorems in the Wild
Finding Theorems in the Wild
AxiomaticTheory["BooleanAxioms"]
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.)
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.}
b.
∀
{a.,b.}
b.
∀
{a.,b.}
∀
{a.,b.,c.}
In[]:=
axioms=AxiomaticTheoryTWP[AxiomaticTheory["BooleanAxioms"]]
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[]:=
theorems=AxiomaticTheoryTWP[Values[AxiomaticTheory["BooleanAxioms","NotableTheorems"]]]
Out[]=
{a_a_⊗(a_⊕b_)},{a_a_⊕a_⊗b_},{(a_⊗b_)⊗c_a_⊗(b_⊗c_)},{a_⊗b_b_⊗a_},{a_⊗(b_⊕c_)a_⊗b_⊕a_⊗c_},{a_a_⊗a_},{a_⊗b_a_⊗(a_⊗b_)},⊗,⊕,{a_},{a_a_⊕b_⊗},{a_a_⊗(b_⊕)},{⊕a_⊕b_},a_⊕b_b_⊕a_,a_⊕(b_⊕c_)(a_⊕b_)⊕c_,⊕b_⊕⊕a_,a_⊕b_b_⊕a_,a_⊕(b_⊕c_)(a_⊕b_)⊕c_,⊕a_,{a_⊕b_a_⊕⊗b_},{⊗a_⊗b_},{(a_⊕b_)⊕c_a_⊕(b_⊕c_)},{a_⊕b_b_⊕a_},{a_⊕b_⊗c_(a_⊕b_)⊗(a_⊕c_)},{a_a_⊕a_},⊕b_⊕
a_⊕b_
a_
b_
a_⊗b_
a_
b_
a_
b_
b_
a_
b_
a_
a_
b_
a_⊕b_
a_⊕
b_
a_
a_
b_
a_
b_
a_
In[]:=
ctheorems=Flatten[canonicalizePatterns/@theorems]
Out[]=
a_a_⊗(a_⊕b_),a_a_⊕a_⊗b_,(a_⊗b_)⊗c_a_⊗(b_⊗c_),a_⊗b_b_⊗a_,a_⊗(b_⊕c_)a_⊗b_⊕a_⊗c_,a_a_⊗a_,a_⊗b_a_⊗(a_⊗b_),⊗,⊕,a_,a_a_⊕b_⊗,a_a_⊗(b_⊕),⊕a_⊕b_,a_⊕b_b_⊕a_,a_⊕(b_⊕c_)(a_⊕b_)⊕c_,⊕b_⊕⊕a_,a_⊕b_b_⊕a_,a_⊕(b_⊕c_)(a_⊕b_)⊕c_,⊕a_,a_⊕b_a_⊕⊗b_,⊗a_⊗b_,(a_⊕b_)⊕c_a_⊕(b_⊕c_),a_⊕b_b_⊕a_,a_⊕b_⊗c_(a_⊕b_)⊗(a_⊕c_),a_a_⊕a_,⊕b_⊕
a_⊕b_
a_
b_
a_⊗b_
a_
b_
a_
b_
b_
a_
b_
a_
a_
b_
a_⊕b_
a_⊕
b_
a_
a_
b_
a_
b_
a_
In[]:=
AccumulativeTokenEventGraph[axioms,1]
Out[]=
In[]:=
baax1=%501;
In[]:=
Length[VertexList[baax1,_TwoWayRule]]
Out[]=
365
In[]:=
Intersection[VertexList[baax1,_TwoWayRule],Join[ctheorems,Reverse/@ctheorems]]
Out[]=
a_⊗b_⊕a_⊗c_a_⊗(b_⊕c_),a_⊕b_⊗a_,a_⊕b_⊗c_(a_⊕b_)⊗(a_⊕c_),a_⊕b_b_⊕a_,a_⊗(b_⊕)a_,a_⊗(b_⊕c_)a_⊗b_⊕a_⊗c_,a_⊗b_b_⊗a_
b_
b_
In[]:=
Intersection[%,Join[axioms,Reverse/@axioms]]
Out[]=
a_⊗b_⊕a_⊗c_a_⊗(b_⊕c_),a_⊕b_⊗a_,a_⊕b_⊗c_(a_⊕b_)⊗(a_⊕c_),a_⊕b_b_⊕a_,a_⊗(b_⊕)a_,a_⊗(b_⊕c_)a_⊗b_⊕a_⊗c_,a_⊗b_b_⊗a_
b_
b_
In[]:=
baax2=AccumulativeTokenEventGraph[axioms,2];
Out[]=
$Aborted
In[]:=
AccumulativeTokenEventGraph[axioms,1,"S"]
Out[]=
In[]:=
VertexCount[%511,_TwoWayRule]
Out[]=
126
In[]:=
ProofCensus[FindEquationalProof[ForAll[{a,b,c},#]&[#/.p_Pattern:>First[p]/.TwoWayRule->Equal],ForAll[{a,b,c},#]&[axioms/.p_Pattern:>First[p]/.TwoWayRule->Equal]]]&/@ctheorems
Out[]=
{{8,15},{8,15},{15,27},{0,0},{0,0},{0,2},{4,10},{25,39},{25,39},{3,8},{0,0},{0,0},{2,2},{0,0},{15,27},{34,41},{0,0},{15,27},{32,39},{1,1},{2,2},{15,27},{0,0},{0,0},{0,2},{4,8}}
In[]:=
ProofCensus[FindEquationalProof[ForAll[{a,b,c},#]&[#/.p_Pattern:>First[p]/.TwoWayRule->Equal],ForAll[{a,b,c},#]&[axioms/.p_Pattern:>First[p]/.TwoWayRule->Equal]]]&/@"Absorption"a.a.⊗(a.⊕b.),"AbsorptionOrAnd"a.a.⊕a.⊗b.,"AndAssociativity"(a.⊗b.)⊗c.a.⊗(b.⊗c.),"AndCommutativity"a.⊗b.b.⊗a.,"AndDistributivity"a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,"AndIdempotence"a.a.⊗a.,"AndPreAssociativity"a.⊗b.a.⊗(a.⊗b.),"DeMorgan"⊗,⊕,"DoubleNegation"a.,"DroppingAlwaysFalse"a.a.⊕b.⊗,"DroppingAlwaysTrue"a.a.⊗b.⊕,"ExcludedMiddle"⊕a.⊕b.,"NegationRedundancy"a.⊕b.a.⊕⊗b.,"Noncontradiction"⊗a.⊗b.,"OrAssociativity"(a.⊕b.)⊕c.a.⊕(b.⊕c.),"OrCommutativity"a.⊕b.b.⊕a.,"OrDistributivity"a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.),"OrIdempotence"a.a.⊕a.,"Transposition"⊕b.⊕
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
a.
∀
{a.,b.}
∀
{a.,b.}
a.⊕b.
a.
b.
∀
{a.,b.}
a.⊗b.
a.
b.
∀
a.
a.
∀
{a.,b.}
b.
∀
{a.,b.}
b.
∀
{a.,b.}
a.
b.
∀
{a.,b.}
a.
∀
{a.,b.}
a.
b.
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
a.
∀
{a.,b.}
a.
b.
a.
Out[]=
Absorption{9,14},AbsorptionOrAnd{10,15},AndAssociativity{15,27},AndCommutativity{0,0},AndDistributivity{0,0},AndIdempotence{0,2},AndPreAssociativity{4,10},DeMorgan{26,40},DoubleNegation{3,8},DroppingAlwaysFalse{0,0},DroppingAlwaysTrue{0,0},ExcludedMiddle{2,2},NegationRedundancy{1,1},Noncontradiction{2,2},OrAssociativity{15,27},OrCommutativity{0,0},OrDistributivity{0,0},OrIdempotence{0,2},Transposition{4,8}
In[]:=
ListPlot[Reverse/@Normal@"Absorption"{9,14},"AbsorptionOrAnd"{10,15},"AndAssociativity"{15,27},"AndCommutativity"{0,0},"AndDistributivity"{0,0},"AndIdempotence"{0,2},"AndPreAssociativity"{4,10},"DeMorgan"{26,40},"DoubleNegation"{3,8},"DroppingAlwaysFalse"{0,0},"DroppingAlwaysTrue"{0,0},"ExcludedMiddle"{2,2},"NegationRedundancy"{1,1},"Noncontradiction"{2,2},"OrAssociativity"{15,27},"OrCommutativity"{0,0},"OrDistributivity"{0,0},"OrIdempotence"{0,2},"Transposition"{4,8},LabelingFunction->Callout]
Out[]=
In[]:=
ProofObjectToTokenEventGraph[FindEquationalProof[ForAll[{a,b,c},#]&[#/.p_Pattern:>First[p]/.TwoWayRule->Equal],ForAll[{a,b,c},#]&[axioms/.p_Pattern:>First[p]/.TwoWayRule->Equal]]]&/@"Absorption"a.a.⊗(a.⊕b.),"AbsorptionOrAnd"a.a.⊕a.⊗b.,"AndAssociativity"(a.⊗b.)⊗c.a.⊗(b.⊗c.),"AndCommutativity"a.⊗b.b.⊗a.,"AndDistributivity"a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,"AndIdempotence"a.a.⊗a.,"AndPreAssociativity"a.⊗b.a.⊗(a.⊗b.),"DeMorgan"⊗,⊕,"DoubleNegation"a.,"DroppingAlwaysFalse"a.a.⊕b.⊗,"DroppingAlwaysTrue"a.a.⊗b.⊕,"ExcludedMiddle"⊕a.⊕b.,"NegationRedundancy"a.⊕b.a.⊕⊗b.,"Noncontradiction"⊗a.⊗b.,"OrAssociativity"(a.⊕b.)⊕c.a.⊕(b.⊕c.),"OrCommutativity"a.⊕b.b.⊕a.,"OrDistributivity"a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.),"OrIdempotence"a.a.⊕a.,"Transposition"⊕b.⊕
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
a.
∀
{a.,b.}
∀
{a.,b.}
a.⊕b.
a.
b.
∀
{a.,b.}
a.⊗b.
a.
b.
∀
a.
a.
∀
{a.,b.}
b.
∀
{a.,b.}
b.
∀
{a.,b.}
a.
b.
∀
{a.,b.}
a.
∀
{a.,b.}
a.
b.
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
a.
∀
{a.,b.}
a.
b.
a.
Huntington Axioms
Huntington Axioms
No new theorems......