[Termtools] New version of the certification problem format available

[René Thiemann]

Dear all,

the certification problem format (CPF) that is used for the certified termination competition has been extended in several ways. For example, it now contains elements for relative termination proofs and also allows to express more complex non-termination proofs that are using dependency pairs.

Most of these changes are backward compatible, however there are also some minor non-backward-compatible changes in order to improve the format. Note that all existing proofs of the old version of CPF can automatically be transformed into the new system using some tiny script that is available from the CPF-website.

All details about the (old and) new format are available at

http://cl-informatik.uibk.ac.at/software/cpf/

where also several examples of proofs are given.

Best regards,
René Thiemann