[Termination tools] termination competition: certification of proofs

[Frederic Blanqui]

On Thu, 26 May 2005, Aart Middeldorp wrote:

> We think it is neither realistic nor desirable to demand that tools 
> participating in the next termination competition produce output in the new 
> format. Such a demand will do nothing to attract new tools.

yes, it should be optional. adam koprowski and i are going to design some xml 
format, and develop some interface for coq/color. we will inform the termtools 
list when it will be ready.