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

[Frederic Blanqui]

Hello Rene.

René Thiemann a écrit :
> Dear Frédéric,
> 
> I am not in the official position (as part of the steering committee)
> to answer your mail but nevertheless want to give some answers
> as part of the organizers.
> 
> Frédéric wrote:
>>
>> could you please give more details on the way the certified category
>> will be run?
>>
>> 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.
> 
>> Finally, why do you restrict proofs to
>> be in the new format (CPF I guess)?
> 
> The idea is to also generate a collection of termination or 
> nontermination proofs similar
> to the TPDB itself which can then serve as a database of challenges for 
> certifiers.
> This seems to be advantageous for two main reasons: first, certifiers 
> become more comparable since
> they now have to certify the same proofs instead of different proofs for 
> the same TRS; and second,
> termination prover only have to export into one proof format instead of 
> three.
> Since all certifiers agreed to support CPF the 2nd item was stated.
> 
>> If a tool implements a new
>> termination criterion and a certifier for it, it may be the case that
>> there is no corresponding proof in the CPF format (yet).
> 
> There is still the possibility to add it to CPF: make some concrete XML 
> proposal, it will be put under
> discussion, and then it can be made public before the competition.

I understand and agree with you but, still, I think that we should leave 
open the possibility of using something else for allowing people outside 
this community to participate to this competition...