[Termtools] A proposal for the next competition

[slucas at dsic.upv.es]

Dear all,

I agree with Juergen that speed should not be the
most important issue in the competition. However,
it is an important aspect which should be somehow
promoted also (although without becoming 'the thing').
So I support Juergen's proposal of separately
recognizing the power and speed of the tools.

And I also agree with Hans' proposal of listing the
concrete ('established') techniques which are used
in the tools.

Best regards,

Salvador.



Mensaje citado por "Koprowski, A." <A.Koprowski at tue.nl>:

>
>   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
>




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

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