termCOMP discusson @ WST '26

[ffrohn]

Like last year, there will be a (short) timeslot at WST to discuss termCOMP related questions, so I'd again like to collect ideas for that.

As a starting point, here are the ideas that were collected last year:

• Full run vs. running on subsets of TPDB? --> resolved (both)
• "Bring your own benchmarks": The idea is that everybody who wants to participate has to contribute a certain number of benchmarks. This is done at the SAT competition. --> resolved (proposal accepted)
• Do we want winner's certificates? --> resolved (yes)
• Uniform format for certification? --> open
• How to deal with several certifiers? Do we want a "competition" between certifiers? --> open
• clean up termination-portal.org --> in progress
• move termination-portal.org to some more recent infrastructure --> open
• Shall we try to standardize ARI (together with CoCo)? --> partially resolved (termCOMP reference)
• Docker / new infrastructure: experiences, criticism, ideas to improve... --> still relevant
• How can we attract new / more participants? --> partially resolved (publicity chair)
• New categories? --> none so far
• Shall we archive participating provers (e.g., on Zenodo)? --> resolved (yes)
• Demo categories: At least this year, they caused tons of work, and I don't see much benefit. Other competitions do not have them either, as far as I know. I'd like to get rid of them. --> resolved (run on request only)
• infrastructure (let's wait for results but ...) matchbox wants: more time, or more cores, or both. mnm wants: more RAM (I guess). --> partially resolved (more time, but same number of cores & RAM)
• not at business meeting, but at workshop dinner: ask participants for predictions (bets) on certain outcomes of the competition (Geoff does something like this for CASC, https://tptp.org/CASC/30/Gambling.html) --> open
• more open ideas: https://git.imn.htwk-leipzig.de/waldmann/cetera/-/blob/wst2025/doc/wst25/talk/termcomp.tex?ref_type=heads --> open

As you can see, many points have been resolved (partially), so I think the discussion payed off.

[nilslommen]

• Should we merge benchmark sets and remove duplicates? For example, Integer_Transition_Systems and Complexity_ITS or C_Integer and Complexity_C_Integer.

[jwaldmann]

SRS benchmark names (in Wenzel16, Cirpons25) are too long, and un-memorizable . Can we rename the files to use numbers instead? (put previous name in meta-data and use it for comparing results of different termcomp years).

several certifiers - we don't have (externally visible/presentable) progress on cetera (our certifier in Agda) right now. But perhaps there are others? At some point, Lean foundation will detect this opportunity for advertising their system, or rather, their sponsors' LLMs.

[jwaldmann]

require participating software to be open source? mild versions:

• require all participants to make their docker container public (after submission deadline)
• require the winner to go open-source (else, they don't get a price)

[J-C-Kassing]

After seeing the new website for the rewriting community (https://rewriting.inria.fr/introduction), I am in strong favor of moving termination-portal.org to some more recent infrastructure, removing all outdated stuff, and making the site overall more accessible. (Maybe asking for advice from the Inria group that worked on this website.)