[Termtools] belated response

[Aart Middeldorp]

Here is a somewhat belated response to the recent email discussion:

- The exam mode proposal of Jörg (having a single timeout for the
   whole set and leave it up to the tools to divide this over the
   individual problems) is elegant.

- To make the competition more interesting (at least for human
   observers) one might consider running the participating tools
   on a fairly random selection of TPDB. One can even think of
   doing this live during a session in the Termination Workshop.
   As motivation: looking at last year's competition, the tools
   in the TRS competition either did very good or very bad on the
   "currying" and "higher-order" systems.

- Concerning Hans' question

   > To my opinion this would be a valuable first step towards
   > verifying generated proofs. For the competition participants I
   > have the following questions:
   > * Do you agree?
   > * Are you willing to accept these rules and adjust your tool
   >   and/or submit a list of techniques used?

   I am not in favor of requirements that make it harder for new
   tools to join the competition. Are there any persons on this
   mailing list who are currently not involved in the competition?
   What do you think should be done about the competition to make
   you participate?

Cheers,

Aart
_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools