[Termtools] A proposal for the next competition

[Koprowski, A.]

  Dear all,
 
 Let me add two words to the discussion.
 With respect to Claude's proposal I share Jurgen's opinion that we should decide whether we want to make a competition for the most powerful or fastest tool. I'm for the former and I guess most of us will agree on that subject so I don't think it's a good idea to limit the time per problem (and punish tools that can solve systems but can do that in more than 5sec.). I agree that it is interesting to see which systems can be solved given more than 1 minute but this question is independent of the competition itself. But how about instead of rewarding fast responses reward solving difficult problems? For instance we could give bonus points for solving TRSs that no other tool could solve. But I think we should try to keep the rules simple so I'm not sure whether this is sensible; just a thought.
 Considering Hans' proposal of making the output somehow more formal I fully agree. Termination tools are getting more and more complex and as always with complicated software bugs happen. Also the proofs itself are getting more involved making it difficult to verify them by hand. Also some of the tools can be used not only for proving termination itself but for some form of verification (AProVE can prove termination of programs and liveness properties, TPA can prove liveness properties... maybe some more that I'm not aware of) and hence may be used by non-term-rewriting-experts. So making the results somehow more reliable is a clear goal. And I believe that this is a nice first step in that direction.

  Kind regards,
   Adam

--
========================================================================
 Adam Koprowski, (A.Koprowski at tue.nl, http://www.win.tue.nl/~akoprows)
 Department of Mathematics and Computer Science
 Eindhoven University of Technology (TU/e)
 The difference between impossible and possible lies in determination
      Tommy Lasorda
========================================================================
_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools