[Termtools] Upcoming competition

[Aart Middeldorp]

It seems to me that the SAT competition has a good understanding of
the challenge of producing non-proofs, by adopting three different
specialties:

SAT        (counting YES answers)
UNSAT      (counting NO answers)
SAT+UNSAT  (counting both)

With the current (interpretation of the) rules, the participating
tools face the question whether to spend/waste any time on proving
non-termination.

Cheers,

Aart

Zantema, H. wrote:
> Since the beginning of the competition we avoided to have very precise definitions of who is the winner, and also it was decided not to reward prizes. 
> 
> Instead every year there is a report on the competition, in which it is tried to present relevant observations on the results as careful as possible.
> 
> Technically it is very simple apart from the YES score and the NO score also to add the sum of these two in the results pages. But what goal does it serve? There are that many issues that could have been added too (count time-out separate from MAYBE, include standard deviations of measured time, count systems that are solved by only this tool, ...).
> 
> 
> 
>             Best regards, Hans Zantema.
> 
> _________________________________________________________
> Dr Hans Zantema            
> Technische Universiteit Eindhoven, Department of Computer Science 
> P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
> e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
> office: Hoofdgebouw room 6.73, tel: (040)2472749
>  
> 
> -----Original Message-----
> From: termtools-bounces at lists.lri.fr [mailto:termtools-bounces at lists.lri.fr] On Behalf Of Rene Thiemann
> Sent: dinsdag 15 mei 2007 16:26
> To: termtools at lists.lri.fr
> Subject: Re: [Termtools] Upcoming competition
> 
> Hi,
> 
> Johannes wrote about color-workshop
>> 2) count YES and/or NO: generally, the idea of summing both counts
>> (to determine the overall winner) was favoured.
>> It was the impression that this was the original intention,
>> but it had been neglected in last year's report.
>>
> 
> COMMENT of Hans:
>> I am not aware of this. We call it a termination competition, so
>> obviously the results on termination proofs should be counted. Apart
>> from that it was decided from the beginning in 2004 also to count 'NO'
>> results. Adding 'YES' and 'NO' results, and present this as a final
>> result, would be something new.
>> As I said, I am not aware that this ever was an intention. In any case,
>> changing this so short before the deadline should not be done.
> 
> 
> I do not see like Hans that this is something new. Here is the corresponding 
> paragraph from the termination competition website:
> 
> ------SNIP---------
> ...
> The answer must start by either YES or NO, meaning that the given rewrite 
> system is terminating (respectively, not terminating) under the STRATEGY 
> given in the input file.
> ...
> 
> On the web page a score table will be presented for each category, by giving 
> one point for each (correct) answer.
> ------SNAP----------
> 
> So, from the above text I cannot see that YES and NO answers are something 
> different and that YES and NO answers should be counted separately.
> 
> Thus, if YES and NO's are counted separately, then this should be clearly 
> stated somewhere in the rules.
> 
> Best regards,
> Rene