[Termtools] [Termcomp] Fwd: Re: [color] Termination Competition 2009: Call for Participation

[René Thiemann]

Am 11.12.2009 um 13:29 schrieb Johannes Waldmann:

>
>>> It should be clear before starting the competition
>>> how the tools (the provers AND  the
>>> certifiers) are going to be evaluated?
>
>> This should be decided by the steering committee [...]
>
> well, who made the proposal for running certification in three stages?
> same person should make a proposal for scoring ... then SC decides :-)

I think I was involved in that part. Therefore, in the previous mail I  
made
a concrete proposal :-)

> We should take into account:
> * all participants should be happy with the decision -
>  so some open discussion seems necessary

Sure, therefore I made a public proposal to termtools where everyone  
can see it
and give comments.

> * scoring algorithm must be easy/trivial to implement on termcomp,
>  otherwise competition cannot start on schedule.

The proposed scoring is easy to implement, it just needs some SQL- 
queries
which do not even have to be ready when running the competition. Since  
all
certifiers are run on all generates proofs, every scoring function can  
be
implemented afterwards.

> Especially with an eye to the schedule,
> the most trivial implementation is none. This would mean:
> * provers are evaluated according to
>  whether they produced any certificate

I do not agree here, one should take into account whether the  
certificate
is really accepted by at least one of the certifiers. Provers should not
be awarded with points for wrong/uncertifiable proofs.

> * certifiers are evaluated according to
>  whether they could verify a certificate.

Agreed. The question is just, do we count "certified TRSs" or  
"certified proofs",
cf. scoring theme 3 and 4 from my previous mail. Since both scores are  
somehow
sensible I would like to display them both.

Moreover, in my opinion it also makes sense to display a winning  
combination
of tool and certifier.

Cheers,
Rene