MultiwayOperatorSystem
MultiwayOperatorSystem
Notable Boolean Theorems
Notable Boolean Theorems
NKS source
NKS source
Result
Result
[[ Excluding theorems already in AxiomaticTheory ]]
In[]:=
ithms="AndIdempotence"a.a.⊗a.,"OrIdempotence"a.a.⊕a.,"AndCommutativity"a.⊗b.b.⊗a.,"OrCommutativity"a.⊕b.b.⊕a.,"Noncontradiction"⊗a.⊗b.,"ExcludedMiddle"⊕a.⊕b.,"AndPreAssociativity"a.⊗b.a.⊗(a.⊗b.),"Absorption"a.a.⊗(a.⊕b.),"AbsorptionOrAnd"a.a.⊕a.⊗b.,"Transposition"⊕b.⊕,"AndAssociativity"(a.⊗b.)⊗c.a.⊗(b.⊗c.),"OrAssociativity"(a.⊕b.)⊕c.a.⊕(b.⊕c.),"NegationRedundancy"a.⊕b.a.⊕⊗b.,"DroppingAlwaysTrue"a.a.⊕b.⊗,"DroppingAlwaysFalse"a.a.⊗b.⊕,"OrDistributivity"a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.),"AndDistributivity"a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.;
∀
a.
∀
a.
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
a.
b.
∀
{a.,b.}
a.
b.
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
a.
b.
a.
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.}
a.
∀
{a.,b.}
b.
∀
{a.,b.}
b.
∀
{a.,b.,c.}
∀
{a.,b.,c.}
In[]:=
Last/@%
Out[]=
AndIdempotencea.a.⊗a.,OrIdempotencea.a.⊕a.,AndCommutativitya.⊗b.b.⊗a.,OrCommutativitya.⊕b.b.⊕a.,Noncontradiction⊗a.⊗b.,ExcludedMiddle⊕a.⊕b.,AndPreAssociativitya.⊗b.a.⊗(a.⊗b.),Absorptiona.a.⊗(a.⊕b.),AbsorptionOrAnda.a.⊕a.⊗b.,Transposition⊕b.⊕,AndAssociativity(a.⊗b.)⊗c.a.⊗(b.⊗c.),OrAssociativity(a.⊕b.)⊕c.a.⊕(b.⊕c.),NegationRedundancya.⊕b.a.⊕⊗b.,DroppingAlwaysTruea.a.⊕b.⊗,DroppingAlwaysFalsea.a.⊗b.⊕,OrDistributivitya.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.),AndDistributivitya.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.
a.
b.
a.
b.
a.
b.
a.
a.
b.
b.
In[]:=
LeafCount/@%
Out[]=
AndIdempotence5,OrIdempotence5,AndCommutativity7,OrCommutativity7,Noncontradiction9,ExcludedMiddle9,AndPreAssociativity9,Absorption7,AbsorptionOrAnd7,Transposition11,AndAssociativity11,OrAssociativity11,NegationRedundancy10,DroppingAlwaysTrue8,DroppingAlwaysFalse8,OrDistributivity13,AndDistributivity13
In[]:=
Sort[%]
Out[]=
AndIdempotence5,OrIdempotence5,AndCommutativity7,OrCommutativity7,Absorption7,AbsorptionOrAnd7,DroppingAlwaysTrue8,DroppingAlwaysFalse8,Noncontradiction9,ExcludedMiddle9,AndPreAssociativity9,NegationRedundancy10,Transposition11,AndAssociativity11,OrAssociativity11,OrDistributivity13,AndDistributivity13
In[]:=
FindEquationalProof[#,"BooleanAxioms"]&/@ithms
Out[]=
Running MW
Running MW
In[]:=
Last/@AxiomaticTheory["BooleanAxioms"]
Out[]=
a.⊗b.b.⊗a.,a.⊕b.b.⊕a.,a.⊗b.⊕a.,a.⊕b.⊗a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
b.
b.
In[]:=
rules=(#1/.{a.a_,b.b_,c.c_})(#2/.{a.a,b.b,c.c})&@@@Join[#,Reverse/@#]&a.⊗b.b.⊗a.,a.⊕b.b.⊕a.,a.⊗b.⊕a.,a.⊕b.⊗a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
b.
b.
Out[]=
a_⊗b_b⊗a,a_⊕b_b⊕a,a_⊗(b_⊕)a,a_⊕b_⊗a,a_⊗(b_⊕c_)a⊗b⊕a⊗c,a_⊕b_⊗c_(a⊕b)⊗(a⊕c),b_⊗a_a⊗b,b_⊕a_a⊕b,a_a⊗(b⊕),a_a⊕b⊗,a_⊗b_⊕a_⊗c_a⊗(b⊕c),(a_⊕b_)⊗(a_⊕c_)a⊕b⊗c
b_
b_
b
b
In[]:=
MultiwayOperatorSystem[rules,{p⊕},2]
p
Out[]=
{{CirclePlus[p, OverBar[p]]},{CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]],CirclePlus[OverBar[p], p],CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]]},{CirclePlus[CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]], CircleTimes[b, OverBar[b]]],CirclePlus[CirclePlus[OverBar[p], p], CircleTimes[b, OverBar[b]]],CirclePlus[CircleTimes[b, OverBar[b]], CirclePlus[p, OverBar[p]]],CirclePlus[CircleTimes[CirclePlus[p, OverBar[p]], b], CircleTimes[CirclePlus[p, OverBar[p]], OverBar[b]]],CirclePlus[CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]], CircleTimes[b, OverBar[b]]],CirclePlus[p, OverBar[p]],CircleTimes[CirclePlus[b, OverBar[b]], CirclePlus[p, OverBar[p]]],CircleTimes[CirclePlus[CirclePlus[p, OverBar[p]], b], CirclePlus[CirclePlus[p, OverBar[p]], OverBar[b]]],CircleTimes[CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]], CirclePlus[b, OverBar[b]]],CircleTimes[CirclePlus[OverBar[p], p], CirclePlus[b, OverBar[b]]],CircleTimes[CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]], CirclePlus[b, OverBar[b]]]}}
In[]:=
Map[ToExpression,MultiwayOperatorSystem[rules,{p⊕},2],{2}]
p
Out[]=
{p⊕},(p⊕)⊕b⊗,⊕p,(p⊕)⊗(b⊕),(p⊕)⊕b⊗⊕b⊗,(⊕p)⊕b⊗,b⊗⊕(p⊕),(p⊕)⊗b⊕(p⊕)⊗,(p⊕)⊗(b⊕)⊕b⊗,p⊕,(b⊕)⊗(p⊕),((p⊕)⊕b)⊗(p⊕)⊕,(p⊕)⊕b⊗⊗(b⊕),(⊕p)⊗(b⊕),(p⊕)⊗(b⊕)⊗(b⊕)
p
p
b
p
p
b
p
b
b
p
b
b
p
p
p
b
p
b
b
p
b
p
p
p
b
p
b
b
p
b
p
b
b
In[]:=
MultiwayOperatorSystem[rules,{p⊕},2,"StatesGraph"]
p
Out[]=
In[]:=
VertexList[%]
Out[]=
{CirclePlus[p, OverBar[p]],CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]],CirclePlus[OverBar[p], p],CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]],CirclePlus[CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]], CircleTimes[b, OverBar[b]]],CirclePlus[CirclePlus[OverBar[p], p], CircleTimes[b, OverBar[b]]],CirclePlus[CircleTimes[b, OverBar[b]], CirclePlus[p, OverBar[p]]],CirclePlus[CircleTimes[CirclePlus[p, OverBar[p]], b], CircleTimes[CirclePlus[p, OverBar[p]], OverBar[b]]],CirclePlus[CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]], CircleTimes[b, OverBar[b]]],CircleTimes[CirclePlus[b, OverBar[b]], CirclePlus[p, OverBar[p]]],CircleTimes[CirclePlus[CirclePlus[p, OverBar[p]], b], CirclePlus[CirclePlus[p, OverBar[p]], OverBar[b]]],CircleTimes[CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]], CirclePlus[b, OverBar[b]]],CircleTimes[CirclePlus[OverBar[p], p], CirclePlus[b, OverBar[b]]],CircleTimes[CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]], CirclePlus[b, OverBar[b]]]}
In[]:=
FullForm[%]
Out[]//FullForm=
List["CirclePlus[p, OverBar[p]]","CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]]","CirclePlus[OverBar[p], p]","CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]]","CirclePlus[CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]], CircleTimes[b, OverBar[b]]]","CirclePlus[CirclePlus[OverBar[p], p], CircleTimes[b, OverBar[b]]]","CirclePlus[CircleTimes[b, OverBar[b]], CirclePlus[p, OverBar[p]]]","CirclePlus[CircleTimes[CirclePlus[p, OverBar[p]], b], CircleTimes[CirclePlus[p, OverBar[p]], OverBar[b]]]","CirclePlus[CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]], CircleTimes[b, OverBar[b]]]","CircleTimes[CirclePlus[b, OverBar[b]], CirclePlus[p, OverBar[p]]]","CircleTimes[CirclePlus[CirclePlus[p, OverBar[p]], b], CirclePlus[CirclePlus[p, OverBar[p]], OverBar[b]]]","CircleTimes[CirclePlus[CirclePlus[p, OverBar[p]], CircleTimes[b, OverBar[b]]], CirclePlus[b, OverBar[b]]]","CircleTimes[CirclePlus[OverBar[p], p], CirclePlus[b, OverBar[b]]]","CircleTimes[CircleTimes[CirclePlus[p, OverBar[p]], CirclePlus[b, OverBar[b]]], CirclePlus[b, OverBar[b]]]"]
In[]:=
MultiwayOperatorSystem[rules,{p⊕},3,"StatesGraphStructure"]
p
Out[]=