[PMC: 1-basis C-N] Looking for related formally published scientific literature

[proof-theory]

I am looking for formally published literature related to the problems discussed in [PMC] Minimal 1-bases for C-N propositional calculus.
I noticed that the mentioned paper by Walsh and Fitelson remains an uncorrected preprint, informally published in 2021.

• Are there published proofs relevant for that challenge which are also styled in a similar manner?
• Where can I find more closely related literature?

[xamidi]

AFAIK, none of Walsh's six single axioms for C-N propositional calculus occurred in a peer-reviewed journal (yet)^✻, but Meredith's single axiom was first mentioned by Carew Meredith in The Journal of Computing Systems in 1953, which is available on the Internet Archive.
Meredith proved m: L1 – L3^❈ there, but his proof is based on formulas, doesn't restore variable order and contains every utilized substitution, e.g. his first three lines

1   CCCCCpqCNrNsrtCCtpCsp
    1 p/Cpq, q/CNCNtNrNs, r/t, s/r, t/CCtpCsp × C1 r/CNtNr - 2
2   CCCCtpCspCpqCrCpq 

are just a way to write

(m) CCCCCpqCNrNsrtCCtpCsp
1. CCCCCpqCNCNtNrNsCNtNrtCCtpCsp  (m) ; 〈r, CNtNr〉
2. CCCCCCpqCNCNtNrNsCNtNrtCCtpCspCCCCtpCspCpqCrCpq  (m) ; 〈p, Cpq〉, 〈q, CNCNtNrNs〉, 〈r, t〉, 〈s, r〉, 〈t, CCtpCsp〉
3. CCCCtpCspCpqCrCpq  (MP):1,2

which is isomorphic to:

    CCCCCpqCNrNsrtCCtpCsp = 1
[0] CCCCpqCrqCqsCtCqs = D11

^✻_{Prof. Fitelson informed me one month ago in an email that their new plan was to “write a new (more comprehensive) paper”.}
^❈_{Provided in order L1,L3,L2, i.e. CCpqCCqrCpr,CpCNpq,CCNppp rather than CCpqCCqrCpr,CCNppp,CpCNpq.}

Theorems in normal Polish notation are generally well suited for search engines.

Regarding more recent literature and a prettier notation, I found the paper Lemmas: Generation, Selection, Application by M. Rawson, C. Wernhard, Z. Zombori and W. Bibel, which has been published as part of Springer's conference proceedings series Lecture Notes in Computer Science for TABLEAUX 2023. It has an extended version on arXiv, which in appendix F (last page) provides a constructive proof with “MGTs” (most general theorems) for TPTP's 1.00-rated^✻ LCL073-1 — the problem to prove that L1 can be derived from Meredith's single axiom via condensed detachment.

Their proof has a similar notation to the here used proof summaries, so it can straightforwardly be translated into

    CCCCCpqCNrNsrtCCtpCsp = 1
[0] CCCppqCrq = D1D1D11
[1] CpCqCrr = D[0][0]
[2] CCCpCqqrCsr = D1[1]
[3] CCCpqrCqr = D1[2]
[4] CpCCpqCrq = D[3]1
[5] CpCCCqprCsr = D[3][4]
[6] CCCpqrCCCqsCNrNpr = DDD1D1[5][4]1
[7] CCCpqCNCCCrpsCtsNrCCCrpsCts = D[6][4]
[8] CCCpqCNCrpNCCCsCptuCvuCrp = D[6]D1[7]
[9] CpCCqrCCNqNpr = DD1D1D[2][8]1
[10] CCCpNqCCqrCsrCtCCqrCsr = D1D[4]D1DD1D[7]D[7]DD[9][1][2]1
[11] CCpCqrCCCsCtNprCqr = DDD[10]D[3]D[6][10]1[5]
[12] CCCCCpqrstCCCqrst = D1D[11]D1D[11][3]
[13] CCpqCCqrCpr = DD1D[11]DDDD[11][4][7][9][8]D[12]D[12]1

for which ./pmGenerator --transform file.txt -f -n -p -2 -d reveals that it has a fundamental proof length of 6553 steps, compared to currently 459 steps for the smallest known D-proof.
They also have a big list of references towards related literature, some informally published — including Walsh's and Fitelson's preprint.

Searching for LCL073-1 further led me to CD Tools, whose SGCD^❈ prover according to the site was only the second program (after OTTER with a highly customized workflow) to solve it automatically.

^✻_{None of their 92 proposed automated theorem provers generated an actual solution — surprisingly not even Vampire 4.9 — which renders this problem “unsolved”.}
^❈_{Short for “Structure Generation for Condensed Detachment”, according to this paper by C. Wernhard on arXiv.}

[xamidi]

Regarding more distantly related literature, there is the option to search by Mathematics Subject Classification (MSC2020), e.g. on zbMATH. I would classify proof minimization as

• 03-XX Mathematical logic and foundations
  • 03Fxx Proof theory and constructive mathematics
    • 03F07 Structure of proofs
    • 03F20 Complexity of proofs

and algorithmic proof minimization, i.e. proof compression, additionally as:

• 03-XX Mathematical logic and foundations
  • 03-08 Computational methods for problems pertaining to mathematical logic and foundations
• 68-XX Computer science
  • 68Vxx Computer science support for mathematical research and practice
    • 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
  • 68Wxx Algorithms in computer science
    • 68W05 Nonnumerical algorithms
    • 68W30 Symbolic computation and algebraic computation

Exemplary search queries: "system cc:03F07 cc:03F20", "cc:03F20 cc:68W30", "short propositional cc:03F20"

It should be noted that there is a lot of literature in proof theory that is highly unrelated to the here relevant subjects. For example, the textbook Proof Theory: The First Step into Impredicativity by Wolfram Pohlers self-declares to fall into only different subcategories:

• 03-XX Mathematical logic and foundations
  • 03Fxx Proof theory and constructive mathematics
    • 03F03 Proof theory in general (including proof-theoretic semantics)
    • 03F05 Cut-elimination and normal-form theorems
    • 03F15 Recursive ordinals and ordinal notations
    • 03F25 Relative consistency and interpretations
    • 03F30 First-order arithmetic and fragments
    • 03F35 Second- and higher-order arithmetic and fragments

More relevant search query results that may also help with finding closely related categories:

• "condensed detachment" (≥ 36 results)
• "proof compression" (≥ 14 results)
• "proof minimization" (≥ 4 results)

Categories specific to the here conducted kind of proof minimization:

• 03-XX Mathematical logic and foundations
  • 03Bxx General logic
    • 03B05 Classical propositional logic
  • 03-04 Software, source code, etc. for problems pertaining to mathematical logic and foundations
  • 03-11 Research data for problems pertaining to mathematical logic and foundations
• 68-XX Computer science
  • 68Qxx Theory of computing
    • 68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
  • 68Rxx Discrete mathematics in relation to computer science
    • 68R07 Computational aspects of satisfiability
  • 68Wxx Algorithms in computer science
    • 68W10 Parallel algorithms in computer science
    • 68W15 Distributed algorithms
    • 68W32 Algorithms on strings