[Termtools] TermComp2020 is running

Johannes Waldmann johannes.waldmann at htwk-leipzig.de
Mon Jun 22 22:20:19 CEST 2020


thanks, Akihisa, for doing the work here!


> participation in debugging!


SRS_Relative/Waldmann_19 random problems are missing?
(they were used last year).

I think I have them here
https://gitlab.imn.htwk-leipzig.de/waldmann/tpdb/

Same for SRS_Standard/Waldmann_19 ?


Matchbox's proofs in SRS-Relative are wrong,
as they use the SRS-Standard method
(with inapplicable RFC matchbounds, DP transform)
(I already told Akihisa - probably the configuration Id was mistyped,
this is just in case others were wondering)


Also, I am currently not printing proofs, is this a problem?
https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/264



Best regards, Johannes.


More information about the Termtools mailing list