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

[René Thiemann]

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

This should be decided by the steering committee and I fully agree  
that this
should be clarified.

One option would be to count the following scores:

Best tool for certification:
# TRSs for that the tool has generated a proof that could be certified

Best combination:
# TRSs for that the tool with corresponding certifier have provided
a certified proof.

Best certifier for TRSs:
# TRS for that proofs have successfully been certified

(in the above three scores, if there are several proofs for the same  
TRS, then
it only counts once, i.e., it suffices to certify one of the proofs  
and there
is no advantage in certifying more than one of them)

Best certifier for proofs:
# proofs that have been certified
(here, each CPF-file that can be certified yields one point, so if there
are multiple proofs for the same TRS perhaps from different tools,
then multiple points can be reached by the certifier)


Best regards,
Rene