MultiwayOperatorSystem


Notable Boolean Theorems

NKS source


Result

[[ Excluding theorems already in AxiomaticTheory ]]
In[]:=
ithms="AndIdempotence"
∀
a.
a.a.⊗a.,"OrIdempotence"
∀
a.
a.a.⊕a.,"AndCommutativity"
∀
{a.,b.}
a.⊗b.b.⊗a.,"OrCommutativity"
∀
{a.,b.}
a.⊕b.b.⊕a.,"Noncontradiction"
∀
{a.,b.}
a.
⊗a.
b.
⊗b.,"ExcludedMiddle"
∀
{a.,b.}
a.
⊕a.
b.
⊕b.,"AndPreAssociativity"
∀
{a.,b.}
a.⊗b.a.⊗(a.⊗b.),"Absorption"
∀
{a.,b.}
a.a.⊗(a.⊕b.),"AbsorptionOrAnd"
∀
{a.,b.}
a.a.⊕a.⊗b.,"Transposition"
∀
{a.,b.}
a.
⊕b.
b.
⊕
a.
,"AndAssociativity"
∀
{a.,b.,c.}
(a.⊗b.)⊗c.a.⊗(b.⊗c.),"OrAssociativity"
∀
{a.,b.,c.}
(a.⊕b.)⊕c.a.⊕(b.⊕c.),"NegationRedundancy"
∀
{a.,b.}
a.⊕b.a.⊕
a.
⊗b.,"DroppingAlwaysTrue"
∀
{a.,b.}
a.a.⊕b.⊗
b.
,"DroppingAlwaysFalse"
∀
{a.,b.}
a.a.⊗b.⊕
b.
,"OrDistributivity"
∀
{a.,b.,c.}
a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.),"AndDistributivity"
∀
{a.,b.,c.}
a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.;
In[]:=
Last/@%
Out[]=
AndIdempotencea.a.⊗a.,OrIdempotencea.a.⊕a.,AndCommutativitya.⊗b.b.⊗a.,OrCommutativitya.⊕b.b.⊕a.,Noncontradiction
a.
⊗a.
b.
⊗b.,ExcludedMiddle
a.
⊕a.
b.
⊕b.,AndPreAssociativitya.⊗b.a.⊗(a.⊗b.),Absorptiona.a.⊗(a.⊕b.),AbsorptionOrAnda.a.⊕a.⊗b.,Transposition
a.
⊕b.
b.
⊕
a.
,AndAssociativity(a.⊗b.)⊗c.a.⊗(b.⊗c.),OrAssociativity(a.⊕b.)⊕c.a.⊕(b.⊕c.),NegationRedundancya.⊕b.a.⊕
a.
⊗b.,DroppingAlwaysTruea.a.⊕b.⊗
b.
,DroppingAlwaysFalsea.a.⊗b.⊕
b.
,OrDistributivitya.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.),AndDistributivitya.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.
In[]:=
LeafCount/@%
Out[]=
AndIdempotence5,OrIdempotence5,AndCommutativity7,OrCommutativity7,Noncontradiction9,ExcludedMiddle9,AndPreAssociativity9,Absorption7,AbsorptionOrAnd7,Transposition11,AndAssociativity11,OrAssociativity11,NegationRedundancy10,DroppingAlwaysTrue8,DroppingAlwaysFalse8,OrDistributivity13,AndDistributivity13
In[]:=
Sort[%]
Out[]=
AndIdempotence5,OrIdempotence5,AndCommutativity7,OrCommutativity7,Absorption7,AbsorptionOrAnd7,DroppingAlwaysTrue8,DroppingAlwaysFalse8,Noncontradiction9,ExcludedMiddle9,AndPreAssociativity9,NegationRedundancy10,Transposition11,AndAssociativity11,OrAssociativity11,OrDistributivity13,AndDistributivity13
In[]:=
FindEquationalProof[#,"BooleanAxioms"]&/@ithms
Out[]=

Running MW

In[]:=
Last/@AxiomaticTheory["BooleanAxioms"]
Out[]=
a.⊗b.b.⊗a.,a.⊕b.b.⊕a.,a.⊗b.⊕
b.
a.,a.⊕b.⊗
b.
a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
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.⊕
b.
a.,a.⊕b.⊗
b.
a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
Out[]=
a_⊗b_b⊗a,a_⊕b_b⊕a,a_⊗(b_⊕
b_
)a,a_⊕b_⊗
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⊕
b
),a_a⊕b⊗
b
,a_⊗b_⊕a_⊗c_a⊗(b⊕c),(a_⊕b_)⊗(a_⊕c_)a⊕b⊗c
In[]:=
MultiwayOperatorSystem[rules,{p⊕
p
},2]
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⊕
p
},2],{2}]
Out[]=
{p⊕
p
},(p⊕
p
)⊕b⊗
b
,
p
⊕p,(p⊕
p
)⊗(b⊕
b
),(p⊕
p
)⊕b⊗
b
⊕b⊗
b
,(
p
⊕p)⊕b⊗
b
,b⊗
b
⊕(p⊕
p
),(p⊕
p
)⊗b⊕(p⊕
p
)⊗
b
,(p⊕
p
)⊗(b⊕
b
)⊕b⊗
b
,p⊕
p
,(b⊕
b
)⊗(p⊕
p
),((p⊕
p
)⊕b)⊗(p⊕
p
)⊕
b
,(p⊕
p
)⊕b⊗
b
⊗(b⊕
b
),(
p
⊕p)⊗(b⊕
b
),(p⊕
p
)⊗(b⊕
b
)⊗(b⊕
b
)
In[]:=
MultiwayOperatorSystem[rules,{p⊕
p
},2,"StatesGraph"]
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⊕
p
},3,"StatesGraphStructure"]
Out[]=