[Termination tools] TPA's bug

[Koprowski, A.]

  Dear all,

 Jambox is not the only tool that took part in the competition and
contained a bug - the same holds for TPA. The bug made TPA to
occasionally admit not well-founded precedences for RPO. 

 To the best of my knowledge there are 6 proofs affected. 4 in TRS
category:
-) Cime - ack_prolog
-) HM - t012
-) Hofwald - 2
-) Rubio - ackclaude
 and 2 in SRS category:
-) Zantema - z035
-) secret2005 - jambox1

 The credit for unrevealing this bug goes to Johannes Waldmann and his
student Andreas Gebhardt - thanks a lot!

 As Johannes Waldmann remarked me, and I do fully agree, this clearly
indicates that we cannot blindly trust proofs generated by tools and
that there is room and need for such an initiative as CoLoR
(http://color.loria.fr) that aims at certification of termination
proofs. And it's not only about Jambox and TPA as bugs in termination
tools happened also before and, considering their complexity, we have to
be prepared that they will show up once in a while.

  Kind regards,
   Adam

========================================================================
 Adam Koprowski, (A.Koprowski at tue.nl, http://www.win.tue.nl/~akoprows)
 Department of Mathematics and Computer Science
 Eindhoven University of Technology (TU/e)
 The difference between impossible and possible lies in determination
      Tommy Lasorda 
========================================================================