Alternative tools and better ways to parse and validate proofs

[proof-theory]

You mentioned CD Tools in your previous answer, but while it appears to have lots of documentation, it provides only a few examples, requires knowledge of the Prolog language, requires installation of third-party compiler or interpreter software, and is complicated to use. For example, its condensed detachment proofs use excessive syntax, such as illustrated in CD Tools' example for LCL038-1:

d(d(d(d(1,d(d(A,A),1)),1),1),1)-[A=d(1,d(d(B,1),B)),B=d(d(d(d(1,d(1,d(1,d(1,d(d(d(d(1,d(1,d(1,1))),1),1),1))))),1),1),1)]

I could translate this into

./pmGenerator --transform "CCCpqrCCrpCsp=1,[0]CCCpCqrCstCCqtCst=DDDD1D1D1D1DDDD1D1D11111111,[1]CCCCpqCrqCCCsCptCrquCvCCCsCptCrqu=D1DD[0]1[0],[2]CCpqCCqrCpr=DDDD1DD[1][1]1111" -n

after figuring out CCCCpqCrqCCCsCptCrquCvCCCsCptCrqu and CCCpCqrCstCCqtCst for A and B, respectively, but it gets really messy with the next example

d(d(1,d(A,d(d(d(d(A,B),C),D),E))),d(F,d(F,1)))-[G=d(1,d(1,d(1,1))),H=d(1,I),I=d(1,J),K=d(1,d(B,d(1,d(d(1,d(C,d(C,d(d(D,J),I)))),1)))),F=d(1,d(A,d(1,d(A,H)))),J=d(G,G),B=d(H,1),L=d(H,B),D=d(d(1,d(1,d(I,E))),1),M=d(d(d(1,d(1,L)),B),1),E=d(M,d(1,C)),C=d(M,B),A=d(d(d(K,d(H,d(M,K))),1),L)]

for LCL073-1, which has many variables whose expressions are given in seemingly random order.

• Can we parse proof summaries without having to provide formulas for each part?
• Do you know other software to parse and validate condensed detachment proofs?
  Preferably easy to use.

[xamidi]

d(d(1,d(A,d(d(d(d(A,B),C),D),E))),d(F,d(F,1)))-[G=d(1,d(1,d(1,1))),H=d(1,I),I=d(1,J),K=d(1,d(B,d(1,d(d(1,d(C,d(C,d(d(D,J),I)))),1)))),F=d(1,d(A,d(1,d(A,H)))),J=d(G,G),B=d(H,1),L=d(H,B),D=d(d(1,d(1,d(I,E))),1),M=d(d(d(1,d(1,L)),B),1),E=d(M,d(1,C)),C=d(M,B),A=d(d(d(K,d(H,d(M,K))),1),L)]

for LCL073-1, which has many variables whose expressions are given in seemingly random order.

• Can we parse proof summaries without having to provide formulas for each part?

We can now parse proof summaries without intermediate conclusions via --transform -w , which I just added following your request.
The function DRuleParser::recombineAbstractDProof() already worked fine without, but the command-line interface first calls DlProofEnumerator::recombineProofSummary(), which previously required all intermediate conclusions to be validated. This can now be disabled with option -w , in which case no formulas apart from axioms shall be given.

Since order of evaluation does not have to be respected for proof summary steps, straightforwardly translating helper variables in their given order via

G	H	I	K	F	J	B	L	D	M	E	C	A
[0]	[1]	[2]	[3]	[4]	[5]	[6]	[7]	[8]	[9]	[10]	[11]	[12]

yields the command

./pmGenerator --transform "CCCCCpqCNrNsrtCCtpCsp=1,[0]=D1D1D11,[1]=D1[2],[2]=D1[5],[3]=D1D[6]D1DD1D[11]D[11]DD[8][5][2]1,[4]=D1D[12]D1D[12][1],[5]=D[0][0],[6]=D[1]1,[7]=D[1][6],[8]=DD1D1D[2][10]1,[9]=DDD1D1[7][6]1,[10]=D[9]D1[11],[11]=D[9][6],[12]=DDD[3]D[1]D[9][3]1[7],[13]=DD1D[12]DDDD[12][6][11][8][10]D[4]D[4]1" -n -w -t .

which orders input and prints the same proof summary that was already mentioned in my previous answer:

    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

Note that helper variables in CD Tools' example for LCL073-1 are provided in order G,H,I,K,F,J,B,L,D,M,E,C,A, but their order of evaluation is uniquely determined as G,J,I,H,B,L,M,C,E,D,K,A,F.

Alternatively, we can obtain the command

./pmGenerator --transform "CCCCCpqCNrNsrtCCtpCsp=1,[0]=D1D1D11,[1]=D[0][0],[2]=D1[1],[3]=D1[2],[4]=D[3]1,[5]=D[3][4],[6]=DDD1D1[5][4]1,[7]=D[6][4],[8]=D[6]D1[7],[9]=DD1D1D[2][8]1,[10]=D1D[4]D1DD1D[7]D[7]DD[9][1][2]1,[11]=DDD[10]D[3]D[6][10]1[5],[12]=D1D[11]D1D[11][3],[13]=DD1D[11]DDDD[11][4][7][9][8]D[12]D[12]1" -n -w -t .

with input respecting to evaluation order.

For usability, you can find and replace regular expressions via \] *[^:= \n,]+[:= ]+ ↦ \]= in a text editor to remove conclusions from proof summaries.

• Do you know other software to parse and validate condensed detachment proofs?
  Preferably easy to use.

Yes, I recently wrote a small program in Lean 4 to define, parse and validate D-proofs. Most of the parser was actually written by Mario Carneiro, who is a former member of the Lean development team and helped me on the Lean research community chat.
The linked code snippet supports nice syntax and doesn't need installation of third-party software since it uses a web editor as interpreter, but so far it cannot parse proof summaries, only concrete D-proofs.

Thus far, I am not aware of any other software capable to parse D-proofs with user-defined axioms. There is a C program drule.c mentioned in Metamath's pmproofs.txt to evaluate concrete D-proofs when based on propositional axioms of Metamath's set.mm.
Future updates of further entries would be appreciated.

When it comes to formula-based condensed detachment proofs, however, there are of course many tools able to parse them, like pretty much every automated deduction tool.