[Termtools] complexity competition

[Georg]

Dear Johannes!

>Thanks, Georg. - What I don't get is why all of a sudden
>there are two competing complexity teams from the very same site
>(same floor, even?). 


That is very simple to answer: Chris, Harald, and Martin realised that 
it was very easy
for them to take a  subset of the TTT2 code and transform it into a 
complexity analyser.
And, apparently they did a good job.

When they informed me about this plan, I of course encouraged it. Actually
I would be very pleased, if all authors of termination provers think about
entering the complexity category with suitable adaptions of their tools.

>How different are these implementations?
>Perhaps the respective authors can enlighten us ... - Johannes.


Both tools are partially build up on basic libraries of TTT2, that explains
for example the common output format. Moreover the tools have 
implemented triangular
matrices, match-bounds and root labeling. In addition CaT uses arctic 
matrix method and TCT
incorporates weak dependency pairs, weak dependency graphs, POP* and
finite semantic labeling.  The main reason why the CaT tool won is (i) a 
cleverer strategy
that uses (triangular) matrix interpretations for higher dimensions and 
(ii) arctic matrix method,
which I suppose will please you.

As indicated, both tools are open source, hence the source is available 
in the respective
web pages, available via the termination-portal since November 1, which 
also includes further documentation.

best wishes,
Georg