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

[René Thiemann]

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.

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

Best regards,
René
-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck