[Termination tools] Re: [Fwd: Re: WST'04 Competition of termination Systems]

[Claude Marche]

First: please send messages regarding the competition to
termtools at lri.fr only, the list is for this purpose. People willing to
follow the discussion should register.
 
>>>>> "Juergen" == Juergen Giesl <giesl at informatik.rwth-aachen.de> writes:

    Juergen> 1. I think that the problems should not be chosen
    Juergen>     from the data base by the organizers. This has
    Juergen>     two disadvantages:

    Juergen>      a) Since all these examples are known before, people
    Juergen>         can train their system w.r.t. the data base.

    Juergen>      b) It might give a strange impression if
    Juergen>         the organizers (who most likely
    Juergen>         participate themselves) have more influence or
    Juergen>         more knowledge about the examples than the other
    Juergen>         participants.

    Juergen>     Therefore, I think the better solution is that
    Juergen>     the examples for the competition come from the participants
    Juergen>     (as Hans suggested), where everyone can bring a
    Juergen>     fixed number of examples, e.g. 10. These examples
    Juergen>     should be unknown before to everyone, including
    Juergen>     the organizers. Since the competition
    Juergen>     will be performed on just one computer, this is easy to
    Juergen>     organize (the participants just have to bring
    Juergen>     their examples on a floppy or memory stick etc.)

But then what is the advantage of organizing the competition ? :-)

More seriously:

. about the "cheating issue" : I hope that nobody will try to make a
tool that "recognizes" the given problem and extracts the correct
answer from his own database... So my guess is that it would be an
issue only if there were billions of dollars to win.

. About the selection of examples: my current plan is to run the tools
on ALL examples of last year's TPDB. Nothing else. So yes, your idea
of asking of fixed number of examples from participants is
interesting. We could ask to other persons as well.


    Juergen> 2. I think that there should be several categories,
    Juergen>     not just TRS, SRS, and LP. For example, there might
    Juergen>     be a category for TRC with AC, just innermost termination,
    Juergen>     just full termination, etc. In particular, I don't think
    Juergen>     that it is a good idea to only to offer a category for proving
    Juergen>     both termination and non-termination. Since most systems
    Juergen>     specialize on proving termination, I think there should
    Juergen>     clearly be a category where only "YES" counts (here I completely
    Juergen>     agree with Hans). One could of course have another category,
    Juergen>     where only "NO" or both "YES" and "NO" counts, and then
    Juergen>     most likely only systems will participate in this category
    Juergen>     which have a feature for non-termination proofs.

First, let's see if there is any tool able to answer NO. 

About sub-categories: yes, I would like to make a scoring for
AC-termination, innermost termination and such. But for the
competition organization, it is simpler to run tools on every TRS
examples. 

- claude



-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |