[Termtools] Complexity and certified categories in upcoming termination competition

[Thiemann, Rene]

Dear all,

there have slight changes concerning the upcoming termination competition w.r.t. the certification mode and the complexity mode.

Certification: 
The new version CPF 2.3 is used instead of the older CPF 2.2. Since the new version just mentions additional proof-techniques, there is no need to change anything in your tools, except if you want to include some of these techniques in your generated proofs. For testing, we propose to use CeTA 2.20.

Complexity:
The first line of the output has been slightly modified, making it less ambiguous and specifying precisely the allowed lower bounds. In short, a typical answer is of the form

WORST_CASE(Omega(n^1),O(n^5))    or    MAYBE

where in the former case one of the bounds can be replaced by ?. Moreover, both lower bounds and upper bounds will be used for scoring, similar to counting both YES and NO for termination.



The new formats and the scoring are documented under the following links:

http://termination-portal.org/wiki/Termination_Competition_2015#Changes_with_respect_to_2014
http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/rules.php
http://cl-informatik.uibk.ac.at/software/cpf/

Comments are of course welcome.

With best regards,
René Thiemann