[Termtools] TRS competition

[Johannes Waldmann]

So we have a thrilling TRS competition now!

Lots of suspense in there, as the problems seem to be handled
in alphabetical (?) order, mixing subcategories. Slightly eccentric,
but it's fine. Currently, we are in the "relative" section.


I wonder whether this proof is correct:
http://www.lri.fr/%7Emarche/termination-competition/2006/webform.cgi?command=viewres&tool=cime&prob=TRS.HofWald.7.trs
(in fact I don't see enough information to reconstruct the meaning)
The original proof by Dieter Probst and Thomas Studer
was worth a few pages in TCS  254(1-2): 677-681 (2001)
http://www.iam.unibe.ch/~tstuder/papers/j.pdf


PS: I know it is equally questionable of Matchbox not to print
*-bound certificate automata. But one could just run TTTbox
on the respective sub-TRSs to see the automata :-)
Really, I am thinking of a way to provide the certificates
after the fact, e. g. by a "-verbose" option that should print
exactly the same proof but with full detail.
So, for the moment please take the number of states as something
like a hash code (not a very unique one) of the real certificate.


Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools