[Proof Minimization Challenge] Minimal 1-bases for C-N propositional calculus #2
xamidi
started this conversation in
Show and tell
Replies: 7 comments 9 replies
-
|
(reserved) |
Beta Was this translation helpful? Give feedback.
0 replies
-
w3: (A2: 2762055↦614905, A3: 182879↦51239, L1: 180451↦39253, L2: 2177↦1649) CpCCNqCCNrsCptCCtqCrq = 1
[0] CCCpCCqrCsrtCCCqrCsrt = DD1D111
[1] CCCNpCCNqCCNrsCNptCCtqCrqCCCrqpCqpCCCCCrqpCqpuCvu = DDD111D[0]D11
[2] CCCpCqrsCCqrs = DD1D[1]D111
[3] CCCCCpqrCqrsCts = DD[2]D111
[4] CCpqCCCpqrCsr = D[2]DDD1DD1111D[0]D1D11
[5] CCCpqrCqr = DDD[3]D[0]DD1111D11
[6] CCCNpqrCpr = DD11DD[1]D1D11[2]
[7] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1DDD1[0]1D[0]DD[3]11
[8] CCNppCqp = DD11D[6]D11
+ [9] CpCqp = DDD[3][3]11
[10] CCCCNpqCrqpCsp = DD11DDD[2]DD[0]111DD[0]D[0]D1D11[0]
[11] CCCNpqCCrCsCtsqCCquCpu = D[0]D1DD[3][3]1
[12] CpCCpqCrq = DDD1D11DDD[0]D[0]D1D[0]D1D11[0][2]D11
[13] CCCNCNpqrsCps = DD11DD[1]D1D11DD11DDD[0]D[0]D1[0]DD1DD1111[2]
[14] CpCqCrp = D[5]D[2]D[1]D11
[15] CCCCCNpqrCsrtCpt = DD[2]D1DDD[3]D[0]D[0]D1DDD1DD1111D[0]D1D111D111
[16] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[2]D1D[2]D1[9]
[17] CCCCCpqrCsrtCqt = DD[2]DD[0]D[2]1[8]1
+ [18] CpCNpq = D[6]DD[0]D11[8]
+ [19] Cpp = DD[6]DD11[12]1
[20] CNNCpqCrCpq = DD[10]DDDD1[0]1D[0]D1[2]D[10]DD1D11D[13]DDD11DDD[0]D[0]D1DDD1[0]1[0][2][2]D[1]D1D111
[21] CCNCCpCqpNrsCrs = DD[0]DD[3]11DD1[9][20]
[22] CCCpqpCrp = DD1[19]D[5]D[15]DD[0]DDD1DD1111D[0]D1D11[21]
[23] CCpqCCCrrNNpq = D[11]DD1[19]DD[11]DD1[19][20]D[6]D11
[24] CCCpqCNprCsCNpr = D[7]D[17]D[4]D[6]DD[2]D1DD[3][3]1D[6]DD1[9][20]
[25] CCpNpCqNp = D[7]D[17]D[4]DD[6]DD1[19]D[21][12]1
[26] CCpCqNpCrCqNp = DD1[19]D[5]DD[11]DD1[19]D[5]D[21][14]D[6]D11
[27] CCCpqrCNpr = DDDD1[19]D[17]D[4]D[6]DD[2]D1DD[3][3]1D[2]D[6]DD1[19][20][4]1
[28] CCpCqNCNppCrCqNCNpp = DD1[19]DD[10]D[4]D[5]DD[11]DD1[19]D[5]D[6]D[21][14][8]1
+ [29] CCNppp = D[21]DDDD11D[5]DDD1DD1[0]11DDD1[0]1D[1]D11DD[11]DD1[19]D[5]D[6]D[21][14][8]1
[30] CCNpqCNCrpq = D[16]D[7]D[5]DD[11]DD1[19]D[21]D[5]DDD1[0]1D[1]D11D[5]D[6][26]
[31] CNCpqCrCsp = DD[10]D[4]DD[10]D[4]DD[22]DD1[19]DD[24]D[6]DDD11DDD[0]D[0]D1[0][0]DD[2]D1D[3]D[1]D1[0]1[3]1111
[32] CCNpqCNCrCspq = D[16]D[7]D[5]D[23]D[5]D[2]D[6][26]
[33] CCpqCCNppq = DD[2]D1D1D11D[7]DD[16]DD[16]D[7]D[5]D[23]D[6][28]DD[10]D[4]DD[28]D[13]DD[0]D11[8]11[14]
[34] CCNCpqrCCrqCpq = DD[33]DD1[8]DDD[0]D[0]D1D[0]D11DD1[0]1[2]D[32]1
[35] CCpCpqCpq = DDD[7][31]D[7][31]DD[7][31]D[7][31]
[36] CCpqCCNqpq = D[7]DDD[2][7]D[33]D[17][35][33]
[37] CpCCpqq = DDD[35]D[7]D[30][31]DDD[2]DD[0]111D[0]D[0]D1D[0]D11DDD1[9]D[22][10][35]
+ [38] CCpqCCqrCpr = DDD1D[16]D[7]DD[24]D[15]DD[0]DDD1DD1111D[0]D1D11[25]1D[9]D[33][37][34]
+ [39] CCNpNqCqp = DD[11][25]DD[35]D[7]D[30][31]DD[36]D[5]D[6][21]D[30]D[35]DD[16]D[7]D[13][26][32]
[40] CCpCqrCqCpr = DD[38][38]D[38][37]
+ [41] CCpCqrCCpqCpr = D[40]DD[38][38]D[34]DD[40]D[27][36]D[40]DD[38][38][27]From further generation of w3's data based on [8a231d7] w3: reduced D-proofs for CCpCqrCCpqCpr,CCNpNqCqp,CCpqCCqrCpr,CCNppp like Generated data:
Other ResultsContinuing from w2's data of [a848c40] improvements via '--extract -l' script like Generated data:
|
Beta Was this translation helpful? Give feedback.
0 replies
-
w2: L2: 781↦535 CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
[2] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = DD[0]11
[3] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DD[2]11
[4] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[3]
[5] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][3]
[6] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[1][3]
[7] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][6]
[8] Cpp = DD[0][5][3]
[9] CCpCCqqrCCNrCCNstpCsr = D1[8]
[10] CpCqCrCsCtq = DDDDD1DD[0][1][3]1[3]11
[11] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[10]1
[12] CpCqp = DD[11][0]1
[13] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[6]D[7][3]
[14] CpCNpq = D[13]1
+ [15] CCNppp = DDDD[9]1DDD[0]DDD1DD[0][7][10][0]D[7]1DDD1DDD[0]D1DD1DD[4][0]11[3]DD[0][4][3]DDD1[11]1[3][3]11DDD1D[13]DD[0][2]DD[0]DDD1DDD1[5]111[3]1[9]D[5]DD1[12]1The proof was found by hand using metamath-exe. I kept temporary work variables undetermined during the proof process, to avoid excessive blowup of proof formulas. Any step that has an unknown formula and does not share its work variable with other unassigned steps can safely be unified directly to w2. Luckily, I kept the partial proof. It's not interesting to show here, but it allows me to provide the crucial step I revised: MM-PA> sh ne /unk 8 -1 min=? $? |- ( -. ph -> ( ( -. ( -. ph -> ph ) -> $616 ) -> ( -. ph -> ph ) ) ) 11 min=? $? |- $620 MM-PA> Originally, an unnecessary proof sequence was assigned to step 11. I assigned w2 to it, since we are allowed to choose any true statement we like. |
Beta Was this translation helpful? Give feedback.
3 replies
-
|
Nice! I never used metamath-exe this way. I updated this challenge and w2.txt accordingly. [c76302a] For the record, before I knew your approach, I tested your proof against the exhaustive database via with up to |
Beta Was this translation helpful? Give feedback.
-
Possibly yes, but I was also fortunate enough to find unknown steps that were readable. Most of them were still quite long and hard to process visually, so ideally the search for "safe to edit" work variables would be assisted with tooling. On another note, it seems that sometimes working things out by hand allows to find patterns that are noticeable to the human eye, but would take much longer with automated search (especially considering the difficulty level of w2). |
Beta Was this translation helpful? Give feedback.
-
You're right. I was curious and motivated by your result, so I just implemented a feature which covers these kinds of replacements, but moreover it attempts to use all intermediate steps encoded in a proof summary (from small to large), just in case any pair of formulas fits, given that it would reduce the fundamental length. This strategy turned out very successful.
Yes, to spot new patterns, definitely. Had I known there was so much possible improvement based on such a simple strategy, I would have had it implemented earlier. Thank you for pushing me in the right direction! |
Beta Was this translation helpful? Give feedback.
-
w1: (A2: 1927↦1925, A3: 363↦343) CCpCCNpqrCsCCNtCrtCpt = 1
[0] CCNpCCqrpCrp = DD1D1D111
[1] CCCCpCCNpqrstCst = D[0]D1D11
[2] CCCpqrCqr = D[0]D1D1D11
[3] CpCCNqCrqCrq = D1D[2]D[0]D11
[4] CpCCNqCCNrsqCrq = D1DDDD[2]111D1D1D11
+ [5] CpCqp = D[2][1]
+ [6] CpCNpq = DD[0][4]D[0][3]
[7] CCCCNNpCpNpqrCpr = D[0]D1D[1]D[1]DD[0]D11DD[0]D11[2]
[8] CCNpCqpCrCCNsCpsCqs = DD[0]DD[2]1DDD1DDD[1]1D1111D1DDD[1]1D111D[2]1
+ [9] Cpp = DD[4]1D[7][2]
+ [10] CCpqCCqrCpr = D[2]DD[0]D1[8][2]
[11] CCCCpqCrqsCCrps = D[0]DD[2]1DD[0]D1DDD[1]1D1D1D111[10]
[12] CCCCNpCqpprCqr = D[0]D1DD[0]D1D[1]D[1]1DD[0]D11D[0]DD[1]D[1]1D[7]D[0]DD[2]1[5]
+ [13] CCNppp = D[0]D[12]D[0][3]
+ [14] CCNpNqCqp = DDD1DD[0]D1D[2][8]D[0]DD[2]D[1]D[2]1D[7][2]1[4]
+ [15] CCpCqrCCpqCpr = DD[11]D[0]D1DD[0]D1D[1]D[1]1DD[0]DD[2]1DD[0]D1DDD[1]1D111[2]DD[0]D11D[0]DD[1]D[2]1D[7]D[0]DD[2]1[5]D[11]DDD[3]1DD[0]DDD1D111DD[0]D1DDDD[1]D[2]1D[1]D[2]DD[0]D11[6]1D1DDD[1]1D1D1D111D[2]D[2]DD[0][4]1D[12][2]DD[0]DDD1D111DD[0]DD[2]1D[0]D1DD[0]D1D[1]D[2]1DDDD[2]1D[0]DD[2]1DD[3]1DD[0][4]D[0]D1DDD[1]1D1111D11DD[0][4]1D[1]D[1]DD[0]D1DD[0]DD[1]1DD[0]D1DD[0]D1DDD[1]1D1111[2]1[2]w2: L2: 535↦417 CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
+ [1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
+ [3] CpCqp = DDD1D[2]1D111
+ [4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
+ [5] CCNppp = DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1w3: (A2: 614905↦254925, A3: 51239↦23321, L1: 39253↦16469, L2: 1649↦1331) CpCCNqCCNrsCptCCtqCrq = 1
[0] CCCpCCqrCsrtCCCqrCsrt = DD1D111
[1] CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw = D[0]D11
[2] CCCCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqpyCCyzCaz = DDD1DD1111D[0]D1D11
[3] CCCpCqrsCCqrs = DD1DDDD111[1]D111
[4] CCCpqrCqr = DDDDD[3]D111D[0]DD1111D11
[5] CCCNpqrCpr = DD11DDDDD111[1]D1D11[3]
[6] CCNppCqp = DD11D[5]D11
+ [7] CpCqp = DDDDD[3]D111DD[3]D11111
[8] CCCCNpqCrqpCsp = DD11DDD[3]DD[0]111DD[0]D[0]D1D11[0]
[9] CpCCpqCrq = DDD1D11DDD[0]D[0]D1D[0]D1D11[0][3]D11
[10] CCCNCNpqrsCps = DD11DDDDD111[1]D1D11DD11DDD[0]D[0]D1[0]DD1DD1111[3]
[11] CpCqCrp = D[4]D[3]DDDD111[1]D11
[12] CCCCCpqrCsrtCqt = DD[3]DD[0]D[3]1[6]1
+ [13] CpCNpq = D[5]D[1][6]
+ [14] Cpp = DD[5]DD11[9]1
[15] CNNCpqCrCpq = DD[8]D[2]D[8]DD11D[10]DDD11DDD[0]D[0]D1DDD1[0]1[0][3][3]DDDD111[1]D111
[16] CCNCCpCqpNrsCrs = D[1]DD1[7][15]
[17] CCpNpCqNp = DD11D[12]D[2]D[5]DD11D[16][9]
[18] CCpCqNpCrCqNp = DD11D[4]DD[1]DD11D[4]D[16][11]D[5]D11
[19] CCCpqrCNpr = DDDD11D[12]DD[3][2]D[5]DD[3]D11D[3]D[5]DD1[14][15]D[3][2]1
+ [20] CCNppp = D[16]DDDD11D[4]DDD1DD1[0]11DDD1[0]1DDDD111[1]D11DD[1]DD11D[4]D[5]D[16][11][6]1
[21] CCNpqCNCrpq = D[1]DD11D[4]DD[1]DD11D[16]D[4]DDD1[0]1DDDD111[1]D11D[4]D[5][18]
[22] CCpqCNCprq = D[1]DD11DDDD11D[12]DD[3][2]D[5]DD[3]D11D[5]DD1[7][15]DDD[3]D1DDDDD[3]D111D[0]D[0]D1[2]1D111DD[0][2][17]1
[23] CCNpqCNCrCspq = D[1]DD11D[4]DD[1]DD11DD[1]DD1[14][15]D[5]D11D[4]D[3]D[5][18]
[24] CCpqCCNppq = D[1]DD11D[19]DD11DD[8]DD[3][2]D[4]DD[1]DD11D[4]D[5]D[16][11][6]1
[25] CCNCpqrCCrqCpq = DD[24]DD1[6]DDD[0]D[0]D1[1]DD1[0]1[3]D[23]1
[26] CCpCpqCpq = DDDD11D[22][11]DD11D[22][11]1
[27] CCCCpqCrqsCps = DD[3]D1DDD1[0]1D[0]DDDD[3]D11111D[24]D[12][26]
+ [28] CCpqCCqrCpr = DDD1[22]DD[3]DDDD111[1]D11D[24]D[27][26][25]
+ [29] CCNpNqCqp = DD[1][17]DD[26]DD11D[21]D[22][11]DDDD11D[27][24]D[4]D[5][16]D[21]D[26]DD[1]DD11D[10][18][23]
[30] CCpCqrCqCpr = DD[28][28]D[28]D[27][26]
+ [31] CCpCqrCCpqCpr = D[30]DD[28][28]D[25]DD[30]D[19]DD11D[27][24]D[30]DD[28][28][19]w4: (A2: 16277↦13917, A3: 12959↦10779, L1: 14261↦12081, L2: 1889↦1709) CpCCNqCCNrsCtqCCrtCrq = 1
[0] CCpCqrCpCqp = DD111
[1] CpCCNqCCNrsCtqp = D[0]1
[2] CpCNCqrp = D[0]DD[0]D[1]11
[3] CCpCNqCCNrsCtqCpCCrtCrq = DD11D[2]1
[4] CCpqCpCCNrCCNstCurq = DD11D[2]D[1][1]
+ [5] CpCNpq = DDD11D[2][1]DD[0]D[1]11
+ [6] CpCqp = D[0]DDD11DDDD11D[2]D[0]D[1]1111
[7] CCpqCpCrq = DD11D[2]D[1][6]
[8] CCpNNqCpq = DD11DDD11D[2]D[4][1]DD[0]D[1]11
[9] CCpqCCrpCrq = D[3]D[7][1]
[10] CCpCqNqCpCqr = DD11D[2]D[1]DD11D[3]DD[0][0]DDD11D[2]D[4][1]DD[0]D[1]11
+ [11] Cpp = DDDDD[3]DD11D[2]D[1]D[4][6]D[7]DDD11D[2]D[1]DD11DDD11D[2]D[1]DD11D[2]D[1]DDD11D[2][1]DD[0]D1111D[0]D[2]1111
+ [12] CCNppp = D[8]DDD11DDD[3][4]D[2]D[7]D[10][6]DDD[3][4]D[10]DDDD11D[4]D[3]DDD11D[2]D[1]DD11D[2][5][2][0]1DDDD11D[4]D[3]DDD11D[2]D[1]DD11D[2][5]D[0]D[2]1[0]1DD[3][4]D[10]DDD11D[2]D[1][8][6]
[13] CpCCpqq = DDD[9][12][7]DDD[3][4]D[2]D[10][6]DDD[9][12]DD11D[2]D[1][5]DDD11D[2]D[1][7]DDD11D[4]DDD11D[2]D[1][5][6][11]
+ [14] CCNpNqCqp = DD[9]D[13][11]D[3]D[9][13]
+ [15] CCpqCCqrCpr = DDDD[9]D[13][11]D[3][4]DD[9][13]DDD11DDD11D[2]D[1]DDD11D[2]D[4][6]DD[0]D[1]11D[7]D[10][6][11]DDD11D[2]D[1][7][9]
+ [16] CCpCqrCCpqCpr = D[3]D[7]D[15][12]w5: L2: 107↦103 CCpqCCCrCstCqCNsNpCps = 1
+ [0] CCpqCCqrCpr = DD11D1DD11D1D11
[1] CCCpCqrCCCsqtCNqNsCsq = DDD11DD1D11D1DD1D11DD11D1DD11D1DD1D1DD11D11D1D111
+ [2] CpCNpq = D[1]1
+ [3] Cpp = D[1][0]
+ [4] CpCqp = DDD11DDD11DDD11D11D1DDD11DD11D1DD11D1DD1D1DD11D11DD11D1DD11D1DD1D1DD11D11D1D111D111
+ [5] CCNpNqCqp = DD1DD11DD1D1DD1D1D1D11D1D11D1DD1D11D1D11D1D1[2]
+ [6] CCNppp = DD1[0]DD11D1DD11D1DD1DD11D1D1DD11D1DD11D1DD1D1DD11DD1D1DD1D1D1D11D1D11D1DD1D11D1D11D11D1D11
+ [7] CCpCqrCCpqCpr = DDD11D1D11DD1DD11D1DDD11D1[1]DD11D1DD1D1DD11D1DD11D1DD1D11D11D1D11D1DD11D1D1DD11D1DD11D1DD1D11D1[0] Essentially, all smaller subproofs encoded in a proof summary (from small to large) have been attempted as alternatives for each argument of each rule. Only for m and w6, this resulted in no improvements. Full output log file: z-improvements.log. Inspired by this solution. ✻Except that index evaluation sequences were not rebuilt. This affected only |
Beta Was this translation helpful? Give feedback.
0 replies
-
w2: A3: ω↦3301 CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
+ [1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
+ [3] CpCqp = DDD1D[2]1D111
+ [4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
+ [5] CCNppp = DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1
[6] CpCCNqqq = D[3][5]
+ [7] CCNpNqCqp = DDD1[6]DDD1DDD1DDD1[6]DDD1[5]1[6][6][1]11[6][6]Overall, what I did was similar to @GinoGiotto’s save, but more obscure. Before using pmGenerator, I had managed to prove mpi, com12, and jarr. The only heuristic at this point was removing unnecesary antecedents or seeing that something was redundant; otherwise I was applying things relatively blind. jarr felt like a particularly lucky and novel ability, as it had come from what was w2.txt[6]. luk2 was also relatively novel, leading to the command: I filled in steps 1 and 14–17, and either on a calculated guess or complete misunderstanding of the proof, filled in id for the longer of the two remaining goals. (Note the similarity to GinoGiotto’s metamath.exe strategy; the long parts were filled in). I was then left with: Metamath proofs (includes w2jarr, etc)
w2: A3: 3301↦1877 CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
+ [1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
+ [3] CpCqp = DDD1D[2]1D111
+ [4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
[5] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq = DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1
+ [6] CCNppp = DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11[5]
+ [7] CCNpNqCqp = DDD1D[3][6]DDD1DDD1DDD1D[3][6]DDD1[6]1[5][5][1]11[5][5](from automatic compression of manual proof) |
Beta Was this translation helpful? Give feedback.
1 reply
-
|
Thank you for this impressive contribution! I updated the challenge proofs and hall of fame accordingly. |
Beta Was this translation helpful? Give feedback.
-
w2: (A2: ω↦898348491, A3: 1877↦1841, L1: ω↦448601069, L2: 417↦405) CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] CCCpCCqCprCCNrCCNstqCsruCvu = DDD11D11[0]
[2] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = DDD1D111[0]
[3] CpCCCNCqCCrCqsCCNsCCNturCtsvNpw = DDD1[0]D111
[4] CpCCNqCCNrsCNqCCNCtpuNCvCCwCvxCCNxCCNyzwCyxCrq = DDDDD11111[0]
+ [5] Cpp = DDD11[1][0]
[6] CCpCCqqrCCNrCCNstpCsr = D1[5]
[7] CCpCCNqCCNrCCNstqCsruCCNuCCNvwpCvu = D1DDD1[3]1[0]
[8] CCCNpqCrCCsCCtCsuCCNuCCNvwtCvuxCCNCpCyxCCNzaCCNCbCCcCbdCCNdCCNefcCedgCNxCCNyhrCzCpCyx = DDD1DDD11DD1D111[0]1[0]
[9] CpCqCrCNps = DDD11D11DDDDD1[2]1[0]11
[10] CpCqCrr = DDD11DDD1DDD1[1]111[0]1
[11] CpCqCCrCpsCCNsCCNturCts = DDD11DDD11DDDD111[0]1[0][0]
[12] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = DDD1[0]D11DDD11DDD1DDD1DD1D111111[0]1
+ [13] CpCqp = DDD1DDD[8]111D111
+ [14] CpCNpq = DD[2]DDD11[2][0]1
[15] CpCqCrp = DDD11DD11[2]DD[8]11
[16] CCNpCCNqrNsCsCqp = DDD11DDD11D[6]1[0][0]
[17] CpCqCrCsCtp = DDD11DDD1DDD1DDDDDD1[2]1[0]111111[0][4]
[18] CNCpqCrCsCqt = DDD11DDD1DD[7]1[0]1[0][4]
[19] CCNCNpqCCNrspCrCNpq = DD11DDD1[15]D11DDD11[2]1
[20] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq = DD[2]DDD11[2][0]DDD11DDD1111[10]
[21] CCNCpCqCrsCCNtuCCNqvNCwCxNsCtCpCqCrs = DD1DDD11DDDDD111[0]DD1[3]1[0]1DDD1D1DDD[8]1111[0]
[22] CCNCpCqrrCpCqr = DDD11DDDD1[0]DDD11DD1[2]1[0][0][11][4]
[23] CNCpNqCrq = DDD1DDD11[9][0]DDD11D[6]1[0][4]
[24] CNNpCqp = DDD11DD1[13]DDD1[3]1[0][12]
[25] CCNpCCNNqrqCNqp = DDDD1DDD11[1]DDD1[0]DDD1[9]1111[13]1
[26] CNNpCqCrCsp = DDD1DDD11DDDDD111[0]DD1[3]1[0]1DDD1D1[13]1[0][4]
[27] CNCpqp = DDDD11DDD11DD11[9][0][18]1
[28] CCCNpqrCpCNrs = DDDDDDDD1DDD1D1[0]1[0]1[0]1[0]DDDD1[0][8][0]DDD1[15]D11DDD11[2]111
[29] CpNNp = DDDDDDDD1[2]1[0]1[18]11[24]
+ [30] CCNppp = DDDD[6]1DD[19]D[21][0]11[20]
[31] CpCCNqqq = D[13][30]
[32] CCNCCpqqCCNrspCrCCpqq = DD1DDD1[1]11DDD1[30]1[31]
[33] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = DD1[31]DDD1[30]1[31]
[34] CpCCNCNqqCNqqq = D[33]DDDD11DDD11[9][0]DDDDDD1D1DDD[8]1111[0]DDD1DDD11[2]1[2]1[11]11
[35] CCNpCqpCqp = DDD11[13]D[33]DD[19]D[21][4]1
[36] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = DD1[31]DDD1[30]1[20]
[37] CpCCNqNpq = DDD1D[36][20][5]1
+ [38] CCNpNqCqp = DDD1[31]DDD1[37]1[20][20]
[39] CpCCNqNpq = DDD1D[33][31][5]1
[40] CpCCNqNNqq = D[13]DDD11[24]D[33][31]
[41] CCpCCqqrCpr = DDDD1[31]D1[31]D[15][6]DDD1[31]D1[31]D[15][6]
[42] CCNCCpqqpCCpqq = D[32]D[33][31]
[43] CCpCqCprCqCpr = D[42]DDDD11DDD11[9][0][18]1
[44] CCCpqCrpCrp = D[42]DDD1DDD11DDD111[0][0]DDD[7]1[0]DDD11[2][0][12]
[45] CpCCNqqCCqrr = D[24]D[29]D[32][34]
[46] CpCCNNCNNqrqq = D[13]D[35]D[32]DDDDD11DDDDD111[0]DD11DDD1[3]1[0][0][15]1[23]
[47] CpCCpqq = D[32][40]
[48] CNCpCNqrCqs = DDDD[7]1[0][13]DD[2]DDD11[2][0]DDD1[0]DDD1111[10]
[49] CCpCqCrNpCqCrNp = D[42]D[25][17]
[50] CCCpqCrCspCrCsp = D[42]DDDDD1[11]DDD1[7]1[0][4]DDD11DDD11DDD11DDD1[2]1[0][0]DDD11[2]1[12]1
[51] CCCpqCrCqsCrCqs = D[42]D[25]DDD11DDDD1[0]DDD1[2]1[0][0]DDD1DD[7]1[0]1[0][4]
[52] CNNpCCNCpqCpqq = D[33]D[13]DDD11[24][34]
[53] CCNpCqCrpCqCrp = D[42]D[25]DDD[7]DDD1DDD1[6]1[0]1[0][4][26]
[54] CpCCNNpqq = D[32]D[13]DDD11DDD11[6][0][52]
[55] CCpCNNpqCNNpq = D[35]D[32][46]
[56] CCpCNCpqrCNCpqr = D[42]D[44]DDD11[1]DDD1[0]DDD1[9]111
[57] CCCCpqqCprCpr = D[43]D[32][45]
[58] CpCCNNCqrqq = D[13]D[44][54]
[59] CCpqCpCrq = DDD11DDD[8]111D[33][58]
[60] CpCCqNpCqr = D[16]D[33][58]
[61] CpCCNNCqprr = DDDD1DDD1[1]11DDD1[39]1[39]D[13]D[41]DDD1[15]DDD1[39]1[39][40]D[35]D[19][45]
[62] CCpqCrCpCsq = D[59][59]
[63] CCpCqNpCqNp = D[35]D[32]DDDD11[15]D[33]DD[19]D[21][4]1[61]
[64] CCpCCNppqCCNppq = D[42]DDDD[6]1DD[19]D[21][4]1DD[6]1DD[19]D[21][4]1D[13]D[44][61]
[65] CCNNpCqCprCqCpr = D[42]D[63]DD[42][48]DDD11[9][12]
[66] CCNpCCpqqCCpqq = D[42]D[63]D[57]DDD11[9][0]
[67] CpCqCCprCsr = D[59]D[57][62]
[68] CCCpqrCqr = D[43]DD[42]D[25][18][67]
[69] CCCNpqrCpNNr = D[68]DDDD1DDD1[26]D111111
[70] CCpqCNNpq = D[43]D[55][67]
[71] CCpqCNCprq = D[43]D[56][67]
[72] CCCCpqqrCpr = D[43]D[57][67]
[73] CCNpCNCqprCNCqpr = DD[47]D[32]D[13]D[63][61][43]
[74] CCpNqCpCqr = D[53]D[71][60]
[75] CpCCNNpqCrq = DD[42]D[63]DDDD11[9]DDD1[10]DDD1DD[7]1[0]1[0][4]1[67]
[76] CCNCpNpCpqCpq = D[66]D[59]D[43]D[38]D[56]D[55]DDD11DDD[8]111D[33][23]
[77] CCpqCCNppq = D[43]D[64][67]
[78] CNCCNpqpq = DD[19]D[33][31]D[59]D[38]D[69]D[64]D[59]D[43]D[56][62]
[79] CCCCpqNpCrqCrq = D[66]D[59]D[59]DD[19]D[33][31]D[49]D[28]D[64]D[59]D[43]D[56][62]
[80] CpCCpNqCqr = D[53]D[71]D[16]D[71][77]
[81] CCCCNpqpCrqCrq = D[66]D[59]D[59][78]
[82] CCNNCCNpqpqq = D[66]D[59]D[70][78]
[83] CCpNqCqCpr = D[53]D[71][80]
[84] CNCCNpqCrpq = D[81]D[28]D[64][62]
[85] CCCCpNNqqCprCpr = D[65]DD[43]D[55]D[57]D[59][67]DD[68][32]D[66]D[59]D[70]D[53][60]
[86] CCNCpNNqqCpNNq = D[22]D[69][82]
[87] CNCCCpqrpCsr = D[59]D[79]D[74]D[86]D[71]D[50][60]
[88] CNCCpqCprq = D[79]D[74]D[86]D[71][74]
[89] CCpqCpCCqrr = D[22]DD[68][32]D[66]D[59]D[70][88]
[90] CNCpCCpqrq = D[79]D[74]D[86]D[71][83]
[91] CCNpqCCqpp = D[53]D[72][89]
[92] CNCCpqCprNNq = D[86]D[71][88]
[93] CCpqCpNNq = D[22][92]
[94] CCpqCpCNqr = D[22]D[74][92]
[95] CCpCCNqpqCCNqpq = DD[53]DD[51]D[57][67][89]DD[47]DDDDDDDD1[2]1[0]1[18]11DDDDDDD11DDD1DDD1[6]1[0]1[0][4]DD1[20][6]11D[13]DDD[7]DDDD1[0]DDD11DD111[0][0]DDD1D1DDD1[0]DDD1[1]1111[0][4][27][81]
[96] CNCpNCpqNNq = D[86]D[71]D[79]D[74]D[86]D[71]D[49][80]
[97] CpCCpqCNqr = D[72][94]
[98] CCNpqCNqp = D[53][97]
[99] CCpNNqCNNNNpq = D[53]DDD[53]D[56]D[59][39]D[79]D[19][45]D[59]D[53]DD[43]D[71]DD[42][48][67]D[77]D[38][92]
[100] CCpCCqpNpNNNp = DD[49]D[70][80]DD[66]D[59]D[70]D[43]D[38]D[56]D[59]DD[32]DDDD11[17]DDD1[15]DDD11DD1DDD1[0]D11DDD11[2]11[0][4]1DDDDD11DDD11D1DDD11DDD11DD11[9][0][12][4][11]1DDD[7]DDD1DD[6]1[0]1[0][4]DDDDDD11DDD1DDD1[6]1[0]1[0][4]D[7]DDDD1[0]DDD11DD111[0][0]DDD11DD11[13][4]11D[38][96]
[101] CpCCpqCNCrqs = D[72]D[53]DD[64]D[59][71]DD[59][98]D[59][88]
[102] CCCpqrCNNNrp = D[50]D[53]DD[43]D[71]DD[42][48][67]D[77]D[38]D[93][90]
[103] CpCCpqCCNNqrr = DD[65]DD[43]D[55]D[57]D[59][67]DD[68][32]D[77][93]D[59][89]
[104] CCNNCNpNNNNNCCNNqqprCNrs = DDD[43][75][97]DD[47]D[55]DDD11D1DDD11DDD11DD1[13]DDD1[3]1[0][4][4][4]D[49]D[70][97]
[105] CCCNpqrCpNCrNr = D[16]D[70]DD[95]D[59]D[47]DDD[6]DD11DD[6]1[0][12]D[35][52]DDDD[68][32]DDDD1[31]D1[15][40]DDD11[15]D[33][31]D[13]D[98]DD[22]D[59]D[38]D[69]D[77][80][96][89]
[106] CNNCpNqCCCqNprr = DD[99]D[93][89]D[100]DD[28]D[64]D[59][70]D[49][80]
[107] CNNCNpqCCqNCrrp = D[70]D[43]DD[43]DD[95]D[59]DDD11DDD11D[3][5][0]D[33][58]DD[43]D[98]D[59][84]D[98][84]DD[99]D[93][89]D[100]D[14][84]
[108] CCNCCpCCpqCrqsss = DD[107]DD[93]D[49][97]D[22]D[79]D[94][89]D[104]DDDD11[15][45]D[57][62]
[109] CCNCpqrCCrqCpq = D[53]DDDDD[107]DD[69]D[64][62]D[79]D[74]D[86]D[71]D[50][60]DDDD[99]D[93][89]DDD[49]D[70]D[53]DD[64]D[59][71]DD[59]D[43]DD[43]D[76]D[59]D[38]D[69][82]D[38]D[69]D[64]D[59][67]D[38]D[93][90]D[83]D[93]D[66][87]DD[59]D[47][27]D[16][52]DD[49][97]DD[53]D[56]D[59][39]DDDD1[31][6]D[13]D[41]D[53][39]D[13][84]DD[43]D[55][62]D[57][62]D[107]DD[69]D[64]D[59][70]DD[43]DD[65]DD[47]D[55][67][89][67][95]DD[70]D[22]DD[70]D[53]DDDDDD[53]D[56]D[59][39]D[105]D[91]D[69]D[64][67]D[72][89]DD[49]DD[64]D[59][71]DD[59][68][97]DD[107]DD[93]D[49][97][94]D[104]DD[59][43]DD[51]DD[43]D[32]D[32]D[22]DDDD1[13]DDD1[3]1[0]DDDDD1[11]DDD1D1[13]1[0][4]DDD11DDD11[9]DDD1DDD11[2]1[2]1[4]11[67]D[102]D[91]D[98]D[81]D[94]D[22]D[59]D[38]D[69]D[77][60]D[13]DDDD[107]DD[93]D[49][97][91]D[104]DD[59][63]D[28]D[59]D[66]D[22]DD[6][38][46]D[71][101]DD[53]D[71][97]DDDD[50][103]DDD[50]DD[43][75]D[85]D[59][89]DD[70]D[39]DDD1DDD1[0]DDD1[1]111DDD11D[6]1[0][4]DD[93]D[53]DD[43][75][97]D[102]D[91]D[98]D[79]D[94]D[49]D[70][97]DD[50][101]D[91]D[49]D[72]D[53]D[71][94]D[70]D[59]D[55][62]D[98]DDD[53]D[73]D[59]D[72][89]D[38]D[93][90]D[94][94]D[43]D[98]DD[99]D[93][89]D[100]D[14][84]DD[93]D[51]D[85]D[59]D[22]D[59]D[59][88]DDDDDD[43][75][103]DDD[53]DD[64]D[59][71]DD[59][98]D[81]D[74]D[86]D[71][74]DD[43]D[98]DD[49]DD[66]D[59]D[70]D[38]D[71]D[76]D[49]D[28]D[66]D[59]D[55]D[59]D[42]DD[19][18]1DD[22]D[59]D[38]D[69]D[77][80][92]D[59]D[79]D[28]D[64][62]D[83]D[63]DD[68][32]D[77]DDD1[39]DDD1[39]1[39]D[13]D[64]D[59]D[43]D[55][62]DD[49]DDD1[31][6][45]D[14]D[43]DD[43][75]D[22]D[59]D[38]D[69]D[77]D[72][83]D[13]D[108]DD[22]D[59]D[81]D[74]D[86]D[71][74]D[102]DD[68][32]D[66]D[59]D[70]D[66]D[59][78]D[70]D[108]DD[43]DD[70]D[43]DD[43]D[98]DD[22]DD[22]DD[68]DDD[6]1DD[19]D[21][4]1DD[6]1DD[19]D[21][4]1[82]D[71][88][84]D[73]D[73]DD[43]DD[43]DD[42][48][67][75]D[59]D[70]D[43]D[56][62]DD[93]D[53]D[38]D[81]D[94][89]D[98]D[102]D[91]D[98]D[81]D[94]D[22]D[59]D[59][88]DD[107]DD[86]D[71]D[49][80]D[86]D[71][71]D[104]D[62]D[32]D[13]D[66]D[59]D[55]D[59]DD[32]DDD11[18]DD[2]DDD11[2][0]DDD1[0]DDD1111[10]DDDDDDD1D[21][4]D111[27]111D[106]D[29]D[69]D[77][80]DD[86]D[56]D[59][68]DD[99]D[93]D[49]D[98]D[59][88]DDD[106]D[29]D[63]D[28]D[66]D[70]D[59]D[35]D[32][45]D[49]D[98]D[79]D[94][94]DDDD[98][87]DD[47]DD[19]D[22]DDDD11DD[6]DDD1[0]DDD11DD111[0][0][4]DDD1DDD11DDD111DDD1DDD11[2]1[2]1[0]DD[6]1[0][4]11D[54]D[63]D[19]D[13]DDD[6]DD11DD[6]1[0][12]D[63]D[32][34]DD[53]DD[43][75]D[72][89]DD[43]DD[70]D[43]D[70]D[55][67]D[29]DD[42]D[25][18][67]D[77]D[49]D[98]D[59][90]DD[22]DDD1[39]DDD1[39]1[39][58]D[105]D[66]D[59]D[70][90][67]
+ [110] CCpqCCqrCpr = D[43]DDD[109][88][62]DD[109]D[56][62]D[109][88]
+ [111] CCpCqrCCpqCpr = DD[110]D[43]DDD[109][88][62]DD[43]DD[65]DD[47]D[55][67][89][67]D[109][88]D[109][88](Preliminary result, before using proof compression via Generated with Prover9 (version 2017-11A (CIIRC)) and further reducements via For Prover9, I used this input file (hints generated with |
Beta Was this translation helpful? Give feedback.
3 replies
-
w2: (A2: 898348491↦2602085, A3: 1841↦1153, L1: 448601069↦1228561) CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = DDD1D111[0]
+ [2] Cpp = DDD11DDD11D11[0][0]
[3] CpCqCrCsp = DDDDDD1DDD11DD1D111[0]1[0]111
[4] CpCqCrCNps = DDD11D11DDDDD1[1]1[0]11
[5] CCCNpqrCCNCpsCCNtuNrCtCps = DDD1DDD1DDD1[0]D1111[0]1[0]
[6] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = DDD1[0]D11DDD11DDD1DDD1DD1D111111[0]1
+ [7] CpCqp = DDD1[3]D111
+ [8] CpCNpq = DD[1]DDD11[1][0]1
[9] CpCqCrp = DDD11DD11[1]DDDDD1DDD11DD1D111[0]1[0]11
[10] CpCqCrCsCtp = DDD11DDD1DDD1DDDDDD1[1]1[0]111111[0][0]
[11] CpCNCqCNprs = DDD11DDD11D11[0]DDD1[0]DDD1[4]111
[12] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq = DD[1]DDD11[1][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1
[13] CCNCpCqrrCpCqr = DDD11DDDD1[0]DDD11DD1[1]1[0][0]DDD11DDD11DDDD111[0]1[0][0][0]
[14] CNCpCqNrCsCtCur = DDD1DDD11DDDDD111[0]DD1DDD1[0]D1111[0]1DDD1D1[3]1[0][0]
[15] CNNpCqCrCsp = DDD1DDD11DDDDD111[0]DD1DDD1[0]D1111[0]1DDD1D1[7]1[0][0]
[16] CCNpCCNNqrqCNqp = DDDD1[11]1[7]1
[17] CNCpCqrCsNr = DDDD11DDD1[9]D11DDD11[1]1[14]1
+ [18] CCNppp = DDDDD1[2]1[17]1[12]
[19] CCNCCpqqCCNrspCrCCpqq = DD1[0]DDD1[18]1[12]
[20] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = DD1[12]DDD1[18]1[12]
[21] CCCpqrCqr = DDDD1[12]D1[2][12]DDDDDD1DDD1D1[0]1[0]1[0]1[0]D[20][12]
+ [22] CCNpNqCqp = DDD1[12]DDD1DDD1D[20][12][2]11[12][12]
[23] CCNCCpqqpCCpqq = D[19]D[20][12]
[24] CCNppCCpqq = D[19]D[20]DDDD11DDD11DD11[4][0][14]1
[25] CCpCqCprCqCpr = D[23]DDDD11DDD11[4][0]DDD11DDD1[5]1[0][0]1
[26] CCCpqCrpCrp = D[23]DDD1DDD11DDD111[0][0]D[5]DDD11[1][0][6]
[27] CCpCqCrNpCqCrNp = D[23]D[16][10]
[28] CCNpCqCrpCqCrp = D[23]D[16]DDDD1[0]DDD1[1]1[0][0][15]
[29] CCpCNCpqrCNCpqr = D[23]D[26][11]
[30] CCpCNNpqCNNpq = DDDD11[7]D[20][17]D[19]DDDD11[9]D[20][17]D[19]DDDDD11DDDDD111[0]DD11DDD1DDD1[0]D1111[0][0][9]1DDD1DDD11[4][0]DDD11DD1[2]1[0][0]
[31] CNCpqCCNCprCprr = D[20]D[7]D[26]D[19]DDDD11DDD11DD1[2]1[0][0]D[20]D[7]DDD11DDD11DD1[7]DDD1DDD1[0]D1111[0][6]D[20]DDDD11DDD11DD11[4][0][14]1
[32] CCpqCpCrq = DDD11[3][31]
[33] CCpqCpCrCsq = DDD11[10][31]
[34] CCNpCCpqqCCpqq = D[23]DD[27]D[19][12]DDD11DDD11[4][0]D[7][24]
[35] CpCqCCprCsr = D[32]D[25][33]
[36] CCpNqCpCqr = D[28]DD[25]D[29][35]DDDD11DDD11DD1[2]1[0][0][31]
[37] CNCCpqCprq = DD[34]D[33]DDDD11DDD1[9]D11DDD11[1]1D[20][12]D[27]DDDD11[4][31]D[25]D[29]D[32][32]DDDD11[4][31][36]
[38] CCpqCpCCqrr = D[13]DD[21][19]D[34]D[30]D[33][37]
[39] CCNCpqrCCrqCpq = D[28]DDDDD[34]D[32]D[30]D[32][32]D[32]D[28]D[28]DD[25]D[29][35]DDD11[4][31]D[25][33]DDD[25]D[30][35]D[13]D[38]D[22]DD[21]DD11DDD1[15]D111DD[25]DD[25][24][35]DD[25]DD[25]D[19]D[7][24][35][36]DDD[27]D[16]D[32][37]D[27]D[16]D[33][37]D[16]D[32]DD[25]D[19]D[7]DD[27]D[19][12]DDDD1[0]DDD1DDD1D[20][12][2]11[12][12]D[16]DDD11[9]D[7][24]D[29]D[32]D[25]D[29][35][35]
+ [40] CCpqCCqrCpr = D[25]DDD[39][37]D[32][32]DD[39]D[29]D[32][32]D[39][37]
+ [41] CCpCqrCCpqCpr = DD[40]D[25]DDD[39][37]D[32][32]DD[25]DDD[23]DD[27]D[19][12]DD[23]DD[5][7][12]DDD11[4][6]D[38]D[30][35][35]D[39][37]D[39][37]Obtained from compressing the previous results via Input, output and log files:
|
Beta Was this translation helpful? Give feedback.
-
|
Is the proof of [32] improvable by my manual proof of a1dt: https://github.com/icecream17/Stuff/blob/main/math/~w2.mm#L445-L446 ? or just Edit: for this particular step I verified it saved 476 steps (noncompressed)In generated 4545-length proof Editing |
Beta Was this translation helpful? Give feedback.
-
|
Yes, generating the compact overview (like stated in w2.txt) via then replacing with and comparing outputs of reveals it is a w2: (A2: 2602085↦2524021, L1: 1228561↦1190957) improvement. I will add that referring to your reply. :-)
Correct, I didn't unfold it but used Edit: This leads to w2: (A2: 2602085↦1264633, L1: 1228561↦588991) with proof compression. the compressing command printed Amazing. I love that feature. |
Beta Was this translation helpful? Give feedback.
-
|
I basically collected all known-to-be-useful connections within syntactic D-rule consequences that I had obtained from any C-N system and tried to implement them in each of the target systems, gradually obtaining and utilizing more useful connections via proof compression. More specifically, improvements given below were obtained by
Initial proof summaries, data generated in the process, used scripts and detailed instructions are contained in the following archive.
✻Most of these computations were performed with computing resources granted by RWTH Aachen University under project rwth1392. m: (A2: 7001↦5401, L1: 619↦459) CCCCCpqCNrNsrtCCtpCsp = 1
[0] CCCppqCrq = D1D1D11
+ [1] CpCqp = DDD11[0]1
[2] CCCpqrCqr = D1D1D[0][0]
+ [3] Cpp = DDD[0][0]11
+ [4] CpCNpq = DD1[2][2]
[5] CpCNNCCqCNNrrss = DD11DDDD1D1DD1DD11[0]111D1DD1DD1D1D[0]1[1]D11
[6] CCCpNCCCqrCNNqrNstCst = D1D1D[0]D1DD11DDDD1D1DD1DD11[0]111D1DD1D1D[1]D1D111
[7] CCpCpqCrCpq = DDD1D1D1D[0][6]11
+ [8] CCNppp = DD[7]DDD1D1DD1D1D[1]D1D11D[2]D[2]1111
+ [9] CCNpNqCqp = DDDDD1D1DD[2]1D[2]D[6]D1D1111DD1D1DD1D1D[2]1D11[1]1
[10] CCpqCCCrCNNssNNpq = DDD1D1DD1DD1D[0]D1[2]111DDDD1D1DD1D1D1D[0]D1DD11DDDD1D1DD1DD1DD1DD11[0]D1DD1D1DD1D111D1[0]1111[0]DD1D11D[2]111D[5]1
+ [11] CCpqCCqrCpr = DD1D[10][10]1
[12] CCpqCCrpCrq = DD[11]DD1DD1D1D1DD1DD1DDD1D1D[2]1D111D1D1D[0]D1[5]DD1D11D111DD[7][7]1D[11][11]
+ [13] CCpCqrCCpqCpr = DD[12]D[11][11]DD[11][11]D[12]DD[7][7]1w1: A2: 1925↦1763 CCpCCNpqrCsCCNtCrtCpt = 1
[0] CCNpCCqrpCrp = DD1D1D111
[1] CCCCpCCNpqrstCst = D[0]D1D11
[2] CCCpqrCqr = D[0]D1D1D11
[3] CpCCNqCCNrsqCrq = D1DDDD[2]111D1D1D11
+ [4] CpCqp = D[2][1]
[5] CCpqCpq = D[0]D1D[2]D[0]D11
+ [6] CpCNpq = DD[0][3][5]
[7] CCCCNNpCpNpqrCpr = D[0]D1D[1]D[1]DD[0]D11DD[0]D11[2]
[8] CCNpCqpCrCCNsCpsCqs = DD[0]DD[2]1DDD1DDD[1]1D1111D1DDD[1]1D111D[2]1
+ [9] Cpp = DD[3]1D[7][2]
+ [10] CCpqCCqrCpr = D[2]DD[0]D1[8][2]
[11] CCCCNpCqpprCqr = D[0]D1DD[0]D1D[1]D[1]1DD[0]D11D[0]DD[1]D[1]1D[7]D[0]DD[2]1[4]
+ [12] CCNppp = D[0]D[11][5]
+ [13] CCNpNqCqp = DDD1DD[0]D1D[2][8]D[0]DD[2]D[1]D[2]1D[7][2]1[3]
+ [14] CCpCqrCCpqCpr = DDD[0]D1D[2][8]D[0]D1D[11]D[2]D[1]D[2]DD[0]D11D[0]DD[1]D[2]1D1D1D11DD[0]DD[2]1DD[0]D1DDD[1]1D1D1D111[10]DDDD1D[2]DD[0]D1[8]D[0]DD[2]D[1]D[2]1[6]1DD[0]D1D[1]D[1]1DD[0]D11DD[0]D1D[0]DD[2]D[1]D[1]1D[2][4][5]DD[0]DDD1D111DD[0]DD[2]1D[0]D1DD[0]D1D[1]D[2]1DDDD[2]1D[0]DD[2]1DDD1D[2]D[0]D111DD[0][3]D[0]D1DDD[1]1D1111D11DD[0][3]1D[1]D[1]DD[0]D1DD[0]DD[1]1DD[0]D1DD[0]D1DDD[1]1D1111[2]1[2]w2: (A2: 1264633↦27599, A3: 1153↦1007, L1: 588991↦11703, L2: 405↦367) CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = DDD1D111[0]
+ [2] Cpp = DDD11DDD11D11[0][0]
[3] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1DDDDDD1DDD11DD1D111[0]1[0]111
[4] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = DDD1[0]D11DDD11DDD1DDD1DD1D111111[0]1
+ [5] CpCqp = DD[3]D111
+ [6] CpCNpq = DD[1]DDD11[1][0]1
[7] CpCCNqCCNCrCNpstNCuCCvCuwCCNwCCNxyvCxwq = DD[1]DDD11[1][0]DDDD11D1[0][0]DDDD11111
[8] CpCCNqCCNrsCpqCrq = DDD11DD1[2]1[4]
[9] CCpCCqCCNrCCNCsCNqtuNCvCwCCxCwyCCNyCCNzaxCzyrbCCNbCCNcdpCcb = D1DD[1]DDD11[1][0]DDD11DDD1[0]DDD1DDD11111[0]11
[10] CNCpCqNrCsCtCur = DDD1DDD11DDDDD111[0]DD1DDD1[0]D1111[0]1DDD1[3]1[0][0]
+ [11] CCNppp = DDDDD1[2]1DDDD11DDD11D11DDD1DDDDD1DDD11DD1D111[0]1[0]11DDD1DD11[1]111[10]11[7]
[12] CCNCCpqCrqCCNstCNqCCNrupCsCCpqCrq = D[9]DDD1DDD1DD[9][8][7]1[7]1[7]
[13] CCNCCpqqpCCpqq = DD[9][8]DD[9]DDD1[11]1[7][7]
+ [14] CCNpNqCqp = DD[9]DDD1DDD1DD[9]DDD1[11]1[7][7][2]11[7][7]
[15] CCpCqCprCqCpr = D[13]DDDD11DDD11DDD11D11DDDDD1[1]1[0]11[0]DDD11DDD1DDD1DDD1DDD1[0]D1111[0]1[0]1[0][0]1
[16] CCpqCCNppq = DD[12][7]DD[9]DDD1[11]1[7]DDDD11DDD11DD11DDD11D11DDDDD1[1]1[0]11[0][10]1
[17] CCpCqrCCqpCqr = DD[12][7]DD[9]DDD1[11]1[7]D[5]DD[13]DDD1DDD11DDD111[0][0]DDDD1DDD1DDD1[0]D1111[0]1[0]DDD11[1][0][4]DD[9][8]D[5]DDD[9]D1[2][7]D[13]DDDD1[0]D11DDDD11DDD1[1]1[0][0]D[3]DDD1DDD1[0]D1111[0]1
[18] CCpCqrCpCqCsr = D[17]DDD11DDDDD111[0]DD[9]DDD1[8]1[7][7][0][0]
+ [19] CCpqCCqrCpr = D[15]D[18]DDD[12][0]D[16]DD[9]DDD1[8]1[7][4][17]
+ [20] CCpCqrCCpqCpr = DD[19]D[15]D[18]DDD[12][0]D[16]D[12][4][17][17]The main method (described at the top) includes files with search results from a w2-extraction Generated Data
Extraction ProcedureThese proof files were first extracted from exhaustive files up to w3: (A2: 254925↦14557, A3: 23321↦4821, L1: 16469↦3227, L2: 1331↦1283) CpCCNqCCNrsCptCCtqCrq = 1
[0] CCCpCCqrCsrtCCCqrCsrt = DD1D111
[1] CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw = D[0]D11
[2] CCCpCqrsCCqrs = DD1DDDD111[1]D111
[3] CCpqCrCpq = D[2]DDDD111[1]D11
[4] CCpqCCCpqrCsr = D[2]DDD1DD1111D[0]D1D11
[5] CCCpqrCqr = DDDDD[2]D111D[0]DD1111D11
[6] CCCNpqrCpr = DD11DDDDD111[1]D1D11[2]
[7] CCNppCqp = DD11D[6]D11
+ [8] CpCqp = DDDDD[2]D111DD[2]D11111
[9] CpCqCrCCpsCts = DDD[2]DD[0]111DD[0]D[0]D1D11[0]
[10] CpCCpqCrq = DDD1D11DDD[0]D[0]D1D[0]D1D11[0][2]D11
[11] CCCNCNpqrsCps = DD11DDDDD111[1]D1D11DD11DDD[0]D[0]D1[0]DD1DD1111[2]
+ [12] CpCNpq = D[6]D[1][7]
+ [13] Cpp = DD[6]DD11[10]1
[14] CNNCpqCrCpq = DDDD11[9]DDDD1DD1111D[0]D1D11DDD11[9]DD11DDD11DDD[0]D[0]D1[0]DD1[0]1DD11DDD[0]D[0]D1[0]DD1[0]1DD11DDD[0]D[0]D1[0]DD1[0]1[2]DDD1[0]1DDDD111[1]D111
[15] CCNCCpCqpNrsCrs = D[1]DD1[8][14]
[16] CNpCqCrCps = D[5]DDD[2]D1DDDDD[2]D111D[0]D[0]D1DDD1DD1111D[0]D1D111D111DD[0]DDD1DD1111D[0]D1D11[15]
[17] CCNNpqCpq = D[1]DD11D[5]DD[1]DD11D[15]D[5]DDD1[0]1DDDD111[1]D11D[6]D11
[18] CCpqCCCrrNCNNpsq = D[1]DD11DDD11DDDDD[2]D111D[0]D[0]D1[3]1D[1]DD1[13][14][3]
[19] CCCpqCNprCsCNpr = DD11DDD[2]DD[0]D[0]1[7]1D[4]D[6]DD[2]D11D[6]DD1[8][14]
+ [20] CCNppp = D[15]DDDD11D[5]DDD1DD1[0]11DDD1[0]1DDDD111[1]D11DD[1]DD11D[5]D[6]D[15]D[5][3][7]1
[21] CCNpCCNqrCqsCCspCqp = DDDDD11D[5]DD[1]DD11DD[19]DD[1]DD1[13][14]D[5]D[2][3]1D[6]D11DD11DD[1]DD11DD[19]D[2]D[2]D[17]D[5]D[2][3]1D[6]D1111
+ [22] CCpqCCqrCpr = D[2]D[2][21]
+ [23] CCNpNqCqp = DD[21]DDDD11DDDD11D[5]DD[1]DD11D[5]D[5]D[2]D[15]D[5][3]D[5][3]D[5]D[11]D[1][7]1[9]1D[6][15]
+ [24] CCpCqrCCpqCpr = DDD11DD[1]DD11DD[19]D[2]D[17]D[5]D[2][3]1DDD[2]D11D[17]DDDD11DDDD11[9]D[4]D[5]DD[1]DD11D[11]D[15]D[5][3][7]1[9]1D[1]DDDDDDD11[16]DD11[9]1DD[1]DD11DDD[2]DD[0]D[0]1[7]1D[17]D[5][3][10]DDD1DD1111D[0]D1D11[7]DD[21]DD[1]DD11DDDD11D[5]D[18][16]D[17]D[5]D[2][3]1DDDD11D[5]D[18][9]D[4][22]1[3]The main method (described at the top) includes files with search results from a w3-extraction Generated Data
Extraction ProcedureFurther generation of w3's data based on [3dcaae4] w3:(A2:2762055↦614905,A3:182879↦51239,L1:180451↦39253,L2:2177↦1649) like
After extracting existing data via and appending was used to create a new extracted generation data directory at Consequently, were static reinsertions, and only were still to reinsert upon further to be inserted on the fly, instead. Summed up, the following generation steps took place after static reinsertions:
Generation of
Routinely used commands
w4: (A2: 13917↦13819, A3: 10779↦10719, L1: 12081↦11989, L2: 1709↦1703) CpCCNqCCNrsCtqCCrtCrq = 1
[0] CCpCqrCpCqp = DD111
[1] CpCCNqCCNrsCtqp = D[0]1
[2] CpCNCqrp = D[0]DD[0]D[1]11
[3] CCpCNqCCNrsCtqCpCCrtCrq = DD11D[2]1
[4] CCpqCpCCNrCCNstCurq = DD11D[2]D[1][1]
+ [5] CpCNpq = DDD11D[2][1]DD[0]D[1]11
+ [6] CpCqp = D[0]DDD11DDDD11D[2]D[0]D[1]1111
[7] CCpqCpCrq = DD11D[2]D[1][6]
[8] CCpqCCrpCrq = D[3]D[7][1]
[9] CCpCqNqCpCqr = DD11D[2]D[1]DD11D[3]DD[0][0]DDD11D[2]D[4][1]DD[0]D[1]11
+ [10] Cpp = DDDDD[3]DD11D[2]D[1]D[4][6]D[7]DDD11D[2]D[1]DD11DDD11D[2]D[1]DD11D[2]D[1]DDD11D[2][1]DD[0]D1111D[0]D[2]1111
+ [11] CCNppp = DDD11DDD11DD[0]DD[0]D111D[4][1]DD[0]D[1]11DDD11DDD[3][4]D[2]D[7]D[9][6]DDD[3][4]D[9]DDDD11D[4]D[3]DDD11D[2]D[1]DD11D[2][5][2][0]1DDDD11D[4]D[3]DDD11D[2]D[1]DD11D[2][5]D[0]D[2]1[0]1DD[3][4]D[9]DDD11D[2]D[1]DD11DDD11D[2]D[4][1]DD[0]D[1]11[6]
[12] CpCCpqq = DDD[8][11][7]DDD[3][4]D[2]D[9][6]DDD[8][11]DD11D[2]D[1][5]DDD11D[2]D[1][7]DDD11D[4]DDD11D[2]D[1][5][6][10]
+ [13] CCNpNqCqp = DD[8]D[12][10]D[3]DD[3]DDD11D[2]D[1][2][1][12]
+ [14] CCpqCCqrCpr = DDDD[8]D[12][10]D[3][4]DDD[3]DDD11D[2]D[1][2][1][12]DDD[3][4]DDD11D[2]D[1]DDD11D[2][1]DD[0]D111D[7]D[9][6][10]DDD11D[2]D[1][7][8]
+ [15] CCpCqrCCpqCpr = D[3]D[7]D[14][11]w5: (A1: 83↦75, A2: 157↦153) CCpqCCCrCstCqCNsNpCps = 1
+ [0] CCpqCCqrCpr = DD11D1DD11D1D11
[1] CCCpCqrCCCsqtCNqNsCsq = DDD11DD1D11D1DD1D11DD11D1DD11D1DD1D1DD11D11D1D111
+ [2] CpCNpq = D[1]1
+ [3] Cpp = D[1][0]
+ [4] CpCqp = DDD11DD1D1DDD11DD11D1DD11D1DD1D1DD11D11DD11D1DD11D1DD1D1DD11D11D1D111D1D111
+ [5] CCNpNqCqp = DD1DD11DD1D1DD1D1D1D11D1D11D1DD1D11D1D11D1D1[2]
+ [6] CCNppp = DD1[0]DD11D1DD11D1DD1DD11D1D1DD11D1DD11D1DD1D1DD11DD1D1DD1D1D1D11D1D11D1DD1D11D1D11D11D1D11
+ [7] CCpCqrCCpqCpr = DDD11D1D11DD1DD11D1D[1]D1DD11D1DD1D1DD11D1DD11D1DD1D11D11D1D11D1DD11D1D1DD11D1DD11D1DD1D11D1[0]w6: (A2: 18339↦10343, L1: 2743↦1821) CCCpqCCCNrNsrtCCtpCsp = 1
[0] CCCCNpNqprCqr = D1DD11D11
[1] CCCppqCrq = D1DD1D111
+ [2] Cpp = DDDD1D11D1111
+ [3] CpCqp = D[0][1]
[4] CCpCpqCrCpq = D1D1[3]
[5] CCCpqrCqr = D1D[3][1]
+ [6] CpCNpq = DDD1D11D1D[4]D111
[7] CpCqCCCrrNps = D[0]D1D[3]DD1D1D[0]D11[1]
[8] CpCCpqCrq = D[5]D[5]1
+ [9] CCNppp = DD[4]D1D1DD[4]D1D1[8]11
[10] CCNpqCNCrpq = D1DD1D1DD1D[3]D1DD1D[3]1D1D[4]D11[7][1]
[11] CCpqCCCrrpq = D1DD1D1DD[4]D1D1[8]1DD1DD1D1[7][1][1]
+ [12] CCNpNqCqp = D[0]D1D[4]D1D[3]D[4]DD1D[4]D1D[3]DD11D[0]D1[8]D1DD1D1[7][3]
[13] CCCCpqqrCpr = DD[5]1D[11]DDD[5]1D[11][8]DD[4][4]1
+ [14] CCpqCCqrCpr = DDD[5]1D[11]DDD[4]D1D1D[5][3]1DDDDD1D[5]1D[5][3]1DDD[5]1D[11]DDD1D1D[0]D11[10]1DDD1D11D1D[4]D1[8]1D[10]DDD1D1D[0]D11D1D[4]D1D[3]DD11D[5]D[0]D1[8]1D[13]D[5]1
+ [15] CCpCqrCCpqCpr = DDD[14][14][13]DD[14][14]DDD[4]D1D1D[5]D[5][3]1D[13][14] |
Beta Was this translation helpful? Give feedback.
2 replies
-
|
The total amount of steps is reduced by 94%. Incredible result! |
Beta Was this translation helpful? Give feedback.
-
|
Yes, this is such a joy.. 🤗 *plays epic music* |
Beta Was this translation helpful? Give feedback.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
There are seven minimal single axioms for propositional logic in terms of {→,¬}, namely Meredith's axiom and Walsh's six axioms.
This thread is meant to allow anyone to participate in the challenge of finding shorter proof(s) in their corresponding Hilbert systems.
Further information about the here relevant proof systems — such as their behavioral graphs and known exhaustive proof data — is available at the project's readme. I summarized this challenge in a blog post.
Rules
All of the following rules are subject to be refined based on experience gained over time.
Challenge
There are seven theorems to prove in seven similar proof systems. The challenge is to minimize the proofs as much as possible. You may pick any number of theorems to prove in any of these systems, so there can be at most 49 evaluated proofs per solution.
Each combination varies in difficulty, and I will state a subjectively perceived difficulty (range 1 to 10) for each system. In the hardest system (called w2), three proofs were missing at first.✻ I initially provided D-proofs for all other combinations.❈
Some proofs are so long that surely there must be shorter ones, but several are already minimal or likely close to minimal, which can be seen by the number of steps covered by an exhaustive search, which is also provided.
✻This means that only non-constructive proofs (via binary resolution) were known. Their length is here considered to be ω (i.e. countably infinite).
❈These proofs, my data, and the information provided in the comments by participants, may be used as valuable hints.
Comments
Comments do not have to contain answers but may contribute to discussions revolving around this challenge. Towards more in-depth examinations, please consider to open new threads with title prefixes “[PMC: general]”, “[PMC: 1-basis C-N]”, “[PMC: m]”, “[PMC: w1]”, or similar.
Answers
Answers should include a text-based abstract representation similar to the one I provide, unless a D-proof is short enough to be stated in full (at most a few thousand characters), in which case it can be stated concretely. Of course, you can additionally provide the proof in whichever representation you like, e.g. with all used logical formulas, in infix notation, image-based, etc. An explanation on how you succeeded and where you failed would be nice, but is not required.
Improvements can be summarized in the header like “<system>:<theorem>:<steps before>↦<steps after>, ...”, e.g. “w2:A3:9001↦1337, w4:id:465↦379”. I might comment and/or edit relevant scoring information.
I will use GitHub usernames for the score board by default. In case you would like to be mentioned by name (or a different pseudonym) here and in potential publications, please state so in your answer or via mail, and how.
Progress
This challenge is an ongoing global game for which one can lead a “highscore”, but progressing towards lower numbers. Starting with three proofs unknown, the initial value is
3ω+c, wherecis the sum of steps of smallest known proofs, one for each solved target theorem. The game becomes even harder once it progresses, but latest successes automatically grant a top ranking. For that, I'll maintain a table below.I have hopes that it will someday reach a finite amount close to several thousand steps. It seems plausible that this is possible when looking at high exponential growths in the amounts of theorems when doing exhaustive generations. Quantum computers might help a lot in the foreseeable future.
Hall of Fame
The top entry is supposed to contain the most recent world record — it therefore takes into account external sources, which should be cited and summarized in corresponding answers, with original authors credited below.
w2: {A2,A3,L1,L2}: 1855182↦40676,
w3: {A2,A3,L1,L2}: 296046↦23888, w4: {A2,A3,L1,L2}: 38486↦38230,
w5: {A1,A2}: 240↦228, w6: {A2,L1}: 21082↦12164
w3: {A2,A3,L1,L2}: 707046↦296046,
w4: {A2,A3,L1,L2}: 45386↦38486, w5: L2: 107↦103
Consecutive entries of the same person are combined such that it benefits conciseness and legibility.
Proof Systems
We are exploring the seven minimal 1-bases for classical propositional logic that use operators → (read: “implies”) and ¬ (read: “not”) with modus ponens (⊢ψ,⊢ψ→φ ⇒ ⊢φ, also called “detachment” or “implication elimination”)✻ as a rule of inference.
✻This rule can be read as “if (the proposition) ψ is provable and (the proposition) ψ→φ is provable, then thereby (the proposition) φ is provable”. An operator '⊢' for ”is provable” is not part of the propositional language. Propositions merely argue about truth, using '→', '¬', and other propositions. For example, the formula ψ→φ can be read as ”if (the proposition) ψ is true, then (the proposition) φ is true”. Suppose ψ→φ is true. When also ”(the proposition) ψ is true”, it follows via modus ponens that ”(the proposition) φ is true”. This kind of argument is the only one allowed in our proofs. Variables (such as ψ and φ) can be instantiated with arbitrary propositions (i.e. formulas in our propositional language).
Axioms
CCCCCpqCNrNsrtCCtpCspCCpCCNpqrCsCCNtCrtCptCpCCqCprCCNrCCNstqCsrCpCCNqCCNrsCptCCtqCrqCpCCNqCCNrsCtqCCrtCrqCCpqCCCrCstCqCNsNpCpsCCCpqCCCNrNsrtCCtpCspDifferent axioms are not allowed to be combined with each other. Indeed, each of these formulas is capable of deducing all theorems of propositional logic using only modus ponens as a rule of inference.
In order to save space, I will use normal Polish notation, a most concise (and well-googleable) prefix notation with (→,¬)=(
C,N) for up to 26 different variablesp,q,...,z,a,...,o, to state conclusions in proof summaries. You may use whichever well-defined formula representation suits you. Actually, a formula is simply a tree structure — follow the links in the leftmost column for graphical representations. A general way (which works for more than 26 different variables) to concisely state formulas is to use numbers as variables and separate them via., e.g.CCCCC0.1CN2N3.2.4CC4.0C3.0for Meredith's axiom.Target Theorems
The target theorems are themselves axioms of popular proof systems, such as {A1,A2,A3} (“Łukasiewicz (L_3)-system”) and {L1,L2,L3} (“Łukasiewicz (L_1)-system”). Propositional axioms of Metamath's main proof database set.mm are also A1-A3.
CpCqpCCpCqrCCpqCprCCNpNqCqpCppCCpqCCqrCprCCNpppCpCNpqProving all axioms of a different proof system that is known to be complete (such as A1-A3 and L1-L3 both are under modus ponens) proves that the original system is complete by itself. There are also non-constructive ways to prove this, which is how we knew that w2 is complete under modus ponens before corresponding D-proofs were known.✻ Analysis of the length of D-proofs can potentially help in finding proof theoretic bounds, which are still a big mystery in the field of proof complexity.
✻The authors of Walsh's paper called the task to find D-proofs from w2 to another system an “open challenge problem for automated reasoning”. We solved it.
Proof Notation
The operator for condensed detachment is the so-called
D-rule, which takes two formulas as arguments, on which it applies tree unification to form the most general unifiers of ψ→φ and ψ, respectively, then applies modus ponens, which results in φ. Axioms in D-proofs are referred to by1,2,…,9,a,b,…,zin their given order.This way, given a sequence of axioms, a proof can be defined by a single prefix formula, e.g.
DD211, which is evaluated likeD(D(2,1),1), i.e.Dis a 2-ary (partially defined) operator over the language of logical formulas.The
D-rule is only partially defined because unifiers to apply modus ponens on certain formulas may not exist.Example
Let's determine
DD211for axioms (1,2):=(A1,A2). At firstD21entails that ψ→φ and ψ are instances of A2 and A1, respectively. Most general such unifiers are the instances (χ→(ξ→χ))→((χ→ξ)→(χ→χ)) and χ→(ξ→χ) of A2 and A1, which implies ψ := χ→(ξ→χ) and φ := (χ→ξ)→(χ→χ). Therefore, (χ→ξ)→(χ→χ) (i.e.CCpqCppin Polish notation) is an intermediate theorem inDD211=D(CCpqCpp)1. This entails that now ψ→φ and ψ are instances of (χ→ξ)→(χ→χ) and A1, respectively. Most general such unifiers are (χ→(τ→χ))→(χ→χ) and χ→(τ→χ), thus ψ := χ→(τ→χ) and φ := χ→χ. Therefore,DD211proves the theorem χ→χ (i.e.Cppin Polish notation). Combined, the D-proofDD211w.r.t. (A1,A2) actually means:Alternatively, using Polish notation:
CpCqp(1)CpCCqpp(1)CCpCCqppCCpCqpCpp(2)CCpCqpCpp(D):2,3Cpp(D):1,4By command:
There are no such small examples in our single axiom systems, for example
D11in Meredith's system is alreadyCCCCCqsCNCNpNtNrCNpNtpCCpqCrq(1)CCCCCCqsCNCNpNtNrCNpNtpCCpqCrqCCCCpqCrqCqsCtCqs(1)CCCCpqCrqCqsCtCqs(D):1,2By command:
and formulas tend to blow up in size for longer proofs.
This illustrates that using formula-based proofs is extremely inefficient, whereas D-proofs are much lighter and can be processed by machines more efficiently.
Note:
Using
-uinstead of-nafter--parseprints formulas in infix notation with variables 0,1,2,… and operators as Unicode characters, e.g.:Challenge Proofs
I will try to keep this information up to date.
The smallest known D-proofs of target theorems have the following amounts of steps.
For example, to the best of my knowledge I searched Meredith's system exhaustively for D-proofs of up to 83 steps. Since all its D-proofs have odd lengths, all its smallest known D-proofs with up to 85 steps are thereby minimal and cannot be reduced further. That is, if my search was actually exhaustive.
My (subjective) overall difficulty rating accounts for how hard I find searching and handling proofs, not for the apparent complexity of a system (which is indicated by “exhausted” — the higher the longer proofs are on average). The issue with a lower difficulty rating is that the given proofs might be so short already that it is very hard to find a smaller one (if it even exists). On the other hand, more difficult systems potentially allow for greater accomplishments.
Compact representations of these proofs are given below. Unfoldings into concrete D-proofs can have exponential blowup. Target theorems are highlighted. More detailed and commented variants representing the same D-proofs are linked at the system identifiers right to the bullet points (and as “[sample]” in the project's readme).
Puzzle Board (Abstract Representation)
Where do I even start?
This is a logic puzzle game with infinitely many pieces: Proofs for different theorems are components which can be used to build new components when arranged in a specific (and potentially very difficult to find) way. When it comes to snapping formulas together in order to create another one, things behave the same in all
D-systems.The above abstract proof representations hide many utilized formulas, but these can be viewed using pmGenerator to display the “full summary” as mentioned in the linked proof files — deriving them by hand is probably too much of a workload. It may be useful, however, to write your own code to assist with this kind of work, and to follow your own ideas.
This is not necessary when approaching things like I already did. Let's take this route for illustration.
Initial Approaches
Starting on the proof files linked in the project's readme, the descriptions of some of my commits explain roughly what I did:
Doing this requires a large amount of time and memory, so I uploaded my results for everyone who would like to use them.
I am only aware of two more automated theorem provers that are capable of hyper resolution: Otter and GKC. Prover9 and Otter are much more useful for this purpose due to their powerful hint system.
1to align the final result with exhaustively generated data.Advanced Approaches
Certain strategies are known to have high success rates, such as utilizing
--assess) just marginally feasible while considering some long formulas, such as illustrated in an answer for w2,--transform -z) with proofs for additional potential intermediate conclusions in order to find an optimal solution over only the formulas used in that solution, which was used in the exemplary answer as part of its main strategy.Inference rules can help to greatly reduce lengths of formulas to work with, such as in this solution where proofs were searched for manually, assisted by metamath-exe.
More Data & Tools
To be updated.
Current shortest known proofs in terms of L1-L3 (i.e.
CCpqCCqrCpr,CCNppp,CpCNpq) of A1-A3 as theorems are:All of L1-L3 are proven in the (exhaustively generated) top1000SmallestConclusions_1to39Steps.txt, by which they have minimal proofs
DD2D1D2DD2D1211,DD2DD2D13D2DD2D1311,DD2D1D2DD2D1311of lengths15,19,15, respectively.Prover9
tfor 'theorem', unary function symbolnfor 'negation', and binary function symbolifor 'implication'.An input file such as w2.in can be utilized like
./prover9 -f w2.in > w2.out. Prover9 can quickly prove theorems id, A1, L2 and L3 due to the provided hints, which were generated from w2.txt viaand subsequently modifying✻ 'tmp.txt' such that it contains only comma-separated D-proofs, then using:
However, due to the hardness of w2, Prover9 did not find any more theorems in several weeks of runtime, even when additionally adding all formulas from top1000SmallestConclusions_1to43Steps.txt as hints, which can be generated like so:
It turned out that w2 is by far the hardest of our systems: Prover9 managed to prove all seven theorems for every other system, based only on hints from their corresponding top lists. This usually took a few days.
Generated proofs can be converted to D-proofs using
./prover9OutputConverter. It often proved useful to generate similar proofs several times using different settings, then combining their strengths in order to find shorter D-proofs.✻In case there are large lines, only a few text editors are capable to edit them without issues, such as EmEditor and BssEditor.
TPTP / Vampire
Using
./CNFFromTopListto look for plausible conclusions in top lists may be useful to verify whether they actually entail a certain proposition. For example, the following input is detected as 'satisfiable' by Vampire 4.8, which means that {CpCqp, CNCpCCCqqrrs, CpCqCNrCCCNqsrt, CpCqCrCCCNpsNpt, CpCqNCCNprNCsCtq, CCCNpqCCNCrrstCpt, CCCpCNCqCNCrqstuu} does not entail L1:Beta Was this translation helpful? Give feedback.
All reactions