[Termtools] Re: SRS standard sub-category

[Johannes Waldmann]

[Hans wrote:]

> It is nice to see that by techniques developed during the last year
> termination proofs could be found for very many systems that were
> unsolvable for all tools last year.

what surprises me most is that the "green spots" of matchbox,
torpa and ttt2 seem to be clearly related, despite rather
different proof methods (arctic matrices, QPI, self labelling)

> ... I expect that Matchbox will be the winner this year
> in the category of standard string rewriting. Johannes:
> congratulations! 

well, thanks, altough this may be a bit premature.
matchbox will not work so well on some of the "known" problems.
although it will hopefully produce a nice z086 proof.

what is more certain is that Jörg won the relative subcategory,
so congrats for that - although I'd like to see the accumulated
weighted scores as well.
(Note that both Torpa and Mu-No-Mu have solved a 75 % problem,
while jambox and matchbox haven't)


> ... On the other hand, as we see hardly
> proofs that are found in a time between 60 and 120 aeconds, probably the
> change of the time limit hardly has influence on the final results.

No, I think the "120" definitely affects jambox' performance.



What is happening in the TRS category meanwhile? Anyone care to comment?
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------