In[]:=
AONTrees[e_,1]=e;​​​​​​AONTrees[e_,n_]:=Flatten[{Function[{xxx},Table[Outer[xxx,AONTrees[e,n-r-1],AONTrees[e,r]],{r,n-2}]]/@{and,or},Outer[not,AONTrees[e,n-1]]}]​​​​​​ToAONCode[expr_,m_]:=Module[{fn},fn=Apply[Function,{expr}];Block[{and=Times,or=(Sign[(#1+#2)]&),not=(1-#1&)},FromDigits[fn@@@Tuples[{1,0},m],2]]]​​​​​​FindAONTheorems[max_,nvar_]:=(Map[Last,Split[Sort[{ToAONCode[#,nvar],#}&/@Flatten[Table[AONTrees[Slot/@Range[nvar],i],{i,max}],1]],First[#1]==First[#2]&],{2}]/.{#1->a,#2->b,#3->c})​​​​​​FindAONTheoremsList[max_,nvar_]:=Flatten[Module[{u={ToAONCode[#,nvar],#}&/@DepthLeafSort[Flatten[Table[AONTrees[Slot/@Range[nvar],i],{i,max}],1]]},Table[Thread[Last/@u[[Flatten[Position[First/@Take[u,n-1],u[[n,1]]]]]]==u[[n,2]]],{n,Length[u]}]]/.{#1->a,#2->b,#3->c,and->Wedge,or->Vee,not->Square}]​​​​​​DepthLeafSort[list_List]:=Flatten[Map[SortBy[#1,{Cases[#,_?AtomQ,{0,∞}]&}]&,(SplitBy[SortBy[#1,{LeafCount}],{LeafCount}]&)/@SplitBy[SortBy[list,{Depth}],{Depth}],{2}],3]​​​​​​DepthLeafSortArray[arr_]:=With[{list=DepthLeafSort/@arr},Flatten[Map[Sort[#1,OrderedQ[{Cases[#1[[1]],_?AtomQ,{0,∞}],Cases[#2[[1]],_?AtomQ,{0,∞}]}]&]&,(Split[Sort[#1,LeafCount[First@#1]<LeafCount[First@#2]&],LeafCount[#1[[1]]]==LeafCount[#1[[1]]]&]&)/@Split[Sort[DepthLeafSort/@list,Depth[First@#1]<Depth[First@#2]&],Depth[First@#1]==Depth[First@#2]&],{2}],2]]​​​​​​LowestQ[expr_,vars_]:=(First[DepthLeafSort[expr/.(Thread[vars->#]&/@Permutations[vars])]]===expr)​​​​​​data53=Select[FindAONTheoremsList[5,3],LowestQ[#,{a,b,c}]&];​​​​​​FindAONTheoremsListX[max_,nvar_]:=Flatten[Table[#[[i]]==#[[j]],{i,Length[#]},{j,i+1,Length[#]}]&/@DepthLeafSort/@FindAONTheorems[max,nvar]]/.{not->Square,and->Wedge,or->Vee}​​​​​​FindAllAON[max_,nvar_]:=Flatten[Module[{u={0,#}&/@DepthLeafSort[Flatten[Table[AONTrees[Slot/@Range[nvar],i],{i,max}],1]]},Table[Thread[Last/@u[[Flatten[Position[First/@Take[u,n-1],u[[n,1]]]]]]==u[[n,2]]],{n,Length[u]}]]/.{#1->a,#2->b,#3->c,and->Wedge,or->Vee,not->Square}]​​​​​​LogicFormat[expr_]:=HoldForm[expr]/.{Square->Not,Vee->Or,Wedge->And,a.->a,b.->b,c.->c}
In[]:=
Grid[Flatten/@Table[{Length@FindAllAON[p,n],Style[Length@FindAONTheorems[p,n],Background->LightBlue]},{p,5},{n,4}],Frame->All,FrameStyle->LightGray,AlignmentRight]
Out[]=
0
1
1
2
3
3
6
4
1
2
6
4
15
6
28
8
10
2
91
6
351
12
946
20
66
4
780
14
3486
32
10296
58
528
4
11781
14
84255
40
362526
90
In[]:=
Last/@%
Out[]=
{3,6,12,32,40}
In[]:=
Differences[%]
Out[]=
{3,6,20,8}
In[]:=
Table[Length@FindAllAON[p,n],{p,4},{n,3}]
Out[]=
{{0,1,3},{1,6,15},{10,91,351},{66,780,3486}}
In[]:=
Table[Length@FindAONTheorems[p,n]/Length@FindAllAON[p,n],{p,5},{n,4}]
Power
:Infinite expression
1
0
encountered.
Out[]=
ComplexInfinity,2,1,
2
3
,2,
2
3
,
2
5
,
2
7
,
1
5
,
6
91
,
4
117
,
10
473
,
2
33
,
7
390
,
16
1743
,
29
5148
,
1
132
,
2
1683
,
8
16851
,
15
60421

In[]:=
N[%]
Out[]=
{{ComplexInfinity,2.,1.,0.666667},{2.,0.666667,0.4,0.285714},{0.2,0.0659341,0.034188,0.0211416},{0.0606061,0.0179487,0.00917958,0.00563326},{0.00757576,0.00118835,0.000474749,0.000248258}}
In[]:=
Ratios/@%//N
Divide
:Infinite expression
1
0
encountered.
Out[]=
{{ComplexInfinity,3.,2.},{6.,2.5,1.86667},{9.1,3.85714,2.69516},{11.8182,4.46923,2.95353},{22.3125,7.15177,4.30272}}
In[]:=
CloudGet["https://wolfr.am/PO7vasDF"];
LogicFormat/@(interesting=First/@{{a==a⋀a,"idempotent law for and"},{a==a⋁a,"idempotent law for or"},{a⋀b==b⋀a,"commutativity for and"},{a⋁b==b⋁a,"commutativity for or"},{a==a,"law of double negation"},{a⋀a==b⋀b,"definition of false (law of noncontradiction)"},{a⋁a==b⋁b,"definition of true (law of excluded middle)"},{(a⋁b)==a⋀b,"de Morgan law"},{(a⋀b)==a⋁b,"de Morgan law"},{a==a⋀(a⋁b),"absorption law"},{a==a⋁a⋀b,"absorption law"},{(a⋀b)⋀c==a⋀(b⋀c),"associativity of and"},{(a⋁b)⋁c==a⋁(b⋁c),"associativity of or"}})//(TraditionalForm[Style[#,15]]&);
In[]:=
data53
Out[]=
{aa⋀a,aa⋁a,a⋀aa⋁a,a⋀bb⋀a,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⋀bb⋀a,a⋀bb⋀a,a⋁bb⋁a,a⋁bb⋁a,(a⋀b)(b⋀a),
⋯878⋯
,a⋀a⋁aa,(a⋁a)⋁aa,a⋁a⋀aa,a⋁(a⋁a)a,a⋀(a⋁b)a,a⋁a⋀ba,(a⋁b)⋀aa,a⋀(b⋁a)a,a⋀b⋁aa,a⋁b⋀aa,a⋀aa,a⋀aa,a⋁aa,a⋁aa,(a⋀a)a,(a⋁a)a,(a⋁b)⋀bb,a⋀b⋁bb}
large output
show less
show more
show all
set size limit...
IfHead[Last[#]]===Failure,FramedTraditionalForm[LogicFormat[First[#]]],Background
,FrameStyleRGBColor["#f7c5b2"],RoundingRadius3,FrameMarginsNone,Graph[Last[#]["ProofGraph"],VertexLabelsNone,ImageSize{Automatic,50}]&/@Take[provable,70]//TraditionalForm
In[]:=
dependencyNetworkSimplified
Out[]=
​
In[]:=
branchialGraph[%]
Out[]=
$Aborted
In[]:=
branchialGraph[dependencyNetworkSimplified,1]
Out[]=

Theorem Lookback

Proving Notable Theorems from Axioms