[Termtools] Remarks on the Termination Competition

[Salvador Lucas]

Dear all,

Zantema, H. wrote:

>Dear all,
>
>I am not in favor of Juergen's proposal. 
>
>The 2007 competition has finished now, with the results as we can read
>on the web page. I just saw Claude's email with the same conclusion.
>
>Juergen mentions two problems motivating his proposal.
>
>1. Unclear time limits. Indeed this was a problem. On the competition
>web page it was announced that the time limit would be in between 1 and
>5 minutes. Separate from that in discussions on termtools I proposed
>only to change time limits if this was announced in advance. Apparently
>this proposal was not followed by Claude, but he followed the range as
>it was announced on the web page. 
>
>2. Bugs found in tools. I think this is not different than other years.
>Remember that last year also there were two disqualifications: one due
>to a YES generation for a non-terminating TRS and one due to wrong
>proofs with agreement with the tool author. This year it was exactly the
>same, with the only difference that we decided not to show the
>disqualified tools. This decision was motivated by undesired effects of
>showing disqualified tools.
>There were indications that referees of papers written by disqualified
>tool authors were already negative in advance before even having read
>the paper. Of course this attitude is not fair, but we do not have any
>control on this. Due to this kind of undesired effects we preferred not
>to emphasize disqualifications.
>
>The fact that the TTT2 team now finds an error in their tool is in my
>view no reason of disqualifying / removing TTT2 from the competition
>results pages.
>
I would agree with this only if the TTT2 team could say that (as far as 
they are aware of)
all their proofs in the TRS competition are correct. In my opinion, it 
is not good that incorrect
proofs are publicly available through the web site of the competition. 
This was the main reason
for us to ask for the removal of MU-TERM's proofs.

> Several other tool authors found errors in their tools
>after the competition was finished without any consequence for the
>result pages.
>
Here, I would apply the same rule. Keeping wrong results available could 
become
problematic in the future... Actually, CiME and MU-TERM have been 
removed from the
2006 web site only few days ago,... Unfortunately, the public 
'disqualification' which has
been published in, e.g., the WST'06 proceedings cannot be erased now...

Best regards,

Salvador.