[Termination tools] Competition

[Juergen Giesl]

Dear all,

like Johannes, I would also like to thank Claude and Hans
very much for organizing and running the competition! I think
you did this very well! I also think the competition was very
exciting and interesting. It stimulated a lot of research and work
on beforehand and it also gave interesting results.
I was also impressed by the performance of several of the participating
tools (in particular, also of the "newcomers" who participated for
the first time with surprising success).

Concerning the unsatisfactory points: For several categories,
it would be rather easy for the authors of the existing TRS-tools
to extend their tools to these categories. This holds at least for LP,
CTRSs, and context-sensitive rewriting, since here, the termination
problems can simply be translated into termination problems of ordinary
TRSs. I would encourage all tools to do that, since this allows a comparison
of the tools on the special forms of termination problems which result
from these areas.

I also think that we should do everything we can to motivate the non-participating
tools (the ones from LP and the non-participating rewriting tools) to
participate next year.

 > 3) I find the 1 minute timeout a bit to low. I would like to suggest,
 >    for the next competition, a larger one, say 5 minutes.

There are indeed a number of problems where the tools would find the proof
if the runtime was longer (at least this is true for AProVE). On the other hand,
of course the runtime must be such that the competition can be completed
in at least a few days.


 > 2) When should it take place ? If it was much before WST (or RTA), we
 >    could have an opportunity the insert a report on the competition in
 >    WST (RTA ?) proceedings.

An insertion at least into the WST-proceedings should clearly be possible
if one holds the competition long enough in advance. I also think that this
could be a good idea.

 > 4) Should we add new categories ? higher-order rewriting ?

We should make sure that there are enough participants for these categories.
Concerning higher-order rewriting, we added a number of examples into the TPDB
where higher-order functions are encoded by first-order TRSs. For such TRSs,
no special category is needed. For real higher-order rewriting, the problem
is that there are several variants of it. Currently, the only tool I'm aware of
which works on higher-order TRSs is TTT (it works on simply-typed TRSs).

Since here, the termination proofs work via a translation into first-order TRSs,
the other tools could easily be extended to accept these higher-order TRSs as well.
So maybe it is a good idea to add this category (what do you think, Aart?).

For other (full) higher-order TRSs, I'm not aware of any automatic termination
tool which can handle them.


 >
 > 5) How could we enhance the tpdb ? Are there volunteers to work on it ?

I had some discussions with Geoff Sutcliffe who organizes the TPTP and the
first-order theorem proving competition at CADE. He organizes this
more or less "full time" and spends a considerable amount of effort in
maintaining it. Moroever, they have carefully selected rules for the competition.
It might be interesting to have a closer look at their form or organizing
the competition and the data base. Maybe we can get some ideas for improvements
from there.

Best Regards
Juergen