[Termtools] timing

[Zantema, H.]

Claude wrote:

> I don't think we should be too strict about the "rules" of the
competition. Being the "winner" is not that important. What is
important is to have a clear idea of respective power of existing
tools. It is also important to motivate and support research on
termination techniques, to emphasize interesting problems, open new
challenges. 

> With respect to this, I think this year's competition is very
successful: it demonstrates the practical power of the matrix
interpretation technique ; I would say that the current Jambox version
has
demonstrated to be a tool of choice for anyone interested in using
termination tools. Personally, I would say that in the TRS category,
for standard rewriting, AProVE and Jambox are winners ex-aequo.
That is, if anyone asks me "I need to use a tool for helping me
proving termination of some TRSs, what do ypu recommend ?" I would
answer try both AProVe and Jambox !


I fully agree!

> For the SRS category, I would say that Jambox is the clear
winner. 

Again I fully agree!

> Especially, I did not expect that any tool could beat TORPA... 

I knew of the developments of the matrix method which are hardly in
TORPA, so I was prepared.

But apart from the matrix method there are more surprises in Jambox. For
instance, the traditional power of TORPA was in the combination of
labelling and interpretation. Compared to 2005 this year's TORPA
strongly improved with respect to recursive labelling. But several new
SRSs in TPDB were not solved by TORPA, but were solved by Jambox using
other kinds of repeated labelling, combined with the most simple
polynomial interpretations. 

> For the future, the challenge of producing verifiable proofs is to me
the most important. I asked some days ago if we could identify a
"unsolved problem of the year" but nobody answered. I suggested
Waldmann/jw1 : b b b -> a a a , a a a -> b a b. Any other suggestion ?

I agree with this suggestion. Since we observed that last years TPDB
contained only very few real challenges in small SRSs, several of this
kind were added this year, many of which turning out to be too hard for
the present tools. So there are more candidates, e.g. in the Gebhardt
list. I propose to mention a few in the WST report of the competition.

Tomorrow there will be a term rewriting meeting in Amsterdam where I
expect to meet several tool authors. I will give a short presentation on
the preliminary competition 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