[Termtools] SRS standard sub-category

[Zantema, H.]

* torpa added the matrix method (via SAT), and this should bring it up
to jambox'  performance (roughly);
  and quasi-periodic interpretations (RTA07 paper by Hans and me),
this gives an additional advantage

The main addition for TORPA is quasi-periodic interpretations. Indeed I
also implemented full matrix interpretations, and even labelling with
arbitrary size finite models, all encoded in SAT, but in the competition
version this is mainly switched off due to poor performance (very time
consuming, hardly new proofs compared to the old TORPA versions). Only
for Z86 and systems having very similar properties matrix
interpretations are tried. Essentially in the present version the old
TORPA techniques are tried for a fixed period of 8 to 10 seconds, and
then quasi-periodic interpretations are tried. This explains why the
time is always over around 10 seconds for the new Waldmann07 systems
that were selected on failing on all 2006 tools. For non-termination not
a single letter was changed in the TORPA code.

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.

Extrapolating the results until now, I expect that Matchbox will be the
winner this year in the category of standard string rewriting. Johannes:
congratulations! 

Several emails of the last days on this list refer to the change of the
time limit to 120 seconds. Since Claude is the only one having the
overview of available machines, he is the only one who can decide
whether increase of time limit is feasible or not. Several times it was
indicated that in case of changing the time limit this should be
announced in advance. On the one hand it is a pity that this did not
happen, probably due to the fact that Claude was in doubt until short
before running the competition. 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.

            Best regards, Hans Zantema.

_________________________________________________________
Dr Hans Zantema            
Technische Universiteit Eindhoven, Department of Computer Science 
P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
office: Hoofdgebouw room 6.73, tel: (040)2472749