In[]:=
Table[Tuples[{a},i],{i,4}]
Out[]=
{{{a}},{{a,a}},{{a,a,a}},{{a,a,a,a}}}
In[]:=
Groupings[#,{CircleTimes2,CirclePlus2,OverBar1}]&/@Table[Tuples[{a,b},i],{i,3}]
Out[]=

a
,
b
,
a
⊗a,
a
⊗b,
b
⊗a,
b
⊗b,a⊗
a
,a⊗
b
,b⊗
a
,b⊗
b
,
a⊗a
,
a⊗b
,
b⊗a
,
b⊗b
,
a
⊗a,
a
⊗b,
b
⊗a,
b
⊗b,a⊗
a
,a⊗
b
,
⋯37⋯
,b⊕
b
,
a
⊕
a
,
a
⊕
b
,
b
⊕
a
,
b
⊕
b
,
a
⊕a
,
a
⊕b
,
b
⊕a
,
b
⊕b
,
a⊕
a
,
a⊕
b
,
b⊕
a
,
b⊕
b
,
a⊕a
,
a⊕b
,
b⊕a
,
b⊕b
,(
a
⊗a)⊗a,(
a
⊗a)⊗b,(
a
⊗b)⊗a,(
a
⊗b)⊗b,
⋯3513⋯
,
b⊕(a⊕b)
,
b⊕(b⊕a)
,
b⊕(b⊕b)

large output
show less
show more
show all
set size limit...
In[]:=
Cases[Equal@@@Tuples[Flatten[Groupings[#,{CircleTimes2,CirclePlus2,OverBar1}]&/@Table[Tuples[{a,b},i],{i,2}]],2],_Equal]
Out[]=

a

b
,
a

a
⊗a,
a

a
⊗b,
a

b
⊗a,
a

b
⊗b,
a
a⊗
a
,
a
a⊗
b
,
a
b⊗
a
,
a
b⊗
b
,
a

a⊗a
,
a

a⊗b
,
a

b⊗a
,
a

b⊗b
,
⋯5377⋯
,
b⊕b

b
⊕
b
,
b⊕b

a
⊕a
,
b⊕b

a
⊕b
,
b⊕b

b
⊕a
,
b⊕b

b
⊕b
,
b⊕b

a⊕
a
,
b⊕b

a⊕
b
,
b⊕b

b⊕
a
,
b⊕b

b⊕
b
,
b⊕b

a⊕a
,
b⊕b

a⊕b
,
b⊕b

b⊕a

large output
show less
show more
show all
set size limit...
In[]:=
DepthLeafSort[%]
Out[]=

a

b
,
b

a
,
a

a
⊗a,
a
a⊗
a
,
a

a⊗a
,
a

a
⊕a,
a
a⊕
a
,
a

a⊕a
,
a
⊗a
a
,a⊗
a

a
,
a⊗a

a
,
a
⊕a
a
,a⊕
a

a
,
a⊕a

a
,
a

a
⊗b,
⋯5373⋯
,
b⊕
b

b
⊕
b
,
b⊕
b

b
⊕b
,
b⊕
b

b⊕b
,
b⊕b

b
⊗b,
b⊕b
b⊗
b
,
b⊕b

b
⊗
b
,
b⊕b

b
⊗b
,
b⊕b

b⊗
b
,
b⊕b

b⊗b
,
b⊕b

b
⊕b,
b⊕b
b⊕
b
,
b⊕b

b
⊕
b
,
b⊕b

b
⊕b
,
b⊕b

b⊕
b

large output
show less
show more
show all
set size limit...
In[]:=
AxiomaticTheory["BooleanAxioms"]
Out[]=

∀
{a.,b.}
a.⊗b.b.⊗a.,
∀
{a.,b.}
a.⊕b.b.⊕a.,
∀
{a.,b.}
a.⊗b.⊕
b.
a.,
∀
{a.,b.}
a.⊕b.⊗
b.
a.,
∀
{a.,b.,c.}
a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,
∀
{a.,b.,c.}
a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
In[]:=
FindEquationalProof[#,"BooleanAxioms"]&/@Take[%141,20]
Out[]=
$Aborted
First, determine true theorems using models.....