[Termtools] Remarks on the Termination Competition

[Zantema, H.]

> In my opinion, it is not good that incorrect
proofs are publicly available through the web site of the competition. 
This was the main reason for us to ask for the removal of MU-TERM's
proofs.

>> Several other tool authors found errors in their tools
>>after the competition was finished without any consequence for the
>>result pages.
>
>Here, I would apply the same rule. Keeping wrong results available
could 
>become problematic in the future...

In general I fully agree, but in practice it is impossible to detect and
remove all wrong results. Thousands of proofs have been generated
automatically. Most of the generated text is quite unreadable for every
one who did not write the code generating it, and is very long and
complicated. For checking correctness you should be aware of all details
of the underlying techniques. Some tool authors are very open about the
errors they found in their tools and tell about it on the termtools
list, some others do not. I think it would not be fair that in the
policy of possibly removing wrong proofs we are mainly guided by this
attitude of tool authors. 

I think an important direction to overcome these problems is in
certification. Until short time ago many people were quite sceptical
about feasibility of this, but the present results on the certified
category are much more positive: for quite complicated techniques full
certification can now be provided fully automatically.

            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: Salvador Lucas [mailto:slucas at dsic.upv.es] 
Sent: dinsdag 12 juni 2007 15:48
To: Zantema, H.
Cc: Juergen Giesl; termtools at lri.fr
Subject: Re: [Termtools] Remarks on the Termination Competition