Dear Florian, dear all,
(b) go back to the old format [1] (here's [2] an example)
...
Contra: There were some issues with the semantics,
also - cf. "Wadler's law of language design", issues with (comment) syntax (? - everything that's invalid, is accepted as comment)
for reference, early discussion is here https://verify.rwth-aachen.de/termtools/2003-November/subject.html
(c) a new S-expression based format has been proposed for the confluence competition [3]
Pro: human readable(?)
Pro: the format is used for SMTLIB as well (?)
- If you participate, can your tool still parse the old format?
matchbox - yes. https://hackage.haskell.org/package/tpdb
- Do you recall more details about the reasons for the switch from the
old format to the current one?
* avoiding discussion of concrete (surface) syntax, e.g., what is a valid identifier, a comment, etc.
* validation of termination proofs needed a (machine-readable) exchange format anyway (cf. https://verify.rwth-aachen.de/termtools/2007-May/000325.html ) but - TRS in CPF syntax (certificates) is not the same as TRS in XTC (benchmarks)? And the name is wrong ... https://verify.rwth-aachen.de/termtools/2009-December/000787.html
* XML was all the rage in the 90s - as was JSON was after that, and S-expressions before.
- Johannes.