[Termination tools] termination competition: certification of proofs

[Aart Middeldorp]

A somewhat slow response from the TTT team. The idea to certify
the output produced by termination tools is around for some
time. We strongly support the development of an interface to
express termination proofs which is independent of both the
existing termination tools as well as the underlying proof
assistant. The interface should be easily extendable, triggered
by developments in termination tools, and XML is the obvious
format.

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.

-- Aart