You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
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,AlignmentRight]
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}]
1
0
Out[]=
ComplexInfinity,2,1,,2,,,,,,,,,,,,,,,
2
3
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
1
0
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[]=
IfHead[Last[#]]===Failure,FramedTraditionalForm[LogicFormat[First[#]]],Background,FrameStyleRGBColor["#f7c5b2"],RoundingRadius3,FrameMarginsNone,Graph[Last[#]["ProofGraph"],VertexLabelsNone,ImageSize{Automatic,50}]&/@Take[provable,70]//TraditionalForm
In[]:=
dependencyNetworkSimplified
Out[]=
In[]:=
branchialGraph[%]
Out[]=
$Aborted
In[]:=
branchialGraph[dependencyNetworkSimplified,1]
Out[]=
Theorem Lookback
Theorem Lookback
Proving Notable Theorems from Axioms
Proving Notable Theorems from Axioms