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

[Frederic Blanqui]

Frederic Blanqui a écrit :

>>> From the webpage, I can read:
>>>
>>> "The certified categories will be run as follows:
>>>
>>>   1. After the corresponding uncertified category of the competition
>>> has finished, the problems that have been solved (yes or no) are
>>> collected and form the initial selection for the certified category.
>>>   2. Termination tools that can produce output in the new format and
>>> that participate in the certified competition are then run on the
>>> collection of 1, resulting in a collection of termination proofs.
>>> (Termination provers may use a different strategy from the uncertified
>>> competition, to increase chances of the proof being certified.)
>>>   3. The certifiers are then run on the collection produced by 2."
>>>
>>> In 3, what are the "certifiers"? Who is providing them?
>> It is assumed that the certifiers are all those who want to participate,
>> i.e., most likely the combinations CiME/Coccinelle/Coq, 
>> Rainbow/CoLoR/Coq, and CeTA.
> 
> Ok, so it means that certifiers must also register for participating to 
> the competition, independently of provers. This is different from 
> previous years, where provers had to provide the runme and checkme 
> programs, and this is not clear from the announcement and the rules.
> 
> Then, do we have to provide a unique command (like checkme)? And, how to 
> make sure that every thing runs well: is there going to be any test 
> before starting the competition?
> 
>>> If there are n
>>> certifiers, do you mean that you are going to run the n certifiers on
>>> each proof provided by each tool?
>> Yes, this is the plan.

Then, what is going to be the output of the competition? It should be 
clear before starting the competition how the tools (the provers AND the 
certifiers) are going to be evaluated? Nothing is said about that in the 
call nor in the rules.