[Termination tools] some interesting small TRSs

[Johannes Waldmann]

Dear all,

here's some entertainment for those (like me)
that couldn't make it to RTA ...

I am currently running an enumeration of "small but hard" TRSs
and apply some of the termination provers (Aprove, Teparla, TTT, 
Matchbox): http://dfa.imn.htwk-leipzig.de/~waldmann/running/

The TRSs are one-rule systems in the signature:
{ nullary a, unary h, binary f }
To save space, I only keep those systems
where at most two of the tools gave an answer
(within 60 s, 2 GHz machine)

The choice of the tools and the enumeration is rather arbitrary,
so one should not jump to conclusions (and I am not implying any).

The nice thing is that for everyone, there's something in it :-)
e. g. for each each tool T there are some TRSs
that can only be handled by T.

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