In[]:=
2+2
Out[]=
4
In[]:=
gg=
;
In[]:=
VertexCount[gg]
Out[]=
387
In[]:=
VertexList[gg]
Out[]=
In[]:=
stheorems=a.a.⋀a.,a.a.⋁a.,a.⋀b.b.⋀a.,a.⋁b.b.⋁a.,a.a.,a.a.⋀(a.⋁b.),a.a.⋁a.⋀b.,a.⋀a.b.⋀b.,a.⋁a.b.⋁b.,a.⋀b.a.⋀(a.⋀b.),(a.⋀b.)⋀c.a.⋀(b.⋀c.),(a.⋁b.)⋁c.a.⋁(b.⋁c.),a.⋁b.⋀c.(a.⋁b.)⋀(a.⋁c.),a.⋀(b.⋁c.)a.⋀b.⋁a.⋀c.,(a.⋁b.)a.⋀b.,(a.⋀b.)a.⋁b.,a.a.⋁b.⋀b.,a.a.⋀(b.⋁b.),a.⋁b.a.⋁a.⋀b.,a.⋁b.b.⋁a.;
∀
a.
∀
a.
∀
{a.,b.}
∀
{a.,b.}
∀
a.
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
In[]:=
toProve=(Delete[#,0]&/@stheorems)[[2;;;;2]]
Out[]=
{a.a.⋀a.,a.a.⋁a.,a.⋀b.b.⋀a.,a.⋁b.b.⋁a.,a.a.,a.a.⋀(a.⋁b.),a.a.⋁a.⋀b.,a.⋀a.b.⋀b.,a.⋁a.b.⋁b.,a.⋀b.a.⋀(a.⋀b.),(a.⋀b.)⋀c.a.⋀(b.⋀c.),(a.⋁b.)⋁c.a.⋁(b.⋁c.),a.⋁b.⋀c.(a.⋁b.)⋀(a.⋁c.),a.⋀(b.⋁c.)a.⋀b.⋁a.⋀c.,(a.⋁b.)a.⋀b.,(a.⋀b.)a.⋁b.,a.a.⋁b.⋀b.,a.a.⋀(b.⋁b.),a.⋁b.a.⋁a.⋀b.,a.⋁b.b.⋁a.}
In[]:=
Position[VertexList[gg],#]&/@toProve
Out[]=
{{},{},{{307,1,1}},{{143,1,1}},{{125,1,1}},{},{},{{354,1,1}},{{238,1,1}},{},{{378,1,1}},{{260,1,1}},{},{},{{129,1,1}},{{138,1,1}},{},{},{},{}}
In[]:=
Graph[gg,VertexSize(#If[!FreeQ[#,Alternatives@@{a.,b.,c.}],10,1]&/@VertexList[gg])]
Out[]=
Graph[gg,VertexSize(#If[!FreeQ[#,Alternatives@@{a.,b.,c.}],10,1]&/@VertexList[gg])]
In[]:=
Select[VertexList[gg],!FreeQ[#,Alternatives@@{a.,b.,c.}]&]
Out[]=
{
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
}
a.·b.a.⋁b. |
a.a. |
(a.⋁b.)a.⋀b. |
(a.⋀b.)a.⋁b. |
a.⋁a.a. |
a.⋁b.b.⋁a. |
a.⋁a.b.⋁b. |
a.⋁a.b.⋁b. |
a.⋁a.⋀b.a. |
a.⋁b.⋀b.a. |
a.⋁a.⋀b.a.⋁b. |
a.⋁a.b.⋁b. |
b.⋁a.a.⋁b. |
(a.⋁b.)⋁c.a.⋁(b.⋁c.) |
(b.⋁a.)⋁c.a.⋁(b.⋁c.) |
(b.⋁b.)⋁a.b.⋁a. |
(b.⋁b.)⋁a.a.⋁b. |
a.⋀b.⋁a.⋀c.a.⋀(b.⋁c.) |
a.⋀b.⋁c.⋀a.a.⋀(b.⋁c.) |
a.⋀b.⋁c.⋀a.a.⋀(c.⋁b.) |
a.⋀a.a. |
a.⋀b.b.⋀a. |
a.⋀a.b.⋀b. |
a.⋀a.b.⋀b. |
a.⋀(a.⋁b.)a. |
a.⋀(b.⋁b.)a. |
a.⋀(a.⋀b.)a.⋀b. |
a.⋀a.b.⋀b. |
(a.⋁b.)⋀(a.⋁c.)a.⋁b.⋀c. |
(a.⋀b.)⋀c.a.⋀(b.⋀c.) |
(b.⋀a.)⋀c.a.⋀(b.⋀c.) |
In[]:=
Length[%]
Out[]=
31
In[]:=
Length[toProve]
Out[]=
20
In[]:=
Complement[%9,toProve]
Out[]=
{
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
}
a.·b.a.⋁b. |
a.a. |
(a.⋁b.)a.⋀b. |
(a.⋀b.)a.⋁b. |
a.⋁a.a. |
a.⋁b.b.⋁a. |
a.⋁a.b.⋁b. |
a.⋁a.b.⋁b. |
a.⋁a.⋀b.a. |
a.⋁b.⋀b.a. |
a.⋁a.⋀b.a.⋁b. |
a.⋁a.b.⋁b. |
b.⋁a.a.⋁b. |
(a.⋁b.)⋁c.a.⋁(b.⋁c.) |
(b.⋁a.)⋁c.a.⋁(b.⋁c.) |
(b.⋁b.)⋁a.b.⋁a. |
(b.⋁b.)⋁a.a.⋁b. |
a.⋀b.⋁a.⋀c.a.⋀(b.⋁c.) |
a.⋀b.⋁c.⋀a.a.⋀(b.⋁c.) |
a.⋀b.⋁c.⋀a.a.⋀(c.⋁b.) |
a.⋀a.a. |
a.⋀b.b.⋀a. |
a.⋀a.b.⋀b. |
a.⋀a.b.⋀b. |
a.⋀(a.⋁b.)a. |
a.⋀(b.⋁b.)a. |
a.⋀(a.⋀b.)a.⋀b. |
a.⋀a.b.⋀b. |
(a.⋁b.)⋀(a.⋁c.)a.⋁b.⋀c. |
(a.⋀b.)⋀c.a.⋀(b.⋀c.) |
(b.⋀a.)⋀c.a.⋀(b.⋀c.) |
In[]:=
Length[%12]
Out[]=
31
In[]:=
toProve
Out[]=
{a.a.⋀a.,a.a.⋁a.,a.⋀b.b.⋀a.,a.⋁b.b.⋁a.,a.a.,a.a.⋀(a.⋁b.),a.a.⋁a.⋀b.,a.⋀a.b.⋀b.,a.⋁a.b.⋁b.,a.⋀b.a.⋀(a.⋀b.),(a.⋀b.)⋀c.a.⋀(b.⋀c.),(a.⋁b.)⋁c.a.⋁(b.⋁c.),a.⋁b.⋀c.(a.⋁b.)⋀(a.⋁c.),a.⋀(b.⋁c.)a.⋀b.⋁a.⋀c.,(a.⋁b.)a.⋀b.,(a.⋀b.)a.⋁b.,a.a.⋁b.⋀b.,a.a.⋀(b.⋁b.),a.⋁b.a.⋁a.⋀b.,a.⋁b.b.⋁a.}
In[]:=
FullForm[a.a.]
Out[]//FullForm=
Equal[Square[Square[\[FormalA]]],\[FormalA]]
In[]:=
FullForm[
]
a.a. |
Out[]//FullForm=
Column[List[Equal[Square[Square[\[FormalA]]],\[FormalA]]],Rule[ItemSize,List[Automatic,Automatic]]]
In[]:=
TransitiveReductionGraph[gg]
Out[]=