[Termination tools] termination competition: certification of proofs

[Frederic Blanqui]

On Mon, 9 May 2005, Koprowski, A. wrote:

>  But then the goal is to come up with the XML schema. For that I see
> another problem not mentioned so far, namely that it's not only about
> the choice of used "building blocks" (ie. basic theorems) but also about
> their precise shape. As far as I know different tools use different
> variants of commonly known theorems (dependency pair transformation is
> the best example). This format should somehow try to capture all of them
> and that's why the more authors of the tools involved in work on this
> format the better.

yes, there are many different variants for every general technique (eg. DP). 
that is why i was insisting on clearly identifying all these variants. color's 
developpers will greatly appreciate to get such details.

>  If there are no other volunteers I can try to propose a (preliminary)
> format that would be suitable for TPA. It could serve as a starting
> point for extension/discussion.

with pleasure!