[Termtools] TPA

[Zantema, H.]

Dear Claude,

I just extensively discussed the situation of TPA with Adam.

For the standard category an error was found, by which the final version
was replaced by the preliminary version, both for the standard category
and the certified category.

In the mean time it turned out that due to a bug in this preliminary
version (which has been solved in the final version) sometimes wrong
proofs are generated.

This shows the power of the certified category: here indeed the Coq
verification ends in the observation that the generated proof is wrong.

So for both the final version and the preliminary version of TPA there
are errors resulting in wrong proofs. Adam indicates himself that either
TPA should withdraw or should be disqualified.

Our joined proposal:

* TPA withdraws in the standard category.

* TPA participates in the certified category with the final version.
Note that the reason of replacing the final version by the preliminary
version was only due to an error for the standard category. This error
is independent of the certified category: it occurred in a technique for
which certification is not supported.

This means that the results in the standard category (both for term
rewriting and string rewriting) for TPA should be removed, and that the
certified category should be restarted with using the final version of
TPA rather than the preliminary version.

By this solution the following question of Claude is not relevant any
more.

> Adam agreed to use the preliminary version of TPA instead, but still
wanted me to keep the final rainbow.

> The last thing I can do is to revert back to the preliminary version
of rainbow.

> Adam ?
 


            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