NKS page 778:
ResourceFunction["MultiwaySystem"][{"A""BAB","BB""A","AA""B"},{"BAB"},4]
In[]:=
{{BAB},{BBABB},{AABB,BBAA,BBBABBB},{AAA,ABABBB,BAABBB,BABABB,BBABAB,BBB,BBBAAB,BBBABA,BBBBABBBB},{AABAB,AB,ABAAB,ABABA,ABBABBBB,BA,BAAAB,BAABA,BABAA,BABABBBB,BABBABBB,BBAABBBB,BBABABBB,BBABBABB,BBBABABB,BBBABBAB,BBBBAABB,BBBBABAB,BBBBABBA,BBBBB,BBBBBABBBBB}}
Out[]=
FindStringReplacePath[{"A""BAB","BB""A","AA""B"},"A","AA"]
In[]:=
{A,BAB,BBABB,AABB,ABABBB,ABBABBBB,AAABBBB,AAAABB,AAAAA,AAAB,ABB,AA}
Out[]=
FindStringReplacePath[{"A""BAB","BB""A","AA""B"},"B","A"]
In[]:=
Failure
Out[]=
FindStringReplacePath[{"A""BAB","BB""A","AA""B"},"A","B"]
In[]:=
{A,BAB,BBABB,AABB,ABABBB,ABBABBBB,AAABBBB,AAAABB,AAAAA,AAAB,ABB,AA,B}
Out[]=
NKS proof length examples
NKS proof length examples
https://www.wolframscience.com/nks/p796--implications-for-mathematics-and-its-foundations/
{{BBB,BBB},{BAA,AAAB},{BABA,A},{BBB,BBA},{BABA,AAB,BBA},{BABA,AAB,BBAB},{BBAB,ABABB,BBAA},{BBA,BAAABB,BABB}}
Out[]=
strings=(StringJoin[#/.{1"B",0"A"}])&/@Rest/@IntegerDigits[Range[2,31],2]
In[]:=
{A,B,AA,AB,BA,BB,AAA,AAB,ABA,ABB,BAA,BAB,BBA,BBB,AAAA,AAAB,AABA,AABB,ABAA,ABAB,ABBA,ABBB,BAAA,BAAB,BABA,BABB,BBAA,BBAB,BBBA,BBBB}
Out[]=
Function[ru,FindStringReplacePath[ru,"B",#,MaxItems1000]&/@strings]/@{{"B""BB","BB""B"},{"B""AA","AA""AB"},{"B""ABA","A"""},{"B""BB","BB""A"},{"B""ABA","AA""B","BB""A"},{"B""ABA","AA""B","BB""AB"},{"B""BAB","ABAB""B","BB""AA"},{"B""BA","BAA""ABB","BAB""B"}}
In[]:=
$Aborted
Out[]=
Function[ru,FindStringReplacePath[ru,"B",#,MaxItems100,TimeConstraint2]&/@strings]/@{{"B""AA","AA""AB"}}
In[]:=
Failure,Failure,{B,AA},{B,AA,AB},Failure,Failure,{B,AA,AB,AAA},{B,AA,AB,AAA,AAB},{B,AA,AB,AAA,ABA},{B,AA,AB,AAA,AAB,ABB},Failure,Failure,Failure,Failure,{B,AA,AB,AAA,AAB,AAAA},{B,AA,AB,AAA,AAB,AAAA,AAAB},{B,AA,AB,AAA,AAB,AAAA,AABA},{B,AA,AB,AAA,AAB,AAAA,AAAB,AABB},{B,AA,AB,AAA,AAB,AAAA,ABAA},{B,AA,AB,AAA,AAB,AAAA,AAAB,ABAB},{B,AA,AB,AAA,AAB,AAAA,AABA,ABBA},{B,AA,AB,AAA,AAB,AAAA,AAAB,AABB,ABBB},Failure,Failure,Failure,Failure,Failure,Failure,Failure,Failure
Out[]=
results=Function[ru,ResourceFunction["ParallelMapMonitored"][FindStringReplacePath[ru,"B",#,MaxItems1000,TimeConstraint2]&,strings]]/@{{"B""BB","BB""B"},{"B""AA","AA""AB"},{"B""ABA","A"""},{"B""BB","BB""A"},{"B""ABA","AA""B","BB""A"},{"B""ABA","AA""B","BB""AB"},{"B""BAB","ABAB""B","BB""AA"},{"B""BA","BAA""ABB","BAB""B"}};
In[]:=
Map[If[Head[#]===Failure,Infinity,Length[#]]&,results,{2}]
In[]:=
{{∞,1,∞,∞,∞,2,∞,∞,∞,∞,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,4},{∞,∞,2,3,∞,∞,4,5,5,6,∞,∞,∞,∞,6,7,7,8,7,8,8,9,∞,∞,∞,∞,∞,∞,∞,∞},{∞,1,∞,3,3,∞,∞,5,2,∞,5,∞,∞,∞,∞,7,4,∞,4,∞,∞,∞,7,∞,∞,∞,∞,∞,∞,∞},{3,∞,6,4,4,2,9,7,7,5,7,5,5,3,12,10,10,8,10,8,8,6,10,8,8,6,8,6,6,4},{13,1,9,6,6,12,5,11,2,8,11,8,8,5,10,7,7,4,7,13,13,10,7,13,13,10,4,10,10,∞},{∞,1,∞,9,∞,8,∞,7,2,6,∞,6,11,5,∞,5,10,4,5,9,9,8,∞,14,9,13,4,8,8,12},{∞,1,5,10,∞,4,∞,8,∞,∞,8,2,∞,7,∞,6,∞,11,∞,11,∞,∞,6,∞,∞,5,11,5,∞,∞},{∞,1,∞,6,2,∞,∞,11,7,4,3,∞,∞,∞,∞,16,12,9,8,5,5,∞,4,∞,∞,∞,∞,∞,∞,∞}}
Out[]=
One Example of Shortening
One Example of Shortening
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},5,"StatesGraph"]
In[]:=
Out[]=
Consider each possible lemma; how much does it shorten the results?
LayeredGraphPlot[ResourceFunction["MultiwaySystem"][{"A""AB","BB""A","A""AA"},{"A"},4,"StatesGraph"]]
In[]:=
Out[]=
Shortening due to a particular lemma
Shortening due to a particular lemma
Map[Length[FindStringReplacePath[{"A""AB","BB""A","A""AA"},"A",#]]&,ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},7],{2}]
In[]:=
{{1},{2},{3},{2,4},{3,3,5},{4,4,4,6},{3,5,5,5,5,7},{4,4,6,4,6,6,6,6,8}}
Out[]=
Map[Length[FindStringReplacePath[{"A""AB","BB""A","A""AA"},"A",#]]&,ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},9],{2}]
In[]:=
{{1},{2},{3},{2,4},{3,3,5},{4,4,4,6},{3,5,5,5,5,7},{4,4,6,4,6,6,6,6,8},{5,5,5,7,5,5,7,5,7,7,7,7,9},{4,6,6,6,6,8,6,6,6,8,6,6,8,6,8,8,8,8,10}}
Out[]=
MapIndexed[First[#2]-#&,%]
In[]:=
{{0},{0},{0},{2,0},{2,2,0},{2,2,2,0},{4,2,2,2,2,0},{4,4,2,4,2,2,2,2,0},{4,4,4,2,4,4,2,4,2,2,2,2,0},{6,4,4,4,4,2,4,4,4,2,4,4,2,4,2,2,2,2,0}}
Out[]=
N[Mean[#]]&/@%
In[]:=
Linear improvement with this lemma....
Consider all A ... lemmas
Consider all A ... lemmas
This looks at shortening of A... paths
Consider AA ... lemmas
Consider AA ... lemmas
The lemmas become more irrelevant if we are not looking at shortening paths that do not reach as far as they do
Bulk lemma measurements
Bulk lemma measurements
Enumeration of Rules
Enumeration of Rules
What is the proof length for a particular string?
What is the proof length for a particular string?
Note: see Metamath-LongProofs-01
Note: see Metamath-LongProofs-01
Proof Shorteners
Proof Shorteners
Lemmas are not general-purpose proof shorteners ... they only shorten in particular “direction” in metamathematical space....
Lemmas are not general-purpose proof shorteners ... they only shorten in particular “direction” in metamathematical space....
If a particular lemma is going to be used on several distinct strings, it must be operating on different substrings
With enough lemmas
With enough lemmas
Terminating Rules
Terminating Rules